🔍

Equations Inline Footnotes

open import Cat.Functor.Adjoint.Reflective
open import Cat.Functor.Properties
open import Cat.Diagram.Terminal
open import Cat.Functor.Adjoint
open import Cat.Morphism.Class
open import Cat.Morphism.Lifts
open import Cat.Prelude

import Cat.Functor.Reasoning.FullyFaithful
import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Morphism.Orthogonal where

Orthogonal maps🔗

A pair of maps $f:a\to b$ and $g:c\to d$ are called orthogonal, written $f\perp g$¹, if for every $u,v$ fitting into a commutative diagram like

the space of liftings $c\to b$ (dashed) which commute with everything is contractible. We will also speak of orthogonality of an object and a morphism, a morphism and a class of morphisms, and so on.

module _ {o ℓ} (C : Precategory o ℓ) where
  open Cat.Reasoning C
  open Terminal
  private
    variable
      a b c d x y : ⌞ C ⌟
      f g h u v : Hom a b

If the ambient category $\mathcal{C}$ has enough co/limits, being orthogonal to an object is equivalent to being orthogonal to a morphism. For example, $f\perp X$ iff. $f\perp {!}_X\text{,}$ where ${!}_X:X\to 1$ is the unique map from $X$ into the terminal object.

  object-orthogonal-!-orthogonal
    : ∀ {X : Ob} (T : Terminal C) (f : Hom a b)
    → Orthogonal C f X ≃ Orthogonal C f (! T {X})

The proof is mostly a calculation, so we present it without a lot of comment.

  object-orthogonal-!-orthogonal {X = X} T f = prop-ext! fwd bwd where
    module T = Terminal T

    fwd : Orthogonal C f X → Orthogonal C f T.!
    fwd f⊥X u v sq .centre =
        f⊥X u .centre .fst
      , f⊥X u .centre .snd
      , T.!-unique₂ _ _
    fwd f⊥X u v sq .paths m = Σ-prop-path! $
      ap fst (f⊥X u .paths (m .fst , m .snd .fst))

    bwd : Orthogonal C f (! T) → Orthogonal C f X
    bwd f⊥! u .centre =
        f⊥! u T.! (T.!-unique₂ _ _) .centre .fst
      , f⊥! u T.! (T.!-unique₂ _ _) .centre .snd .fst
    bwd f⊥! u .paths (w , eq) = Σ-prop-path! $
      ap fst (f⊥! _ _ _ .paths (w , eq , (T.!-unique₂ _ _)))

As a passing observation we note that if $f\perp X$ and $X\cong Y\text{,}$ then $f\perp Y\text{.}$ Of course, this is immediate in categories, but it holds in the generality of precategories.

  obj-orthogonal-iso
    : ∀ {a b} {X Y} (f : Hom a b)
    → X ≅ Y → Orthogonal C f X → Orthogonal C f Y

  obj-orthogonal-iso f x≅y f⊥X a =
    contr
      ( g.to ∘ contr' .centre .fst
      , pullr (contr' .centre .snd) ∙ cancell g.invl )
      λ x → Σ-prop-path! $
        ap₂ _∘_ refl (ap fst (contr' .paths (g.from ∘ x .fst , pullr (x .snd))))
        ∙ cancell g.invl
    where
      module g = _≅_ x≅y
      contr' = f⊥X (g.from ∘ a)

A slightly more interesting lemma is that, if $f$ is orthogonal to itself, then it is an isomorphism:

  self-orthogonal→invertible
    : ∀ {a b} (f : Hom a b) → Orthogonal C f f → is-invertible f
  self-orthogonal→invertible f f⊥f =
    let (f , p , q) = f⊥f id id (idl _ ∙ intror refl) .centre in
    make-invertible f q p

If $f$ is an epi or $g$ is a mono, then the mere existence of any lift is enough to establish that $f\perp g\text{.}$

  left-epic-lift→orthogonal
    : (g : Hom c d)
    → is-epic f → Lifts C f g → Orthogonal C f g
  left-epic-lift→orthogonal g f-epi lifts u v vf=gu = is-prop∥∥→is-contr
    (left-epic→lift-is-prop C f-epi vf=gu)
    (lifts u v vf=gu)

  right-monic-lift→orthogonal
    : (f : Hom a b)
    → is-monic g → Lifts C f g → Orthogonal C f g
  right-monic-lift→orthogonal f g-mono lifts u v vf=gu = is-prop∥∥→is-contr
    (right-monic→lift-is-prop C g-mono vf=gu)
    (lifts u v vf=gu)

  left-epic-lift→orthogonal-class
    : ∀ {κ} (R : Arrows C κ)
    → is-epic f → Lifts C f R → Orthogonal C f R
  left-epic-lift→orthogonal-class R f-epic lifts r r∈R = left-epic-lift→orthogonal
    r f-epic (lifts r r∈R)

  right-monic-lift→orthogonal-class
    : ∀ {κ} (L : Arrows C κ)
    → is-monic f → Lifts C L f → Orthogonal C L f
  right-monic-lift→orthogonal-class L f-epic lifts l l∈L =
    right-monic-lift→orthogonal l f-epic (lifts l l∈L)

As a corollary, we get that isomorphisms are left and right orthogonal to every other morphism.

  invertible→left-orthogonal : (g : Hom c d) → Orthogonal C Isos g
  invertible→left-orthogonal g f f-inv =
      left-epic-lift→orthogonal g (invertible→epic f-inv)
    $ invertible-left-lifts C f f-inv

  invertible→right-orthogonal : (f : Hom a b) → Orthogonal C f Isos
  invertible→right-orthogonal f g g-inv =
      right-monic-lift→orthogonal f (invertible→monic g-inv)
    $ invertible-right-lifts C g g-inv

Phrased another way, the class of isomorphisms is left and right orthogonal to every other class.

  isos-left-orthogonal : ∀ {κ} (R : Arrows C κ) → Orthogonal C Isos R
  isos-left-orthogonal R f f-inv r r∈R = invertible→left-orthogonal r f f-inv

  isos-right-orthogonal : ∀ {κ} (L : Arrows C κ) → Orthogonal C L Isos
  isos-right-orthogonal L l l∈L f f-inv = invertible→right-orthogonal l f f-inv

  invertible→left-orthogonal-class : ∀ {κ} (R : Arrows C κ) → is-invertible f → Orthogonal C f R
  invertible→left-orthogonal-class R f-inv r _ = invertible→left-orthogonal r _ f-inv

  invertible→right-orthogonal-class : ∀ {κ} (L : Arrows C κ) → is-invertible f → Orthogonal C L f
  invertible→right-orthogonal-class L f-inv l _ = invertible→right-orthogonal l _ f-inv

  orthogonal→lifts-against : Orthogonal C f g → Lifts C f g
  orthogonal→lifts-against o u v p = pure (o u v p .centre)

  orthogonal→lifts-left-class
    : ∀ {κ} (L : Arrows C κ)
    → Orthogonal C L f → Lifts C L f
  orthogonal→lifts-left-class L L⊥f l l∈L =
    orthogonal→lifts-against (L⊥f l l∈L)

  orthogonal→lifts-right-class
    : ∀ {κ} (R : Arrows C κ)
    → Orthogonal C f R → Lifts C f R
  orthogonal→lifts-right-class R f⊥R r r∈R =
    orthogonal→lifts-against (f⊥R r r∈R)

Fully faithful functors🔗

module _
  {oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd}
  (ι : Functor C D)
  (ι-ff : is-fully-faithful ι)
  where
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module ι = Cat.Functor.Reasoning.FullyFaithful ι ι-ff

If $\iota :\mathcal{C}\to \mathcal{D}$ is a fully faithful functor and $\iota (f)\perp \iota (g)$ in $\mathcal{D}\text{,}$ then $f\perp g$ in $\mathcal{C}\text{.}$

  ff→reflect-orthogonal
    : ∀ {A B X Y} {f : C.Hom A B} {g : C.Hom X Y}
    → Orthogonal D (ι.₁ f) (ι.₁ g)
    → Orthogonal C f g

Suppose that $\iota (f)\perp \iota (g)\text{,}$ and let $v\circ f=g\circ u$ be a square in $\mathcal{D}\text{.}$ Functors preserve all commutative diagrams, so we also have a square $\iota (v)\circ \iota (f)=\iota (g)\circ \iota (u)$ in $\mathcal{D}\text{.}$ This in turn gives us a lift $w$ of the square in $\mathcal{D}\text{,}$ as $\iota (f)\perp \iota (g)\text{.}$ Moreover, $\iota$ is fully faithful, so we can reflect this lift back to $\mathcal{C}\text{.}$

  ff→reflect-orthogonal {f = f} {g = g} ι[f]⊥ι[g] u v vf=gu .centre =
    ff→reflect-lifting ι ι-ff (ι[f]⊥ι[g] (ι.₁ u) (ι.₁ v) (ι.weave vf=gu) .centre)

Uniqueness of the lift follows from a similar argument. Let $w^{\prime }$ be a lift of the square $v\circ f=g\circ u\text{.}$ Functors preserve liftings, so $\iota (w^{\prime })$ is a lift of $\iota (v)\circ \iota (f)=\iota (g)\circ \iota (u)\text{.}$ However, $\iota (f)\perp \iota (g)\text{,}$ so $\iota (w^{\prime })=w\text{.}$ Finally, $\iota$ is an equivalence on hom sets, so we get $w^{\prime }={\iota }^{-1}(w)\text{.}$

  ff→reflect-orthogonal {f = f} {g = g} ι[f]⊥ι[g] u v vf=gu .paths w =
    Σ-prop-path! $ sym $ ι.adjunctl $ sym $ ap fst
    $ ι[f]⊥ι[g] (ι.₁ u) (ι.₁ v) (ι.weave vf=gu) .paths (F-map-lifting ι w)

Regarding reflections🔗

module
  _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
    {r : Functor C D} {ι : Functor D C}
    (r⊣ι : r ⊣ ι) (ι-ff : is-fully-faithful ι)
  where
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module ι = Cat.Functor.Reasoning.FullyFaithful ι ι-ff
    module r = Cat.Functor.Reasoning r
    module rι = Cat.Functor.Reasoning (r F∘ ι)
    module ιr = Cat.Functor.Reasoning (ι F∘ r)

    module r⊣ι = _⊣_ r⊣ι

    module counit where
      open r⊣ι.counit public

      ε-inv : ∀ x → D.is-invertible (ε x)
      ε-inv x = is-reflective→counit-is-invertible r⊣ι ι-ff {o = x}

      module ε⁻¹ x = D.is-invertible (ε-inv x)
      open ε⁻¹
        renaming (inv to ε⁻¹)
        using (invl; invr)
        public

    open r⊣ι hiding (module counit)

Let $r⊣\iota :\mathcal{D}\rightleftarrows \mathcal{C}$ be an arbitrary reflective subcategory. Speaking abstractly, there is a “universal” choice of test for whether an object is “in” the subcategory: Whether the adjunction unit: ${\eta }_x:x\to \iota r(x)$ is an isomorphism. The theory of orthogonality gives a second way to detect this situation. The proof here is from (Borceux 1994, vol. 1, sec. 5.4).

The first thing we observe is that any map $f$ such that $r(f)$ is an isomorphism is orthogonal to every object in the subcategory: $f\perp \iota (X)\text{.}$ Let $f:a\to b$ be inverted by $r\text{,}$ and $X$ be the object. Given a map $a:a\to \iota X\text{,}$

  in-subcategory→orthogonal-to-inverted
    : ∀ {X} {a b} {f : C.Hom a b} → D.is-invertible (r.₁ f) → Orthogonal C f (ι.₀ X)
  in-subcategory→orthogonal-to-inverted {X} {A} {B} {f} rf-inv a→x =
    contr (fact , factors) λ { (g , factors') → Σ-prop-path! (h≡k factors factors') }
    where
      module rf = D.is-invertible rf-inv
      module η⁻¹ {a} = C.is-invertible (is-reflective→unit-right-is-iso r⊣ι ι-ff {a})

Observe that, since $r⊣\iota$ is a reflective subcategory, every unit morphism ${\eta }_{\iota X}$ is an isomorphism; We define a morphism $b:\iota r(A)\to \iota X$ as the composite

      b : C.Hom (ι.₀ (r.₀ A)) (ι.₀ X)
      b = η⁻¹.inv C.∘ ι.₁ (r.₁ a→x)

satisfying (by naturality of the unit map) the property that $b\eta =a\text{.}$ This is an intermediate step in what we have to do: construct a map $B\to \iota (X)\text{.}$

      p : a→x ≡ b C.∘ unit.η _
      p = sym (C.pullr (sym (unit.is-natural _ _ _)) ∙ C.cancell zag)

We define that using the map $b$ we just constructed. It’s the composite

and a calculation shows us that this map is indeed a factorisation of $a$ through $f\text{.}$

      fact : C.Hom B (ι.₀ X)
      fact = b C.∘ ι.₁ rf.inv C.∘ unit.η _

      factors =
        (b C.∘ ι.₁ rf.inv C.∘ unit.η B) C.∘ f      ≡⟨ C.pullr (C.pullr (unit.is-natural _ _ _)) ⟩≡
        b C.∘ ι.₁ rf.inv C.∘ (ιr.₁ f) C.∘ unit.η A ≡⟨ C.refl⟩∘⟨ C.cancell (ι.annihilate rf.invr) ⟩≡
        b C.∘ unit.η A                             ≡˘⟨ p ⟩≡˘
        a→x                                        ∎

The proof that this factorisation is unique is surprisingly totally independent of the actual map we just constructed: If $hf=a=kf\text{,}$ note that we must have $r(h)=r(k)$ (since $r(f)$ is invertible, it is epic); But then we have

and since ${\eta }_{\iota X}$ is an isomorphism, thus monic, we have $h=k\text{.}$

      module _ {h k : C.Hom B (ι.₀ X)} (p : h C.∘ f ≡ a→x) (q : k C.∘ f ≡ a→x) where
        rh≡rk : r.₁ h ≡ r.₁ k
        rh≡rk = D.invertible→epic rf-inv (r.₁ h) (r.₁ k) (r.weave (p ∙ sym q))

        h≡k = C.invertible→monic (is-reflective→unit-right-is-iso r⊣ι ι-ff) _ _ $
          unit.η (ι.₀ X) C.∘ h ≡⟨ unit.is-natural _ _ _ ⟩≡
          ιr.₁ h C.∘ unit.η B  ≡⟨ ap ι.₁ rh≡rk C.⟩∘⟨refl ⟩≡
          ιr.₁ k C.∘ unit.η B  ≡˘⟨ unit.is-natural _ _ _ ⟩≡˘
          unit.η (ι.₀ X) C.∘ k ∎

As a partial converse, if an object $X$ is orthogonal to every unit map (it suffices to be orthogonal to its own unit map), then it lies in the subcategory:

  orthogonal-to-ηs→in-subcategory
    : ∀ {X} → (∀ B → Orthogonal C (unit.η B) X) → C.is-invertible (unit.η X)
  orthogonal-to-ηs→in-subcategory {X} ortho =
    C.make-invertible x lemma (ortho X C.id .centre .snd) where
      x = ortho X C.id .centre .fst
      lemma =
        unit.η _ C.∘ x             ≡⟨ unit.is-natural _ _ _ ⟩≡
        ιr.₁ x C.∘ unit.η (ιr.₀ X) ≡⟨ C.refl⟩∘⟨ η-comonad-commute r⊣ι ι-ff ⟩≡
        ιr.₁ x C.∘ ιr.₁ (unit.η X) ≡⟨ ιr.annihilate (ortho X C.id .centre .snd) ⟩≡
        C.id                       ∎

And the converse to that is a specialisation of the first thing we proved: We established that $f\perp \iota (X)$ if $f$ is invertible by the reflection functor, and we know that $\eta$ is invertible by the reflection functor; It remains to replace $\iota (X)$ with any object for which $\eta$ is an isomorphism.

  in-subcategory→orthogonal-to-ηs
    : ∀ {X B} → C.is-invertible (unit.η X) → Orthogonal C (unit.η B) X
  in-subcategory→orthogonal-to-ηs inv =
      obj-orthogonal-iso C (unit.η _)
        (C.invertible→iso _ (C.is-invertible-inverse inv))
    $ in-subcategory→orthogonal-to-inverted
        (is-reflective→left-unit-is-iso r⊣ι ι-ff)