module Cat.Morphism.Orthogonal where

# Orthogonal maps🔗

A pair of maps
$f:a→b$
and
$g:ctod$
are called **orthogonal**, written
$f⊥g$^{1}, if for every
$u,v$
fitting into a commutative diagram like

the space of arrows $c→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⊥X,$ and an object being orthogonal to a map $Y⊥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))

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
$C$
has enough co/limits, being orthogonal to an object is equivalent to
being orthogonal to an object. For example,
$f⊥X$
iff.
$f⊥!_{X},$
where
$!_{X}:X→1$
is the unique map from
$X$
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 $f⊥X$ and $X≅Y,$ then $f⊥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

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

A slightly more interesting lemma is that, if $f$ 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🔗

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 = Cr C module D = Cr D module ι = Func ι module r = Func r module rι = Func (r F∘ ι) module ιr = Func (ι F∘ r) open _⊣_ r⊣ι

Let $r⊣ι:D⇄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)$ 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⊥ι(X).$ Let $f:a→b$ be inverted by $r,$ and $X$ be the object. Given a map $a:a→ιX,$

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 $r⊣ι$ is a reflective subcategory, every unit morphism $η_{ιX}$ is an isomorphism; We define a morphism $b:ιr(A)→ιX$ as the composite

$ιr(A)ιr(a) ιrι(X)η_{−1} ι(X),$b : C.Hom (ι.₀ (r.₀ A)) (ι.₀ X) b = η⁻¹.inv C.∘ ι.₁ (r.₁ a→x)

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

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.$

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

$η_{ιX}h=ιr(h)η=ιr(k)η=η_{ιX}k,$and since $η_{ιX}$ is an isomorphism, thus monic, we have $h=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 ≡⟨ 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 → 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
$f⊥ι(X)$
if
$f$
is invertible by the reflection functor, and we know that
$η$
is invertible by the reflection functor; It remains to replace
$ι(X)$
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))

Though hang tight for a note on formalised notation↩︎

## References

- Borceux, Francis. 1994.
*Handbook of Categorical Algebra*. Vol. 1. Encyclopedia of Mathematics and Its Applications. Cambridge University Press. https://doi.org/10.1017/CBO9780511525858.