module Cat.Morphism.Duality {o โ} (๐ : Precategory o โ) where
private module ๐ = Cat.Morphism ๐ module ๐^op = Cat.Morphism (๐ ^op) private variable a b c d : ๐.Ob f g : ๐.Hom a b
Duality of morphism classes๐
In this file we prove that morphisms classes in a category correspond to their duals in the opposite category. There is very little interesting mathematical content in this file; it is pure boilerplate.
We start by showing that monos and epis are dual.
co-monoโepi : a ๐^op.โช b โ b ๐.โ a co-monoโepi f .Cat.Morphism.mor = ๐^op.mor f co-monoโepi f .Cat.Morphism.epic = ๐^op.monic f epiโco-mono : b ๐.โ a โ a ๐^op.โช b epiโco-mono f .Cat.Morphism.mor = ๐.mor f epiโco-mono f .Cat.Morphism.monic = ๐.epic f co-epiโmono : a ๐^op.โ b โ b ๐.โช a co-epiโmono f .Cat.Morphism.mor = ๐^op.mor f co-epiโmono f .Cat.Morphism.monic = ๐^op.epic f monoโco-epi : b ๐.โช a โ a ๐^op.โ b monoโco-epi f .Cat.Morphism.mor = ๐.mor f monoโco-epi f .Cat.Morphism.epic = ๐.monic f
Next, sections and retractions.
co-sectionโretract : ๐^op.has-section f โ ๐.has-retract f co-sectionโretract f .Cat.Morphism.retract = ๐^op.section f co-sectionโretract f .Cat.Morphism.is-retract = ๐^op.is-section f retractโco-section : ๐.has-retract f โ ๐^op.has-section f retractโco-section f .Cat.Morphism.section = ๐.retract f retractโco-section f .Cat.Morphism.is-section = ๐.is-retract f co-retractโsection : ๐^op.has-retract f โ ๐.has-section f co-retractโsection f .Cat.Morphism.section = ๐^op.retract f co-retractโsection f .Cat.Morphism.is-section = ๐^op.is-retract f sectionโco-retract : ๐.has-section f โ ๐^op.has-retract f sectionโco-retract f .Cat.Morphism.retract = ๐.section f sectionโco-retract f .Cat.Morphism.is-retract = ๐.is-section f
Next, we show that invertible morphisms are self-dual.
co-inversesโinverses : ๐^op.Inverses f g โ ๐.Inverses f g co-inversesโinverses i .Cat.Morphism.Inverses.invl = ๐^op.Inverses.invr i co-inversesโinverses i .Cat.Morphism.Inverses.invr = ๐^op.Inverses.invl i inversesโco-inverses : ๐.Inverses f g โ ๐^op.Inverses f g inversesโco-inverses i .Cat.Morphism.Inverses.invl = ๐.Inverses.invr i inversesโco-inverses i .Cat.Morphism.Inverses.invr = ๐.Inverses.invl i co-invertibleโinvertible : ๐^op.is-invertible f โ ๐.is-invertible f co-invertibleโinvertible i .Cat.Morphism.is-invertible.inv = ๐^op.is-invertible.inv i co-invertibleโinvertible i .Cat.Morphism.is-invertible.inverses = co-inversesโinverses (๐^op.is-invertible.inverses i) invertibleโco-invertible : ๐.is-invertible f โ ๐^op.is-invertible f invertibleโco-invertible i .Cat.Morphism.is-invertible.inv = ๐.is-invertible.inv i invertibleโco-invertible i .Cat.Morphism.is-invertible.inverses = inversesโco-inverses (๐.is-invertible.inverses i) co-isoโiso : a ๐^op.โ b โ b ๐.โ a co-isoโiso f .Cat.Morphism.to = ๐^op.to f co-isoโiso f .Cat.Morphism.from = ๐^op.from f co-isoโiso f .Cat.Morphism.inverses = co-inversesโinverses (๐^op.inverses f) isoโco-iso : b ๐.โ a โ a ๐^op.โ b isoโco-iso f .Cat.Morphism.to = ๐.to f isoโco-iso f .Cat.Morphism.from = ๐.from f isoโco-iso f .Cat.Morphism.inverses = inversesโco-inverses (๐.inverses f)