Grace/Cumulus/Category/MonoEpi.g17

Open in Workbench Download source

Imports

Isomorphism

Declarations

Source

1-- Monomorphisms, epimorphisms, and split morphisms2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Category.MonoEpi8import Isomorphism910-- A monomorphism is left cancellable, an epimorphism right cancellable.11predicate Monomorphism (C f : Set) :=12  f ∈ mor(C) ∧ (∀ u ∈ mor(C), ∀ v ∈ mor(C), dom(C)(f) = cod(C)(u) → dom(C)(f) = cod(C)(v) →13    comp(C)(f, u) = comp(C)(f, v) → u = v)1415predicate Epimorphism (C f : Set) :=16  f ∈ mor(C) ∧ (∀ u ∈ mor(C), ∀ v ∈ mor(C), dom(C)(u) = cod(C)(f) → dom(C)(v) = cod(C)(f) →17    comp(C)(u, f) = comp(C)(v, f) → u = v)1819predicate Bimorphism (C f : Set) :=20  Monomorphism(C, f) ∧ Epimorphism(C, f)2122notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis Monomorphism(C, f) for C.mor23notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis Epimorphism(C, f) for C.mor2425-- r is a retraction of f (a left inverse), s a section of f (a right26-- inverse).27predicate Retraction (C f r : Set) :=28  f ∈ mor(C) ∧ r ∈ mor(C) ∧ dom(C)(r) = cod(C)(f) ∧ cod(C)(r) = dom(C)(f) ∧ comp(C)(r, f) = id(C)(dom(C)(f))2930predicate SectionOf (C f s : Set) :=31  f ∈ mor(C) ∧ s ∈ mor(C) ∧ dom(C)(s) = cod(C)(f) ∧ cod(C)(s) = dom(C)(f) ∧ comp(C)(f, s) = id(C)(cod(C)(f))3233notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis Retraction(C, f, r) for C.mor34notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis SectionOf(C, f, s) for C.mor3536predicate SplitMonomorphism (C f : Set) :=37  ∃ r, Retraction(C, f, r)3839predicate SplitEpimorphism (C f : Set) :=40  ∃ s, SectionOf(C, f, s)4142theorem Monomorphism.morphism (C f : Set)43  requires mono : Monomorphism(C, f)44  shows f ∈ mor(C)45proof46  obtain ⟨fInM, cancel⟩ := mono47  exact fInM4849theorem Monomorphism.cancel (C f u v : Set)50  requires mono : Monomorphism(C, f)51  requires uInM : u ∈ mor(C)52  requires vInM : v ∈ mor(C)53  requires uComposable : dom(C)(f) = cod(C)(u)54  requires vComposable : dom(C)(f) = cod(C)(v)55  requires same : f ∘ u = f ∘ v56  shows u = v57proof58  obtain ⟨fInM, cancel⟩ := mono59  exact cancel with u, uInM, v, vInM, uComposable, vComposable, same6061theorem Epimorphism.morphism (C f : Set)62  requires epi : Epimorphism(C, f)63  shows f ∈ mor(C)64proof65  obtain ⟨fInM, cancel⟩ := epi66  exact fInM6768theorem Epimorphism.cancel (C f u v : Set)69  requires epi : Epimorphism(C, f)70  requires uInM : u ∈ mor(C)71  requires vInM : v ∈ mor(C)72  requires uComposable : dom(C)(u) = cod(C)(f)73  requires vComposable : dom(C)(v) = cod(C)(f)74  requires same : u ∘ f = v ∘ f75  shows u = v76proof77  obtain ⟨fInM, cancel⟩ := epi78  exact cancel with u, uInM, v, vInM, uComposable, vComposable, same7980theorem Bimorphism.mono (C f : Set)81  requires bi : Bimorphism(C, f)82  shows Monomorphism(C, f)83proof84  simp [Bimorphism]8586theorem Bimorphism.epi (C f : Set)87  requires bi : Bimorphism(C, f)88  shows Epimorphism(C, f)89proof90  simp [Bimorphism]9192theorem Monomorphism.id (C a : Set)93  requires category : Category(C)94  requires aInO : a ∈ obj(C)95  shows Monomorphism(C, id(C)(a))96proof97  have idInM := Category.id_closed with category, aInO98  have domId := Category.id_dom with category, aInO99  unfold Monomorphism100  refine ⟨idInM, ?_⟩101  intros u uInM v vInM uComposable vComposable same102  have uCod : cod(C)(u) = a by cc103  have vCod : cod(C)(v) = a by cc104  have unitU := Category.id_left_of_cod with category, uInM, uCod105  have unitV := Category.id_left_of_cod with category, vInM, vCod106  calc107    u = id(C)(a) ∘ u := by rw unitU108    _ = id(C)(a) ∘ v := same109    _ = v := unitV110111theorem Epimorphism.id (C a : Set)112  requires category : Category(C)113  requires aInO : a ∈ obj(C)114  shows Epimorphism(C, id(C)(a))115proof116  have idInM := Category.id_closed with category, aInO117  have codId := Category.id_cod with category, aInO118  unfold Epimorphism119  refine ⟨idInM, ?_⟩120  intros u uInM v vInM uComposable vComposable same121  have uDom : dom(C)(u) = a by cc122  have vDom : dom(C)(v) = a by cc123  have unitU := Category.id_right_of_dom with category, uInM, uDom124  have unitV := Category.id_right_of_dom with category, vInM, vDom125  calc126    u = u ∘ id(C)(a) := by rw unitU127    _ = v ∘ id(C)(a) := same128    _ = v := unitV129130section MonomorphismComposition131variable (C : Set)132hypothesis category : Category(C)133134theorem Monomorphism.comp (a b c : Set) (f : a ⟶ b) (g : b ⟶ c)135  requires gMono : Monomorphism(C, g)136  requires fMono : Monomorphism(C, f)137  shows Monomorphism(C, g ∘ f)138proof139  have gfHom : g ∘ f : a ⟶ c by synthesize140  unfold Monomorphism141  refine ⟨?_, ?_⟩142  . assumption143  intros u uInM v vInM uComposable vComposable same144  have uHom : u : dom(C)(u) ⟶ a := Morphism.of_dom_cod with *145  have vHom : v : dom(C)(v) ⟶ a := Morphism.of_dom_cod with *146  have fuHom : f ∘ u : dom(C)(u) ⟶ b by synthesize147  have fvHom : f ∘ v : dom(C)(v) ⟶ b by synthesize148  have inner : g ∘ (f ∘ u) = g ∘ (f ∘ v)149    calc150      g ∘ (f ∘ u) = (g ∘ f) ∘ u := by rw Category.assoc151      _ = (g ∘ f) ∘ v := same152      _ = g ∘ (f ∘ v) := by rw Category.assoc153  have cancelled : f ∘ u = f ∘ v := Monomorphism.cancel with gMono, inner, *154  exact Monomorphism.cancel with fMono, cancelled, *155156end MonomorphismComposition157158theorem Epimorphism.comp (C g f : Set)159  requires category : Category(C)160  requires gEpi : Epimorphism(C, g)161  requires fEpi : Epimorphism(C, f)162  requires composable : dom(C)(g) = cod(C)(f)163  shows Epimorphism(C, g ∘ f)164proof165  have gInM := Epimorphism.morphism with gEpi166  have fInM := Epimorphism.morphism with fEpi167  have gfInM := Category.comp_closed with category, gInM, fInM, composable168  have codGF := Category.comp_cod with category, gInM, fInM, composable169  unfold Epimorphism170  refine ⟨gfInM, ?_⟩171  intros u uInM v vInM uComposable vComposable same172  have ugComposable : dom(C)(u) = cod(C)(g) by cc173  have vgComposable : dom(C)(v) = cod(C)(g) by cc174  have assocU := Category.associative with175    category, uInM, gInM, fInM, ugComposable, composable176  have assocV := Category.associative with177    category, vInM, gInM, fInM, vgComposable, composable178  have ugInM := Category.comp_closed with category, uInM, gInM, ugComposable179  have vgInM := Category.comp_closed with category, vInM, gInM, vgComposable180  have domUG := Category.comp_dom with category, uInM, gInM, ugComposable181  have domVG := Category.comp_dom with category, vInM, gInM, vgComposable182  have ugfComposable : dom(C)(u ∘ g) = cod(C)(f) by cc183  have vgfComposable : dom(C)(v ∘ g) = cod(C)(f) by cc184  have inner : (u ∘ g) ∘ f = (v ∘ g) ∘ f185    calc186      (u ∘ g) ∘ f = u ∘ (g ∘ f) := assocU187      _ = v ∘ (g ∘ f) := same188      _ = (v ∘ g) ∘ f := by rw assocV189  have cancelled := Epimorphism.cancel with190    fEpi, ugInM, vgInM, ugfComposable, vgfComposable, inner191  exact Epimorphism.cancel with192    gEpi, uInM, vInM, ugComposable, vgComposable, cancelled193194-- If a composite is mono, so is its first factor; if it is epi, so is195-- its second factor.196theorem Monomorphism.of_comp (C g f : Set)197  requires category : Category(C)198  requires gInM : g ∈ mor(C)199  requires fInM : f ∈ mor(C)200  requires composable : dom(C)(g) = cod(C)(f)201  requires mono : Monomorphism(C, g ∘ f)202  shows Monomorphism(C, f)203proof204  have domGF := Category.comp_dom with category, gInM, fInM, composable205  unfold Monomorphism206  refine ⟨fInM, ?_⟩207  intros u uInM v vInM uComposable vComposable same208  have assocU := Category.associative with209    category, gInM, fInM, uInM, composable, uComposable210  have assocV := Category.associative with211    category, gInM, fInM, vInM, composable, vComposable212  have gfuComposable : dom(C)(g ∘ f) = cod(C)(u) by cc213  have gfvComposable : dom(C)(g ∘ f) = cod(C)(v) by cc214  have outer : (g ∘ f) ∘ u = (g ∘ f) ∘ v215    calc216      (g ∘ f) ∘ u = g ∘ (f ∘ u) := assocU217      _ = g ∘ (f ∘ v) := by rw same218      _ = (g ∘ f) ∘ v := by rw assocV219  exact Monomorphism.cancel with220    mono, uInM, vInM, gfuComposable, gfvComposable, outer221222theorem Epimorphism.of_comp (C g f : Set)223  requires category : Category(C)224  requires gInM : g ∈ mor(C)225  requires fInM : f ∈ mor(C)226  requires composable : dom(C)(g) = cod(C)(f)227  requires epi : Epimorphism(C, g ∘ f)228  shows Epimorphism(C, g)229proof230  have codGF := Category.comp_cod with category, gInM, fInM, composable231  unfold Epimorphism232  refine ⟨gInM, ?_⟩233  intros u uInM v vInM uComposable vComposable same234  have assocU := Category.associative with235    category, uInM, gInM, fInM, uComposable, composable236  have assocV := Category.associative with237    category, vInM, gInM, fInM, vComposable, composable238  have ugfComposable : dom(C)(u) = cod(C)(g ∘ f) by cc239  have vgfComposable : dom(C)(v) = cod(C)(g ∘ f) by cc240  have outer : u ∘ (g ∘ f) = v ∘ (g ∘ f)241    calc242      u ∘ (g ∘ f) = (u ∘ g) ∘ f := by rw assocU243      _ = (v ∘ g) ∘ f := by rw same244      _ = v ∘ (g ∘ f) := assocV245  exact Epimorphism.cancel with246    epi, uInM, vInM, ugfComposable, vgfComposable, outer247248theorem Retraction.morphism (C f r : Set)249  requires retraction : Retraction(C, f, r)250  shows f ∈ mor(C)251proof252  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction253  exact fInM254255theorem Retraction.inverse_morphism (C f r : Set)256  requires retraction : Retraction(C, f, r)257  shows r ∈ mor(C)258proof259  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction260  exact rInM261262theorem Retraction.law (C f r : Set)263  requires retraction : Retraction(C, f, r)264  shows r ∘ f = id(C)(dom(C)(f))265proof266  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction267  exact law268269theorem SectionOf.morphism (C f s : Set)270  requires section : SectionOf(C, f, s)271  shows f ∈ mor(C)272proof273  obtain ⟨fInM, sInM, domS, codS, law⟩ := section274  exact fInM275276theorem SectionOf.inverse_morphism (C f s : Set)277  requires section : SectionOf(C, f, s)278  shows s ∈ mor(C)279proof280  obtain ⟨fInM, sInM, domS, codS, law⟩ := section281  exact sInM282283theorem SectionOf.law (C f s : Set)284  requires section : SectionOf(C, f, s)285  shows f ∘ s = id(C)(cod(C)(f))286proof287  obtain ⟨fInM, sInM, domS, codS, law⟩ := section288  exact law289290-- A retraction of f is a morphism of which f is a section, and conversely.291theorem Retraction.section (C f r : Set)292  requires retraction : Retraction(C, f, r)293  shows SectionOf(C, r, f)294proof295  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction296  unfold SectionOf297  refine ⟨rInM, fInM, ?_, ?_, ?_⟩298  . cc299  . cc300  . cc301302theorem SectionOf.retraction (C f s : Set)303  requires section : SectionOf(C, f, s)304  shows Retraction(C, s, f)305proof306  obtain ⟨fInM, sInM, domS, codS, law⟩ := section307  unfold Retraction308  refine ⟨sInM, fInM, ?_, ?_, ?_⟩309  . cc310  . cc311  . cc312313theorem InversePair.retraction (C f g : Set)314  requires pair : InversePair(C, f, g)315  shows Retraction(C, f, g)316proof317  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair318  unfold Retraction319  refine ⟨fInM, gInM, domG, codG, leftLaw⟩320321theorem InversePair.section (C f g : Set)322  requires pair : InversePair(C, f, g)323  shows SectionOf(C, f, g)324proof325  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair326  unfold SectionOf327  refine ⟨fInM, gInM, domG, codG, rightLaw⟩328329theorem InversePair.of_retraction_section (C f g : Set)330  requires retraction : Retraction(C, f, g)331  requires section : SectionOf(C, f, g)332  shows InversePair(C, f, g)333proof334  obtain ⟨fInM, gInM, domG, codG, leftLaw⟩ := retraction335  have rightLaw := SectionOf.law with section336  unfold InversePair337  refine ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩338339theorem SplitMonomorphism.morphism (C f : Set)340  requires split : SplitMonomorphism(C, f)341  shows f ∈ mor(C)342proof343  obtain ⟨r, retraction⟩ := split344  exact Retraction.morphism with retraction345346theorem SplitEpimorphism.morphism (C f : Set)347  requires split : SplitEpimorphism(C, f)348  shows f ∈ mor(C)349proof350  obtain ⟨s, section⟩ := split351  exact SectionOf.morphism with section352353theorem SplitMonomorphism.of_retraction (C f r : Set)354  requires retraction : Retraction(C, f, r)355  shows SplitMonomorphism(C, f)356proof357  refine ⟨r, retraction⟩358359theorem SplitEpimorphism.of_section (C f s : Set)360  requires section : SectionOf(C, f, s)361  shows SplitEpimorphism(C, f)362proof363  refine ⟨s, section⟩364365theorem Isomorphism.split_mono (C f : Set)366  requires iso : Isomorphism(C, f)367  shows SplitMonomorphism(C, f)368proof369  obtain ⟨g, pair⟩ := iso370  have retraction := InversePair.retraction with pair371  exact SplitMonomorphism.of_retraction with retraction372373theorem Isomorphism.split_epi (C f : Set)374  requires iso : Isomorphism(C, f)375  shows SplitEpimorphism(C, f)376proof377  obtain ⟨g, pair⟩ := iso378  have section := InversePair.section with pair379  exact SplitEpimorphism.of_section with section380381-- Split monomorphisms are monomorphisms.382theorem Retraction.mono (C f r : Set)383  requires category : Category(C)384  requires retraction : Retraction(C, f, r)385  shows Monomorphism(C, f)386proof387  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction388  unfold Monomorphism389  refine ⟨fInM, ?_⟩390  intros u uInM v vInM uComposable vComposable same391  have unitU : id(C)(dom(C)(f)) ∘ u = u392    have unit := Category.left_unit with category, uInM393    rwa ← uComposable at unit394  have unitV : id(C)(dom(C)(f)) ∘ v = v395    have unit := Category.left_unit with category, vInM396    rwa ← vComposable at unit397  have assocU := Category.associative with398    category, rInM, fInM, uInM, domR, uComposable399  have assocV := Category.associative with400    category, rInM, fInM, vInM, domR, vComposable401  calc402    u = id(C)(dom(C)(f)) ∘ u := by rw unitU403    _ = (r ∘ f) ∘ u := by rw law404    _ = r ∘ (f ∘ u) := assocU405    _ = r ∘ (f ∘ v) := by rw same406    _ = (r ∘ f) ∘ v := by rw assocV407    _ = id(C)(dom(C)(f)) ∘ v := by rw law408    _ = v := unitV409410theorem SplitMonomorphism.mono (C f : Set)411  requires category : Category(C)412  requires split : SplitMonomorphism(C, f)413  shows Monomorphism(C, f)414proof415  obtain ⟨r, retraction⟩ := split416  exact Retraction.mono with category, retraction417418theorem SectionOf.epi (C f s : Set)419  requires category : Category(C)420  requires section : SectionOf(C, f, s)421  shows Epimorphism(C, f)422proof423  obtain ⟨fInM, sInM, domS, codS, law⟩ := section424  unfold Epimorphism425  refine ⟨fInM, ?_⟩426  intros u uInM v vInM uComposable vComposable same427  have unitU := Category.id_right_of_dom with category, uInM, uComposable428  have unitV := Category.id_right_of_dom with category, vInM, vComposable429  have fsComposable : dom(C)(f) = cod(C)(s) by cc430  have assocU := Category.associative with431    category, uInM, fInM, sInM, uComposable, fsComposable432  have assocV := Category.associative with433    category, vInM, fInM, sInM, vComposable, fsComposable434  calc435    u = u ∘ id(C)(cod(C)(f)) := by rw unitU436    _ = u ∘ (f ∘ s) := by rw law437    _ = (u ∘ f) ∘ s := by rw assocU438    _ = (v ∘ f) ∘ s := by rw same439    _ = v ∘ (f ∘ s) := assocV440    _ = v ∘ id(C)(cod(C)(f)) := by rw law441    _ = v := unitV442443theorem SplitEpimorphism.epi (C f : Set)444  requires category : Category(C)445  requires split : SplitEpimorphism(C, f)446  shows Epimorphism(C, f)447proof448  obtain ⟨s, section⟩ := split449  exact SectionOf.epi with category, section450451theorem Isomorphism.mono (C f : Set)452  requires category : Category(C)453  requires iso : Isomorphism(C, f)454  shows Monomorphism(C, f)455proof456  have split := Isomorphism.split_mono with iso457  exact SplitMonomorphism.mono with category, split458459theorem Isomorphism.epi (C f : Set)460  requires category : Category(C)461  requires iso : Isomorphism(C, f)462  shows Epimorphism(C, f)463proof464  have split := Isomorphism.split_epi with iso465  exact SplitEpimorphism.epi with category, split466467theorem Isomorphism.bimorphism (C f : Set)468  requires category : Category(C)469  requires iso : Isomorphism(C, f)470  shows Bimorphism(C, f)471proof472  have mono := Isomorphism.mono with category, iso473  have epi := Isomorphism.epi with category, iso474  unfold Bimorphism475  refine ⟨mono, epi⟩476477-- A split monomorphism that is an epimorphism is an isomorphism, and its478-- retraction is its inverse.479theorem Retraction.inverse_of_epi (C f r : Set)480  requires category : Category(C)481  requires retraction : Retraction(C, f, r)482  requires epi : Epimorphism(C, f)483  shows InversePair(C, f, r)484proof485  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction486  have codIn := Category.cod_closed with category, fInM487  have idInM := Category.id_closed with category, codIn488  have domId := Category.id_dom with category, codIn489  have frComposable : dom(C)(f) = cod(C)(r) by cc490  have frInM := Category.comp_closed with category, fInM, rInM, frComposable491  have domFR := Category.comp_dom with category, fInM, rInM, frComposable492  have assoc := Category.associative with493    category, fInM, rInM, fInM, frComposable, domR494  have rightF := Category.right_unit with category, fInM495  have leftF := Category.left_unit with category, fInM496  have frfComposable : dom(C)(f ∘ r) = cod(C)(f) by cc497  have same : (f ∘ r) ∘ f = id(C)(cod(C)(f)) ∘ f498    calc499      (f ∘ r) ∘ f = f ∘ (r ∘ f) := assoc500      _ = f ∘ id(C)(dom(C)(f)) := by rw law501      _ = f := rightF502      _ = id(C)(cod(C)(f)) ∘ f := by rw leftF503  have rightLaw := Epimorphism.cancel with504    epi, frInM, idInM, frfComposable, domId, same505  unfold InversePair506  refine ⟨fInM, rInM, domR, codR, law, rightLaw⟩507508theorem SplitMonomorphism.iso_of_epi (C f : Set)509  requires category : Category(C)510  requires split : SplitMonomorphism(C, f)511  requires epi : Epimorphism(C, f)512  shows Isomorphism(C, f)513proof514  obtain ⟨r, retraction⟩ := split515  have pair := Retraction.inverse_of_epi with category, retraction, epi516  exact Isomorphism.of_pair with pair517518theorem SectionOf.inverse_of_mono (C f s : Set)519  requires category : Category(C)520  requires section : SectionOf(C, f, s)521  requires mono : Monomorphism(C, f)522  shows InversePair(C, f, s)523proof524  obtain ⟨fInM, sInM, domS, codS, law⟩ := section525  have domIn := Category.dom_closed with category, fInM526  have idInM := Category.id_closed with category, domIn527  have codId := Category.id_cod with category, domIn528  have sfInM := Category.comp_closed with category, sInM, fInM, domS529  have codSF := Category.comp_cod with category, sInM, fInM, domS530  have fsComposable : dom(C)(f) = cod(C)(s) by cc531  have assoc := Category.associative with532    category, fInM, sInM, fInM, fsComposable, domS533  have rightF := Category.right_unit with category, fInM534  have leftF := Category.left_unit with category, fInM535  have fsfComposable : dom(C)(f) = cod(C)(s ∘ f) by cc536  have fidComposable : dom(C)(f) = cod(C)(id(C)(dom(C)(f))) by cc537  have same : f ∘ (s ∘ f) = f ∘ id(C)(dom(C)(f))538    calc539      f ∘ (s ∘ f) = (f ∘ s) ∘ f := by rw assoc540      _ = id(C)(cod(C)(f)) ∘ f := by rw law541      _ = f := leftF542      _ = f ∘ id(C)(dom(C)(f)) := by rw rightF543  have leftLaw := Monomorphism.cancel with544    mono, sfInM, idInM, fsfComposable, fidComposable, same545  unfold InversePair546  refine ⟨fInM, sInM, domS, codS, leftLaw, law⟩547548theorem SplitEpimorphism.iso_of_mono (C f : Set)549  requires category : Category(C)550  requires split : SplitEpimorphism(C, f)551  requires mono : Monomorphism(C, f)552  shows Isomorphism(C, f)553proof554  obtain ⟨s, section⟩ := split555  have pair := SectionOf.inverse_of_mono with category, section, mono556  exact Isomorphism.of_pair with pair557558-- Split monomorphisms compose, and a first factor of a split mono is one.559theorem Retraction.comp (C g r f q : Set)560  requires category : Category(C)561  requires gRetraction : Retraction(C, g, r)562  requires fRetraction : Retraction(C, f, q)563  requires composable : dom(C)(g) = cod(C)(f)564  shows Retraction(C, g ∘ f, q ∘ r)565proof566  obtain ⟨gInM, rInM, domR, codR, rLaw⟩ := gRetraction567  obtain ⟨fInM, qInM, domQ, codQ, qLaw⟩ := fRetraction568  have qrComposable : dom(C)(q) = cod(C)(r) by cc569  have gfInM := Category.comp_closed with category, gInM, fInM, composable570  have qrInM := Category.comp_closed with category, qInM, rInM, qrComposable571  have domGF := Category.comp_dom with category, gInM, fInM, composable572  have codGF := Category.comp_cod with category, gInM, fInM, composable573  have domQR := Category.comp_dom with category, qInM, rInM, qrComposable574  have codQR := Category.comp_cod with category, qInM, rInM, qrComposable575  have fCod : cod(C)(f) = dom(C)(g) by cc576  have unitF := Category.id_left_of_cod with category, fInM, fCod577  have rgfComposable : dom(C)(r) = cod(C)(g ∘ f) by cc578  have assocOne := Category.associative with579    category, qInM, rInM, gfInM, qrComposable, rgfComposable580  have assocTwo := Category.associative with581    category, rInM, gInM, fInM, domR, composable582  unfold Retraction583  refine ⟨gfInM, qrInM, ?_, ?_, ?_⟩584  . cc585  . cc586  . calc587      (q ∘ r) ∘ (g ∘ f) = q ∘ (r ∘ (g ∘ f)) := assocOne588      _ = q ∘ ((r ∘ g) ∘ f) := by rw assocTwo589      _ = q ∘ (id(C)(dom(C)(g)) ∘ f) := by rw rLaw590      _ = q ∘ f := by rw unitF591      _ = id(C)(dom(C)(f)) := qLaw592      _ = id(C)(dom(C)(g ∘ f)) := by rw domGF593594theorem SplitMonomorphism.comp (C g f : Set)595  requires category : Category(C)596  requires gSplit : SplitMonomorphism(C, g)597  requires fSplit : SplitMonomorphism(C, f)598  requires composable : dom(C)(g) = cod(C)(f)599  shows SplitMonomorphism(C, g ∘ f)600proof601  obtain ⟨r, gRetraction⟩ := gSplit602  obtain ⟨q, fRetraction⟩ := fSplit603  have retraction := Retraction.comp with604    category, gRetraction, fRetraction, composable605  exact SplitMonomorphism.of_retraction with retraction606607theorem Retraction.of_comp (C g f r : Set)608  requires category : Category(C)609  requires gInM : g ∈ mor(C)610  requires fInM : f ∈ mor(C)611  requires composable : dom(C)(g) = cod(C)(f)612  requires retraction : Retraction(C, g ∘ f, r)613  shows Retraction(C, f, r ∘ g)614proof615  obtain ⟨gfInM, rInM, domR, codR, law⟩ := retraction616  have domGF := Category.comp_dom with category, gInM, fInM, composable617  have codGF := Category.comp_cod with category, gInM, fInM, composable618  have rgComposable : dom(C)(r) = cod(C)(g) by cc619  have rgInM := Category.comp_closed with category, rInM, gInM, rgComposable620  have domRG := Category.comp_dom with category, rInM, gInM, rgComposable621  have codRG := Category.comp_cod with category, rInM, gInM, rgComposable622  have assoc := Category.associative with623    category, rInM, gInM, fInM, rgComposable, composable624  unfold Retraction625  refine ⟨fInM, rgInM, ?_, ?_, ?_⟩626  . cc627  . cc628  . calc629      (r ∘ g) ∘ f = r ∘ (g ∘ f) := assoc630      _ = id(C)(dom(C)(g ∘ f)) := law631      _ = id(C)(dom(C)(f)) := by rw domGF632633theorem SplitMonomorphism.of_comp (C g f : Set)634  requires category : Category(C)635  requires gInM : g ∈ mor(C)636  requires fInM : f ∈ mor(C)637  requires composable : dom(C)(g) = cod(C)(f)638  requires split : SplitMonomorphism(C, g ∘ f)639  shows SplitMonomorphism(C, f)640proof641  obtain ⟨r, retraction⟩ := split642  have factor := Retraction.of_comp with643    category, gInM, fInM, composable, retraction644  exact SplitMonomorphism.of_retraction with factor645646-- Split epimorphisms compose, and a second factor of a split epi is one.647theorem SectionOf.comp (C g s f t : Set)648  requires category : Category(C)649  requires gSection : SectionOf(C, g, s)650  requires fSection : SectionOf(C, f, t)651  requires composable : dom(C)(g) = cod(C)(f)652  shows SectionOf(C, g ∘ f, t ∘ s)653proof654  obtain ⟨gInM, sInM, domS, codS, sLaw⟩ := gSection655  obtain ⟨fInM, tInM, domT, codT, tLaw⟩ := fSection656  have tsComposable : dom(C)(t) = cod(C)(s) by cc657  have gfInM := Category.comp_closed with category, gInM, fInM, composable658  have tsInM := Category.comp_closed with category, tInM, sInM, tsComposable659  have domGF := Category.comp_dom with category, gInM, fInM, composable660  have codGF := Category.comp_cod with category, gInM, fInM, composable661  have domTS := Category.comp_dom with category, tInM, sInM, tsComposable662  have codTS := Category.comp_cod with category, tInM, sInM, tsComposable663  have sCod : cod(C)(s) = cod(C)(f) by cc664  have unitS := Category.id_left_of_cod with category, sInM, sCod665  have ftsComposable : dom(C)(f) = cod(C)(t ∘ s) by cc666  have assocOne := Category.associative with667    category, gInM, fInM, tsInM, composable, ftsComposable668  have ftComposable : dom(C)(f) = cod(C)(t) by cc669  have assocTwo := Category.associative with670    category, fInM, tInM, sInM, ftComposable, tsComposable671  unfold SectionOf672  refine ⟨gfInM, tsInM, ?_, ?_, ?_⟩673  . cc674  . cc675  . calc676      (g ∘ f) ∘ (t ∘ s) = g ∘ (f ∘ (t ∘ s)) := assocOne677      _ = g ∘ ((f ∘ t) ∘ s) := by rw assocTwo678      _ = g ∘ (id(C)(cod(C)(f)) ∘ s) := by rw tLaw679      _ = g ∘ s := by rw unitS680      _ = id(C)(cod(C)(g)) := sLaw681      _ = id(C)(cod(C)(g ∘ f)) := by rw codGF682683theorem SplitEpimorphism.comp (C g f : Set)684  requires category : Category(C)685  requires gSplit : SplitEpimorphism(C, g)686  requires fSplit : SplitEpimorphism(C, f)687  requires composable : dom(C)(g) = cod(C)(f)688  shows SplitEpimorphism(C, g ∘ f)689proof690  obtain ⟨s, gSection⟩ := gSplit691  obtain ⟨t, fSection⟩ := fSplit692  have section := SectionOf.comp with category, gSection, fSection, composable693  exact SplitEpimorphism.of_section with section694695theorem SectionOf.of_comp (C g f s : Set)696  requires category : Category(C)697  requires gInM : g ∈ mor(C)698  requires fInM : f ∈ mor(C)699  requires composable : dom(C)(g) = cod(C)(f)700  requires section : SectionOf(C, g ∘ f, s)701  shows SectionOf(C, g, f ∘ s)702proof703  obtain ⟨gfInM, sInM, domS, codS, law⟩ := section704  have domGF := Category.comp_dom with category, gInM, fInM, composable705  have codGF := Category.comp_cod with category, gInM, fInM, composable706  have fsComposable : dom(C)(f) = cod(C)(s) by cc707  have fsInM := Category.comp_closed with category, fInM, sInM, fsComposable708  have domFS := Category.comp_dom with category, fInM, sInM, fsComposable709  have codFS := Category.comp_cod with category, fInM, sInM, fsComposable710  have assoc := Category.associative with711    category, gInM, fInM, sInM, composable, fsComposable712  unfold SectionOf713  refine ⟨gInM, fsInM, ?_, ?_, ?_⟩714  . cc715  . cc716  . calc717      g ∘ (f ∘ s) = (g ∘ f) ∘ s := by rw assoc718      _ = id(C)(cod(C)(g ∘ f)) := law719      _ = id(C)(cod(C)(g)) := by rw codGF720721theorem SplitEpimorphism.of_comp (C g f : Set)722  requires category : Category(C)723  requires gInM : g ∈ mor(C)724  requires fInM : f ∈ mor(C)725  requires composable : dom(C)(g) = cod(C)(f)726  requires split : SplitEpimorphism(C, g ∘ f)727  shows SplitEpimorphism(C, g)728proof729  obtain ⟨s, section⟩ := split730  have factor := SectionOf.of_comp with731    category, gInM, fInM, composable, section732  exact SplitEpimorphism.of_section with factor733734-- Monomorphisms and epimorphisms in hom-set form.735theorem Monomorphism.cancel_hom (C a b c f u v : Set)736  requires mono : Monomorphism(C, f)737  requires fHom : f ∈ hom(C, b, c)738  requires uHom : u ∈ hom(C, a, b)739  requires vHom : v ∈ hom(C, a, b)740  requires same : f ∘ u = f ∘ v741  shows u = v742proof743  have uInM := hom.in_morphisms with uHom744  have vInM := hom.in_morphisms with vHom745  have uComposable := hom.composable with fHom, uHom746  have vComposable := hom.composable with fHom, vHom747  exact Monomorphism.cancel with748    mono, uInM, vInM, uComposable, vComposable, same749750theorem Epimorphism.cancel_hom (C a b c f u v : Set)751  requires epi : Epimorphism(C, f)752  requires fHom : f ∈ hom(C, a, b)753  requires uHom : u ∈ hom(C, b, c)754  requires vHom : v ∈ hom(C, b, c)755  requires same : u ∘ f = v ∘ f756  shows u = v757proof758  have uInM := hom.in_morphisms with uHom759  have vInM := hom.in_morphisms with vHom760  have uComposable := hom.composable with uHom, fHom761  have vComposable := hom.composable with vHom, fHom762  exact Epimorphism.cancel with epi, uInM, vInM, uComposable, vComposable, same763