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

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.

  object-orthogonal-!-orthogonal
    : βˆ€ {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
    where
      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 β†’ C.is-invertible f
  self-orthogonalβ†’is-iso f fβŠ₯f =
    C.make-invertible (gpq .fst) (gpq .snd .snd) (gpq .snd .fst)
    where
      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

  in-subcategory→orthogonal-to-inverted
    : βˆ€ {X} {a b} {f : C.Hom a b} β†’ D.is-invertible (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') }
    where
      module rf = D.is-invertible rf-inv
      module η⁻¹ {a} = C.is-invertible (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 (unit.is-natural _ _ _)) βˆ™ 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 (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 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 β‰‘βŸ¨ 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 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 β†’ mβŠ₯o 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 .Precategory.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 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.

  in-subcategory→orthogonal-to-ηs
    : βˆ€ {X B} β†’ C.is-invertible (unit.Ξ· X) β†’ mβŠ₯o C (unit.Ξ· B) X
  in-subcategory→orthogonal-to-ηs inv =
    mβŠ₯-iso C (unit.Ξ· _) (C.invertibleβ†’iso _ (C.is-invertible-inverse inv))
      (in-subcategory→orthogonal-to-inverted
        (is-reflectiveβ†’F-unit-is-iso r⊣ι ΞΉ-ff))

  1. Though hang tight for a note on formalised notationβ†©οΈŽ


References