open import Cat.Functor.Adjoint.Reflective
open import Cat.Diagram.Terminal
open import Cat.Functor.Adjoint
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cr

module Cat.Morphism.Orthogonal where

Orthogonal maps🔗

A pair of maps f:a→bf : a \to b and g:c todg : c \ to d are called orthogonal, written f⊥gf {\mathrel{\bot}}g1, if for every u,vu, v fitting into a commutative diagram like

the space of arrows c→bc \to b (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 f⊥Xf {\mathrel{\bot}}X, and an object being orthogonal to a map Y⊥fY {\mathrel{\bot}}f.

  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))

Note: In the formalisation, we don’t write ⊥\bot 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 C\mathcal{C} has enough co/limits, being orthogonal to an object is equivalent to being orthogonal to an object. For example, f⊥Xf {\mathrel{\bot}}X iff. f⊥!Xf {\mathrel{\bot}}\mathop{!}_X, where !X:X→1!_X : X \to 1 is the unique map from XX 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 (λ _ → hlevel 1)
            (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 (λ _ → hlevel 1)
            (ap fst (f⊥! _ .paths (x .fst , x .snd , !-unique₂ T _ _)))

As a passing observation we note that if f⊥Xf {\mathrel{\bot}}X and X≅YX \cong Y, then f⊥Yf {\mathrel{\bot}}Y. 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 ff 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 r⊣ι:D⇄Cr \dashv \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: ηx:x→ιr(x)\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 ff such that r(f)r(f) is an isomorphism is orthogonal to every object in the subcategory: f⊥ι(X)f {\mathrel{\bot}}\iota(X). Let f:a→bf : a \to b be inverted by rr, and XX be the object. Given a map a:a→ιXa : a \to \iota X,

    : ∀ {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 (λ _ → hlevel 1) (h≡k factors factors′) }
      module rf = rf-inv
      module η⁻¹ {a} = (is-reflective→unit-G-is-iso r⊣ι ι-ff {a})

Observe that, since r⊣ιr \dashv \iota is a reflective subcategory, every unit morphism ηιX\eta_{\iota X} is an isomorphism; We define a morphism b:ιr(A)→ιXb : \iota r(A) \to \iota X as the composite

ιr(A)→ιr(a)ιrι(X)→η−1ι(X), \iota r(A) {\xrightarrow{\iota r(a)}} \iota r \iota(X) {\xrightarrow{\eta^{-1}}} \iota(X)\text{,}

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

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

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

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

B→ηιr(B)→ι(r(f)−1)ιr(A)→bι(X), B {\xrightarrow{\eta}} \iota r(B) {\xrightarrow{\iota(r(f)^{-1})}} \iota r(A) {\xrightarrow{b}} \iota(X)\text{,}

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

      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 hf=a=kfhf = a = kf, note that we must have r(h)=r(k)r(h) = r(k) (since r(f)r(f) is invertible, it is epic); But then we have

ηιXh=ιr(h)η=ιr(k)η=ηιXk, \eta_{\iota X} h = \iota r(h) \eta = \iota r(k) \eta = \eta_{\iota X} k\text{,}

and since ηιX\eta_{\iota X} is an isomorphism, thus monic, we have h=kh = k.

      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 XX 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 f⊥ι(X)f {\mathrel{\bot}}\iota(X) if ff is invertible by the reflection functor, and we know that η\eta is invertible by the reflection functor; It remains to replace ι(X)\iota(X) with any object for which η\eta 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↩︎