module Cat.Morphism.Orthogonal where

Orthogonal maps🔗

A pair of maps and are called orthogonal, written 1, if for every fitting into a commutative diagram like

the space of arrows (dashed) which commute with everything is contractible.

  m⊥m : ∀ {a b c d} → C.Hom a b → C.Hom c d → Type _
  m⊥m {b = b} {c = c} f g =
    ∀ {u v} → v C.∘ f ≡ g C.∘ u
    → is-contr (Σ[ w ∈ C.Hom b c ] ((w C.∘ f ≡ u) × (g C.∘ w ≡ v)))

We also outline concepts of a map being orthogonal to an object, which is informally written and an object being orthogonal to a map

  m⊥o : ∀ {a b} → C.Hom a b → C.Ob → Type _
  m⊥o {A} {B} f X = (a : C.Hom A X) → is-contr (Σ[ b ∈ C.Hom B X ] (b C.∘ f ≡ a))

  o⊥m : ∀ {a b} → C.Ob → C.Hom a b → Type _
  o⊥m {A} {B} Y f = (c : C.Hom Y B) → is-contr (Σ[ d ∈ C.Hom Y A ] (f C.∘ d ≡ c))

In the formalisation, we don’t write infix, since it must be explicitly applied to the category in which the morphisms live. Thus, we define three distinct predicates expressing orthogonality: m⊥m (“map-map”), m⊥o (“map-object”), and o⊥m (“object-map”). If the ambient category has enough co/limits, being orthogonal to an object is equivalent to being orthogonal to an object. For example, iff. where is the unique map from into the terminal object.

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

    : ∀ {A B X} (T : Terminal C) (f : C.Hom A B) → m⊥o f X ≃ m⊥m f (! T)
  object-orthogonal-!-orthogonal {X = X} T f =
    prop-ext (hlevel 1) (hlevel 1) to from
      to : m⊥o f X → m⊥m f (! T)
      to f⊥X {u} {v} sq =
        contr (f⊥X u .centre .fst , f⊥X u .centre .snd , !-unique₂ T _ _) λ m →
          Σ-prop-path! (ap fst (f⊥X u .paths (m .fst , m .snd .fst)))

      from : m⊥m f (! T) → m⊥o f X
      from f⊥! a = contr
        ( f⊥! {v = ! T} (!-unique₂ T _ _) .centre .fst
        , f⊥! (!-unique₂ T _ _) .centre .snd .fst ) λ x → Σ-prop-path!
          (ap fst (f⊥! _ .paths (x .fst , x .snd , !-unique₂ T _ _)))

As a passing observation we note that if and then Of course, this is immediate in categories, but it holds in the generality of precategories.

  m⊥-iso : ∀ {a b} {X Y} (f : C.Hom a b) → X C.≅ Y → m⊥o f X → m⊥o f Y

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

  self-orthogonal→is-iso : ∀ {a b} (f : C.Hom a b) → m⊥m f f → f
  self-orthogonal→is-iso f f⊥f =
    C.make-invertible (gpq .fst) (gpq .snd .snd) (gpq .snd .fst)
      gpq = f⊥f (C.idl _ ∙ C.intror refl) .centre

Regarding reflections🔗

Let 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: 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 such that is an isomorphism is orthogonal to every object in the subcategory: Let be inverted by and be the object. Given a map

    : ∀ {X} {a b} {f : C.Hom a b} → (r.₁ f) → m⊥o 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') }
      module rf = rf-inv
      module η⁻¹ {a} = (is-reflective→unit-G-is-iso r⊣ι ι-ff {a})

Observe that, since is a reflective subcategory, every unit morphism is an isomorphism; We define a morphism 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 This is an intermediate step in what we have to do: construct a map

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

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

and a calculation shows us that this map is indeed a factorisation of through

      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 ( _ _ _)) ⟩≡
        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 note that we must have (since is invertible, it is epic); But then we have

and since is an isomorphism, thus monic, we have

      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-G-is-iso r⊣ι ι-ff) _ _ $
          unit.η (ι.₀ X) C.∘ h ≡⟨ _ _ _ ⟩≡
          ιr.₁ h C.∘ unit.η B  ≡⟨ ap ι.₁ rh≡rk C.⟩∘⟨refl ⟩≡
          ιr.₁ k C.∘ unit.η B  ≡˘⟨ _ _ _ ⟩≡˘
          unit.η (ι.₀ X) C.∘ k ∎

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

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

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

    : ∀ {X B} → (unit.η X) → m⊥o C (unit.η B) X
  in-subcategory→orthogonal-to-ηs inv =
    m⊥-iso C (unit.η _) (C.invertible→iso _ ( inv))
        (is-reflective→F-unit-is-iso r⊣ι ι-ff))

  1. Though hang tight for a note on formalised notation↩︎