open import 1Lab.Prelude hiding (_β_ ; id ; _βͺ_) open import Cat.Solver open import Cat.Base module Cat.Morphism {o h} (C : Precategory o h) where
Morphismsπ
This module defines the three most important classes of morphisms that can be found in a category: monomorphisms, epimorphisms, and isomorphisms.
Monosπ
A morphism is said to be monic when it is left-cancellable. A monomorphism from to , written , is a monic morphism.
is-monic : Hom a b β Type _ is-monic {a = a} f = β {c} β (g h : Hom c a) β f β g β‘ f β h β g β‘ h is-monic-is-prop : β {a b} (f : Hom a b) β is-prop (is-monic f) is-monic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i record _βͺ_ (a b : Ob) : Type (o β h) where field mor : Hom a b monic : is-monic mor
Conversely, a morphism is said to be epic when it is right-cancellable. An epimorphism from to , written , is an epic morphism.
Episπ
is-epic : Hom a b β Type _ is-epic {b = b} f = β {c} β (g h : Hom b c) β g β f β‘ h β f β g β‘ h is-epic-is-prop : β {a b} (f : Hom a b) β is-prop (is-epic f) is-epic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i record _β _ (a b : Ob) : Type (o β h) where field mor : Hom a b monic : is-epic mor
Isosπ
Maps and are inverses when we have and both equal to the identity. A map is invertible (or is an isomorphism) when there exists a for which and are inverses. An isomorphism is a choice of map , together with a specified inverse.
record Inverses (f : Hom a b) (g : Hom b a) : Type h where field invl : f β g β‘ id invr : g β f β‘ id open Inverses record is-invertible (f : Hom a b) : Type h where field inv : Hom b a inverses : Inverses f inv open Inverses inverses public op : is-invertible inv op .inv = f op .inverses .Inverses.invl = invr inverses op .inverses .Inverses.invr = invl inverses record _β _ (a b : Ob) : Type h where field to : Hom a b from : Hom b a inverses : Inverses to from open Inverses inverses public open _β _ public
A given map is invertible in at most one way: If you have with two inverses and , then not only are equal, but the witnesses of these equalities are irrelevant.
Inverses-are-prop : β {f : Hom a b} {g : Hom b a} β is-prop (Inverses f g) Inverses-are-prop x y i .Inverses.invl = Hom-set _ _ _ _ (x .invl) (y .invl) i Inverses-are-prop x y i .Inverses.invr = Hom-set _ _ _ _ (x .invr) (y .invr) i is-invertible-is-prop : β {f : Hom a b} β is-prop (is-invertible f) is-invertible-is-prop {a = a} {b = b} {f = f} g h = p where module g = is-invertible g module h = is-invertible h gβ‘h : g.inv β‘ h.inv gβ‘h = g.inv β‘β¨ sym (idr _) β apβ _β_ refl (sym h.invl) β©β‘ g.inv β f β h.inv β‘β¨ assoc _ _ _ Β·Β· apβ _β_ g.invr refl Β·Β· idl _ β©β‘ h.inv β p : g β‘ h p i .is-invertible.inv = gβ‘h i p i .is-invertible.inverses = is-propβpathp (Ξ» i β Inverses-are-prop {g = gβ‘h i}) g.inverses h.inverses i
We note that the identity morphism is always iso, and that isos compose:
id-iso : a β a id-iso = make-iso id id (idl _) (idl _) Inverses-β : {f : Hom a b} {fβ»ΒΉ : Hom b a} {g : Hom b c} {gβ»ΒΉ : Hom c b} β Inverses f fβ»ΒΉ β Inverses g gβ»ΒΉ β Inverses (g β f) (fβ»ΒΉ β gβ»ΒΉ) Inverses-β {f = f} {fβ»ΒΉ} {g} {gβ»ΒΉ} finv ginv = record { invl = l ; invr = r } where module finv = Inverses finv module ginv = Inverses ginv abstract l : (g β f) β fβ»ΒΉ β gβ»ΒΉ β‘ id l = (g β f) β fβ»ΒΉ β gβ»ΒΉ β‘β¨ solve C β©β‘ g β (f β fβ»ΒΉ) β gβ»ΒΉ β‘β¨ (Ξ» i β g β finv.invl i β gβ»ΒΉ) β©β‘ g β id β gβ»ΒΉ β‘β¨ solve C β©β‘ g β gβ»ΒΉ β‘β¨ ginv.invl β©β‘ id β r : (fβ»ΒΉ β gβ»ΒΉ) β g β f β‘ id r = (fβ»ΒΉ β gβ»ΒΉ) β g β f β‘β¨ solve C β©β‘ fβ»ΒΉ β (gβ»ΒΉ β g) β f β‘β¨ (Ξ» i β fβ»ΒΉ β ginv.invr i β f) β©β‘ fβ»ΒΉ β id β f β‘β¨ solve C β©β‘ fβ»ΒΉ β f β‘β¨ finv.invr β©β‘ id β _βIso_ : a β b β b β c β a β c (f βIso g) .to = g .to β f .to (f βIso g) .from = f .from β g .from (f βIso g) .inverses = Inverses-β (f .inverses) (g .inverses) _Isoβ»ΒΉ : a β b β b β a (f Isoβ»ΒΉ) .to = f .from (f Isoβ»ΒΉ) .from = f .to (f Isoβ»ΒΉ) .inverses .invl = f .inverses .invr (f Isoβ»ΒΉ) .inverses .invr = f .inverses .invl
We also note that invertible morphisms are both epic and monic.
invertibleβmonic : is-invertible f β is-monic f invertibleβmonic {f = f} invert g h p = g β‘Λβ¨ idl g β©β‘Λ id β g β‘Λβ¨ ap (_β g) (is-invertible.invr invert) β©β‘Λ (inv β f) β g β‘Λβ¨ assoc inv f g β©β‘Λ inv β (f β g) β‘β¨ ap (inv β_) p β©β‘ inv β (f β h) β‘β¨ assoc inv f h β©β‘ (inv β f) β h β‘β¨ ap (_β h) (is-invertible.invr invert) β©β‘ id β h β‘β¨ idl h β©β‘ h β where open is-invertible invert invertibleβepic : is-invertible f β is-epic f invertibleβepic {f = f} invert g h p = g β‘Λβ¨ idr g β©β‘Λ g β id β‘Λβ¨ ap (g β_) (is-invertible.invl invert) β©β‘Λ g β (f β inv) β‘β¨ assoc g f inv β©β‘ (g β f) β inv β‘β¨ ap (_β inv) p β©β‘ (h β f) β inv β‘Λβ¨ assoc h f inv β©β‘Λ h β (f β inv) β‘β¨ ap (h β_) (is-invertible.invl invert) β©β‘ h β id β‘β¨ idr h β©β‘ h β where open is-invertible invert