module Cat.Displayed.Morphism.Duality {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where
private module ℬ = Cat.Morphism ℬ module ℬ^op = Cat.Morphism (ℬ ^op) module ℰ = Cat.Displayed.Morphism ℰ module ℰ^op = Cat.Displayed.Morphism (ℰ ^total-op) open Displayed ℰ open Cat.Morphism.Duality ℬ open Cat.Displayed.Reasoning ℰ open Cat.Displayed.Morphism private variable a b c d : ℬ.Ob f g : ℬ.Hom a b a′ b′ c′ d′ : Ob[ a ] f′ g′ : Hom[ f ] a′ b′
Duality of Displayed Morphism Classes🔗
In this file we prove that morphism classes in a displayed category correspond to their duals in the total opposite displayed category. There is even less mathematical content here than the non-displayed case, just mountains of boilerplate.
We start by showing that displayed monos and epis are dual.
co-mono[]→epi[] : ∀ {f : a ℬ^op.↪ b} → a′ ℰ^op.↪[ f ] b′ → b′ ℰ.↠[ co-mono→epi f ] a′ co-mono[]→epi[] f .mor′ = ℰ^op.mor′ f co-mono[]→epi[] f .epic′ = ℰ^op.monic′ f epi[]→co-mono[] : ∀ {f : b ℬ.↠ a} → b′ ℰ.↠[ f ] a′ → a′ ℰ^op.↪[ epi→co-mono f ] b′ epi[]→co-mono[] f .mor′ = ℰ.mor′ f epi[]→co-mono[] f .monic′ = ℰ.epic′ f co-epi[]→mono[] : ∀ {f : a ℬ^op.↠ b} → a′ ℰ^op.↠[ f ] b′ → b′ ℰ.↪[ co-epi→mono f ] a′ co-epi[]→mono[] f .mor′ = ℰ^op.mor′ f co-epi[]→mono[] f .monic′ = ℰ^op.epic′ f mono[]→co-epi[] : ∀ {f : b ℬ.↪ a} → b′ ℰ.↪[ f ] a′ → a′ ℰ^op.↠[ mono→co-epi f ] b′ mono[]→co-epi[] f .mor′ = ℰ.mor′ f mono[]→co-epi[] f .epic′ = ℰ.monic′ f
Next, we show the same for weak monos and weak epis.
weak-mono→weak-co-epi : ∀ {f : ℬ.Hom b a} → ℰ.weak-mono-over f b′ a′ → ℰ^op.weak-epi-over f a′ b′ weak-mono→weak-co-epi f .mor′ = ℰ.mor′ f weak-mono→weak-co-epi f .weak-epic = ℰ.weak-monic f weak-co-epi→weak-mono : ∀ {f : ℬ.Hom b a} → ℰ^op.weak-epi-over f a′ b′ → ℰ.weak-mono-over f b′ a′ weak-co-epi→weak-mono f .mor′ = ℰ^op.mor′ f weak-co-epi→weak-mono f .weak-monic = ℰ^op.weak-epic f weak-epi→weak-co-mono : ∀ {f : ℬ.Hom b a} → ℰ.weak-epi-over f b′ a′ → ℰ^op.weak-mono-over f a′ b′ weak-epi→weak-co-mono f .mor′ = ℰ.mor′ f weak-epi→weak-co-mono f .weak-monic = ℰ.weak-epic f weak-co-mono→weak-epi : ∀ {f : ℬ.Hom b a} → ℰ^op.weak-mono-over f a′ b′ → ℰ.weak-epi-over f b′ a′ weak-co-mono→weak-epi f .mor′ = ℰ^op.mor′ f weak-co-mono→weak-epi f .weak-epic = ℰ^op.weak-monic f
Next, sections and retractions.
co-section[]→retract[] : ∀ {s : ℬ^op.has-section f} → ℰ^op.has-section[ s ] f′ → ℰ.has-retract[ co-section→retract s ] f′ co-section[]→retract[] f .retract′ = ℰ^op.section′ f co-section[]→retract[] f .is-retract′ = ℰ^op.is-section′ f retract[]→co-section[] : ∀ {r : ℬ.has-retract f} → ℰ.has-retract[ r ] f′ → ℰ^op.has-section[ retract→co-section r ] f′ retract[]→co-section[] f .section′ = ℰ.retract′ f retract[]→co-section[] f .is-section′ = ℰ.is-retract′ f co-retract[]→section[] : ∀ {r : ℬ^op.has-retract f} → ℰ^op.has-retract[ r ] f′ → ℰ.has-section[ co-retract→section r ] f′ co-retract[]→section[] f .section′ = ℰ^op.retract′ f co-retract[]→section[] f .is-section′ = ℰ^op.is-retract′ f section[]→co-retract[] : ∀ {s : ℬ.has-section f} → ℰ.has-section[ s ] f′ → ℰ^op.has-retract[ section→co-retract s ] f′ section[]→co-retract[] f .retract′ = ℰ.section′ f section[]→co-retract[] f .is-retract′ = ℰ.is-section′ f
We handle vertical sections and retract separately.
vertical-co-section→vertical-retract : ℰ^op.has-section↓ f′ → ℰ.has-retract↓ f′ vertical-co-section→vertical-retract f .retract′ = ℰ^op.section′ f vertical-co-section→vertical-retract f .is-retract′ = cast[] (ℰ^op.is-section′ f) vertical-retract→vertical-co-section : ℰ.has-retract↓ f′ → ℰ^op.has-section↓ f′ vertical-retract→vertical-co-section f .section′ = ℰ.retract′ f vertical-retract→vertical-co-section f .is-section′ = cast[] (ℰ.is-retract′ f) vertical-co-retract→vertical-section : ℰ^op.has-retract↓ f′ → ℰ.has-section↓ f′ vertical-co-retract→vertical-section f .section′ = ℰ^op.retract′ f vertical-co-retract→vertical-section f .is-section′ = cast[] (ℰ^op.is-retract′ f) vertical-section→vertical-co-retract : ℰ.has-section↓ f′ → ℰ^op.has-retract↓ f′ vertical-section→vertical-co-retract f .retract′ = ℰ.section′ f vertical-section→vertical-co-retract f .is-retract′ = cast[] (ℰ.is-section′ f)
Now, on to self-duality for invertible morphisms.
co-inverses[]→inverses[] : {i : ℬ^op.Inverses f g} → ℰ^op.Inverses[ i ] f′ g′ → ℰ.Inverses[ co-inverses→inverses i ] f′ g′ co-inverses[]→inverses[] i .Inverses[_].invl′ = ℰ^op.Inverses[_].invr′ i co-inverses[]→inverses[] i .Inverses[_].invr′ = ℰ^op.Inverses[_].invl′ i inverses[]→co-inverses[] : {i : ℬ.Inverses f g} → ℰ.Inverses[ i ] f′ g′ → ℰ^op.Inverses[ inverses→co-inverses i ] f′ g′ inverses[]→co-inverses[] i .Inverses[_].invl′ = ℰ.Inverses[_].invr′ i inverses[]→co-inverses[] i .Inverses[_].invr′ = ℰ.Inverses[_].invl′ i co-invertible[]→invertible[] : {i : ℬ^op.is-invertible f} → ℰ^op.is-invertible[ i ] f′ → ℰ.is-invertible[ co-invertible→invertible i ] f′ co-invertible[]→invertible[] i .is-invertible[_].inv′ = ℰ^op.is-invertible[_].inv′ i co-invertible[]→invertible[] i .is-invertible[_].inverses′ = co-inverses[]→inverses[] (ℰ^op.is-invertible[_].inverses′ i) invertible[]→co-invertible[] : {i : ℬ.is-invertible f} → ℰ.is-invertible[ i ] f′ → ℰ^op.is-invertible[ invertible→co-invertible i ] f′ invertible[]→co-invertible[] i .is-invertible[_].inv′ = ℰ.is-invertible[_].inv′ i invertible[]→co-invertible[] i .is-invertible[_].inverses′ = inverses[]→co-inverses[] (ℰ.is-invertible[_].inverses′ i) co-iso[]→iso[] : {f : a ℬ^op.≅ b} → a′ ℰ^op.≅[ f ] b′ → b′ ℰ.≅[ co-iso→iso f ] a′ co-iso[]→iso[] f .to′ = ℰ^op.to′ f co-iso[]→iso[] f .from′ = ℰ^op.from′ f co-iso[]→iso[] f .inverses′ = co-inverses[]→inverses[] (ℰ^op.inverses′ f) iso[]→co-iso[] : {f : b ℬ.≅ a} → b′ ℰ.≅[ f ] a′ → a′ ℰ^op.≅[ iso→co-iso f ] b′ iso[]→co-iso[] f .to′ = ℰ.to′ f iso[]→co-iso[] f .from′ = ℰ.from′ f iso[]→co-iso[] f .inverses′ = inverses[]→co-inverses[] (ℰ.inverses′ f)
We handle the case of vertical isos separately, as the dual of the identity iso isn’t definitionally the identity iso.
vertical-co-invertible→vertical-invertible : ℰ^op.is-invertible↓ f′ → ℰ.is-invertible↓ f′ vertical-co-invertible→vertical-invertible f = ℰ.make-invertible↓ (ℰ^op.is-invertible[_].inv′ f) (cast[] (ℰ^op.is-invertible[_].invr′ f)) (cast[] (ℰ^op.is-invertible[_].invl′ f)) vertical-invertible→vertical-co-invertible : ℰ.is-invertible↓ f′ → ℰ^op.is-invertible↓ f′ vertical-invertible→vertical-co-invertible f = ℰ^op.make-invertible↓ (ℰ.is-invertible[_].inv′ f) (cast[] (ℰ.is-invertible[_].invr′ f)) (cast[] (ℰ.is-invertible[_].invl′ f)) vertical-co-iso→vertical-iso : a′ ℰ^op.≅↓ b′ → b′ ℰ.≅↓ a′ vertical-co-iso→vertical-iso f = ℰ.make-vertical-iso (ℰ^op.to′ f) (ℰ^op.from′ f) (cast[] (ℰ^op.invr′ f)) (cast[] (ℰ^op.invl′ f)) vertical-iso→vertical-co-iso : a′ ℰ.≅↓ b′ → b′ ℰ^op.≅↓ a′ vertical-iso→vertical-co-iso f = ℰ^op.make-vertical-iso (ℰ.to′ f) (ℰ.from′ f) (cast[] (ℰ.invr′ f)) (cast[] (ℰ.invl′ f))