Grace/Cumulus/Category/Terminal.g17

Open in Workbench Download source

Imports

MonoEpi

Declarations

Source

1-- Initial, terminal, and zero objects2-- 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.Terminal8import MonoEpi910-- A terminal object receives exactly one morphism from each object, an11-- initial object sends exactly one morphism to each object.12predicate Terminal (C t : Set) :=13  t ∈ obj(C) ∧ (∀ a ∈ obj(C), ∃ f ∈ hom(C, a, t),14    ∀ g ∈ hom(C, a, t), g = f)1516predicate Initial (C i : Set) :=17  i ∈ obj(C) ∧ (∀ a ∈ obj(C), ∃ f ∈ hom(C, i, a),18    ∀ g ∈ hom(C, i, a), g = f)1920predicate ZeroObject (C z : Set) :=21  Initial(C, z) ∧ Terminal(C, z)2223theorem Terminal.object (C t : Set)24  requires terminal : Terminal(C, t)25  shows t ∈ obj(C)26proof27  obtain ⟨tInO, universal⟩ := terminal28  exact tInO2930theorem Terminal.exists_morphism (C t a : Set)31  requires terminal : Terminal(C, t)32  requires aInO : a ∈ obj(C)33  shows ∃ f ∈ hom(C, a, t), ∀ g ∈ hom(C, a, t), g = f34proof35  obtain ⟨tInO, universal⟩ := terminal36  exact universal with a, aInO3738theorem Terminal.unique_morphism (C t a f g : Set)39  requires terminal : Terminal(C, t)40  requires aInO : a ∈ obj(C)41  requires fHom : f ∈ hom(C, a, t)42  requires gHom : g ∈ hom(C, a, t)43  shows f = g44proof45  obtain ⟨u, uHom, unique⟩ := Terminal.exists_morphism with terminal, aInO46  have fEqual := unique with f, fHom47  have gEqual := unique with g, gHom48  cc4950theorem Initial.object (C i : Set)51  requires initial : Initial(C, i)52  shows i ∈ obj(C)53proof54  obtain ⟨iInO, universal⟩ := initial55  exact iInO5657theorem Initial.exists_morphism (C i a : Set)58  requires initial : Initial(C, i)59  requires aInO : a ∈ obj(C)60  shows ∃ f ∈ hom(C, i, a), ∀ g ∈ hom(C, i, a), g = f61proof62  obtain ⟨iInO, universal⟩ := initial63  exact universal with a, aInO6465theorem Initial.unique_morphism (C i a f g : Set)66  requires initial : Initial(C, i)67  requires aInO : a ∈ obj(C)68  requires fHom : f ∈ hom(C, i, a)69  requires gHom : g ∈ hom(C, i, a)70  shows f = g71proof72  obtain ⟨u, uHom, unique⟩ := Initial.exists_morphism with initial, aInO73  have fEqual := unique with f, fHom74  have gEqual := unique with g, gHom75  cc7677theorem ZeroObject.initial (C z : Set)78  requires zero : ZeroObject(C, z)79  shows Initial(C, z)80proof81  simp [ZeroObject]8283theorem ZeroObject.terminal (C z : Set)84  requires zero : ZeroObject(C, z)85  shows Terminal(C, z)86proof87  simp [ZeroObject]8889theorem ZeroObject.object (C z : Set)90  requires zero : ZeroObject(C, z)91  shows z ∈ obj(C)92proof93  have initial := ZeroObject.initial with zero94  exact Initial.object with initial9596-- The only endomorphism of a terminal or initial object is its identity.97theorem Terminal.endomorphism (C t f : Set)98  requires category : Category(C)99  requires terminal : Terminal(C, t)100  requires fHom : f ∈ hom(C, t, t)101  shows f = id(C)(t)102proof103  have tInO := Terminal.object with terminal104  have idHom := hom.id with category, tInO105  exact Terminal.unique_morphism with terminal, tInO, fHom, idHom106107theorem Initial.endomorphism (C i f : Set)108  requires category : Category(C)109  requires initial : Initial(C, i)110  requires fHom : f ∈ hom(C, i, i)111  shows f = id(C)(i)112proof113  have iInO := Initial.object with initial114  have idHom := hom.id with category, iInO115  exact Initial.unique_morphism with initial, iInO, fHom, idHom116117-- Terminal objects are isomorphic through a unique isomorphism.118theorem Terminal.inverse_pair (C t u f g : Set)119  requires category : Category(C)120  requires tTerminal : Terminal(C, t)121  requires uTerminal : Terminal(C, u)122  requires fHom : f ∈ hom(C, t, u)123  requires gHom : g ∈ hom(C, u, t)124  shows InversePair(C, f, g)125proof126  have gfHom := hom.comp with category, gHom, fHom127  have fgHom := hom.comp with category, fHom, gHom128  have gfId := Terminal.endomorphism with category, tTerminal, gfHom129  have fgId := Terminal.endomorphism with category, uTerminal, fgHom130  have fInM := hom.in_morphisms with fHom131  have gInM := hom.in_morphisms with gHom132  have domF := hom.dom with fHom133  have codF := hom.cod with fHom134  have domG := hom.dom with gHom135  have codG := hom.cod with gHom136  unfold InversePair137  refine ⟨fInM, gInM, ?_, ?_, ?_, ?_⟩138  . cc139  . cc140  . cc141  . cc142143theorem Terminal.isomorphism (C t u f : Set)144  requires category : Category(C)145  requires tTerminal : Terminal(C, t)146  requires uTerminal : Terminal(C, u)147  requires fHom : f ∈ hom(C, t, u)148  shows Isomorphism(C, f)149proof150  have tInO := Terminal.object with tTerminal151  obtain ⟨g, gHom, unique⟩ := Terminal.exists_morphism with152    tTerminal, uTerminal.left153  have pair := Terminal.inverse_pair with154    category, tTerminal, uTerminal, fHom, gHom155  exact Isomorphism.of_pair with pair156157theorem Terminal.isomorphic (C t u : Set)158  requires category : Category(C)159  requires tTerminal : Terminal(C, t)160  requires uTerminal : Terminal(C, u)161  shows Isomorphic(C, t, u)162proof163  have tInO := Terminal.object with tTerminal164  obtain ⟨f, fHom, unique⟩ := Terminal.exists_morphism with uTerminal, tInO165  have iso := Terminal.isomorphism with category, tTerminal, uTerminal, fHom166  exact Isomorphic.of_hom with fHom, iso167168theorem Terminal.unique_isomorphism (C t u f g : Set)169  requires tTerminal : Terminal(C, t)170  requires uTerminal : Terminal(C, u)171  requires fHom : f ∈ hom(C, t, u)172  requires gHom : g ∈ hom(C, t, u)173  shows f = g174proof175  have tInO := Terminal.object with tTerminal176  exact Terminal.unique_morphism with uTerminal, tInO, fHom, gHom177178theorem Initial.inverse_pair (C i j f g : Set)179  requires category : Category(C)180  requires iInitial : Initial(C, i)181  requires jInitial : Initial(C, j)182  requires fHom : f ∈ hom(C, i, j)183  requires gHom : g ∈ hom(C, j, i)184  shows InversePair(C, f, g)185proof186  have gfHom := hom.comp with category, gHom, fHom187  have fgHom := hom.comp with category, fHom, gHom188  have gfId := Initial.endomorphism with category, iInitial, gfHom189  have fgId := Initial.endomorphism with category, jInitial, fgHom190  have fInM := hom.in_morphisms with fHom191  have gInM := hom.in_morphisms with gHom192  have domF := hom.dom with fHom193  have codF := hom.cod with fHom194  have domG := hom.dom with gHom195  have codG := hom.cod with gHom196  unfold InversePair197  refine ⟨fInM, gInM, ?_, ?_, ?_, ?_⟩198  . cc199  . cc200  . cc201  . cc202203theorem Initial.isomorphism (C i j f : Set)204  requires category : Category(C)205  requires iInitial : Initial(C, i)206  requires jInitial : Initial(C, j)207  requires fHom : f ∈ hom(C, i, j)208  shows Isomorphism(C, f)209proof210  have iInO := Initial.object with iInitial211  obtain ⟨g, gHom, unique⟩ := Initial.exists_morphism with jInitial, iInO212  have pair := Initial.inverse_pair with213    category, iInitial, jInitial, fHom, gHom214  exact Isomorphism.of_pair with pair215216theorem Initial.isomorphic (C i j : Set)217  requires category : Category(C)218  requires iInitial : Initial(C, i)219  requires jInitial : Initial(C, j)220  shows Isomorphic(C, i, j)221proof222  have jInO := Initial.object with jInitial223  obtain ⟨f, fHom, unique⟩ := Initial.exists_morphism with iInitial, jInO224  have iso := Initial.isomorphism with category, iInitial, jInitial, fHom225  exact Isomorphic.of_hom with fHom, iso226227theorem Initial.unique_isomorphism (C i j f g : Set)228  requires iInitial : Initial(C, i)229  requires jInitial : Initial(C, j)230  requires fHom : f ∈ hom(C, i, j)231  requires gHom : g ∈ hom(C, i, j)232  shows f = g233proof234  have jInO := Initial.object with jInitial235  exact Initial.unique_morphism with iInitial, jInO, fHom, gHom236237theorem ZeroObject.isomorphic (C z w : Set)238  requires category : Category(C)239  requires zZero : ZeroObject(C, z)240  requires wZero : ZeroObject(C, w)241  shows Isomorphic(C, z, w)242proof243  have zTerminal := ZeroObject.terminal with zZero244  have wTerminal := ZeroObject.terminal with wZero245  exact Terminal.isomorphic with category, zTerminal, wTerminal246247-- Being terminal or initial is invariant under isomorphism.248theorem Terminal.of_isomorphic (C t u : Set)249  requires category : Category(C)250  requires terminal : Terminal(C, t)251  requires iso : Isomorphic(C, t, u)252  shows Terminal(C, u)253proof254  obtain ⟨f, fHom, g, pair⟩ := iso255  have gHom := InversePair.in_hom with pair, fHom256  have uInO := hom.cod with fHom257  have fInM := hom.in_morphisms with fHom258  have uIn : u ∈ obj(C)259    have codIn := Category.cod_closed with category, fInM260    rwa uInO at codIn261  unfold Terminal262  refine ⟨uIn, ?_⟩263  intros a aInO264  obtain ⟨v, vHom, unique⟩ := Terminal.exists_morphism with terminal, aInO265  have fvHom := hom.comp with category, fHom, vHom266  refine ⟨f ∘ v, fvHom, ?_⟩267  intros h hHom268  have ghHom := hom.comp with category, gHom, hHom269  have ghEqual := unique with g ∘ h, ghHom270  have assoc := Category.assoc_hom with category, fHom, gHom, hHom271  have unitH := Category.id_left_hom with category, hHom272  have fgId : f ∘ g = id(C)(u)273    have law := InversePair.right with pair274    have codF := hom.cod with fHom275    rwa codF at law276  calc277    h = id(C)(u) ∘ h := by rw unitH278    _ = (f ∘ g) ∘ h := by rw fgId279    _ = f ∘ (g ∘ h) := assoc280    _ = f ∘ v := by rw ghEqual281282theorem Initial.of_isomorphic (C i j : Set)283  requires category : Category(C)284  requires initial : Initial(C, i)285  requires iso : Isomorphic(C, i, j)286  shows Initial(C, j)287proof288  obtain ⟨f, fHom, g, pair⟩ := iso289  have gHom := InversePair.in_hom with pair, fHom290  have jInO := hom.cod with fHom291  have fInM := hom.in_morphisms with fHom292  have jIn : j ∈ obj(C)293    have codIn := Category.cod_closed with category, fInM294    rwa jInO at codIn295  unfold Initial296  refine ⟨jIn, ?_⟩297  intros a aInO298  obtain ⟨v, vHom, unique⟩ := Initial.exists_morphism with initial, aInO299  have vgHom := hom.comp with category, vHom, gHom300  refine ⟨v ∘ g, vgHom, ?_⟩301  intros h hHom302  have hfHom := hom.comp with category, hHom, fHom303  have hfEqual := unique with h ∘ f, hfHom304  have assoc := Category.assoc_hom with category, hHom, fHom, gHom305  have unitH := Category.id_right_hom with category, hHom306  have fgId : f ∘ g = id(C)(j)307    have law := InversePair.right with pair308    have codF := hom.cod with fHom309    rwa codF at law310  calc311    h = h ∘ id(C)(j) := by rw unitH312    _ = h ∘ (f ∘ g) := by rw fgId313    _ = (h ∘ f) ∘ g := by rw assoc314    _ = v ∘ g := by rw hfEqual315316-- Every morphism into a terminal object is a split epimorphism when its317-- domain is itself terminal, and every morphism from a terminal object is318-- a split monomorphism.319theorem Terminal.split_mono (C t a f : Set)320  requires category : Category(C)321  requires terminal : Terminal(C, t)322  requires aInO : a ∈ obj(C)323  requires fHom : f ∈ hom(C, t, a)324  shows SplitMonomorphism(C, f)325proof326  obtain ⟨r, rHom, unique⟩ := Terminal.exists_morphism with terminal, aInO327  have rfHom := hom.comp with category, rHom, fHom328  have rfId := Terminal.endomorphism with category, terminal, rfHom329  have fInM := hom.in_morphisms with fHom330  have rInM := hom.in_morphisms with rHom331  have domF := hom.dom with fHom332  have codF := hom.cod with fHom333  have domR := hom.dom with rHom334  have codR := hom.cod with rHom335  have retraction : Retraction(C, f, r)336    unfold Retraction337    refine ⟨fInM, rInM, ?_, ?_, ?_⟩338    . cc339    . cc340    . cc341  exact SplitMonomorphism.of_retraction with retraction342343theorem Initial.split_epi (C i a f : Set)344  requires category : Category(C)345  requires initial : Initial(C, i)346  requires aInO : a ∈ obj(C)347  requires fHom : f ∈ hom(C, a, i)348  shows SplitEpimorphism(C, f)349proof350  obtain ⟨s, sHom, unique⟩ := Initial.exists_morphism with initial, aInO351  have fsHom := hom.comp with category, fHom, sHom352  have fsId := Initial.endomorphism with category, initial, fsHom353  have fInM := hom.in_morphisms with fHom354  have sInM := hom.in_morphisms with sHom355  have domF := hom.dom with fHom356  have codF := hom.cod with fHom357  have domS := hom.dom with sHom358  have codS := hom.cod with sHom359  have section : SectionOf(C, f, s)360    unfold SectionOf361    refine ⟨fInM, sInM, ?_, ?_, ?_⟩362    . cc363    . cc364    . cc365  exact SplitEpimorphism.of_section with section366367-- The unique morphism from an object to a terminal object, and from an368-- initial object to an object.369defunique terminalMorphism (C t a : Set)370    (f ∈ hom(C, a, t)) :=371  ∀ g ∈ hom(C, a, t), g = f372requires terminal : Terminal(C, t)373requires aInO : a ∈ obj(C)374proof375  exact Terminal.exists_morphism with terminal, aInO376uniqueness377  intros u hu first v hv second378  exact second with u, hu379380theorem terminalMorphism.hom (C t a : Set)381  requires terminal : Terminal(C, t)382  requires aInO : a ∈ obj(C)383  shows terminalMorphism(C, t, a) ∈ hom(C, a, t)384proof385  have selected := terminalMorphism.selected at C, t, a with386    terminal, aInO387  exact selected.left388389theorem terminalMorphism.eq (C t a g : Set)390  requires terminal : Terminal(C, t)391  requires aInO : a ∈ obj(C)392  requires gHom : g ∈ hom(C, a, t)393  shows g = terminalMorphism(C, t, a)394proof395  have selected := terminalMorphism.selected at C, t, a with396    terminal, aInO397  exact selected.right with g, gHom398399theorem terminalMorphism.self (C t : Set)400  requires category : Category(C)401  requires terminal : Terminal(C, t)402  shows terminalMorphism(C, t, t) = id(C)(t)403proof404  have tInO := Terminal.object with terminal405  have idHom := hom.id with category, tInO406  have equal := terminalMorphism.eq with terminal, tInO, idHom407  symm408  exact equal409410theorem terminalMorphism.comp (C t a b f : Set)411  requires category : Category(C)412  requires terminal : Terminal(C, t)413  requires aInO : a ∈ obj(C)414  requires fHom : f ∈ hom(C, a, b)415  shows terminalMorphism(C, t, b) ∘ f =416    terminalMorphism(C, t, a)417proof418  have bInO : b ∈ obj(C)419    have fInM := hom.in_morphisms with fHom420    have codIn := Category.cod_closed with category, fInM421    have codF := hom.cod with fHom422    rwa codF at codIn423  have bHom := terminalMorphism.hom with terminal, bInO424  have composite := hom.comp with category, bHom, fHom425  exact terminalMorphism.eq with terminal, aInO, composite426427defunique initialMorphism (C i a : Set)428    (f ∈ hom(C, i, a)) :=429  ∀ g ∈ hom(C, i, a), g = f430requires initial : Initial(C, i)431requires aInO : a ∈ obj(C)432proof433  exact Initial.exists_morphism with initial, aInO434uniqueness435  intros u hu first v hv second436  exact second with u, hu437438theorem initialMorphism.hom (C i a : Set)439  requires initial : Initial(C, i)440  requires aInO : a ∈ obj(C)441  shows initialMorphism(C, i, a) ∈ hom(C, i, a)442proof443  have selected := initialMorphism.selected at C, i, a with444    initial, aInO445  exact selected.left446447theorem initialMorphism.eq (C i a g : Set)448  requires initial : Initial(C, i)449  requires aInO : a ∈ obj(C)450  requires gHom : g ∈ hom(C, i, a)451  shows g = initialMorphism(C, i, a)452proof453  have selected := initialMorphism.selected at C, i, a with454    initial, aInO455  exact selected.right with g, gHom456457theorem initialMorphism.self (C i : Set)458  requires category : Category(C)459  requires initial : Initial(C, i)460  shows initialMorphism(C, i, i) = id(C)(i)461proof462  have iInO := Initial.object with initial463  have idHom := hom.id with category, iInO464  have equal := initialMorphism.eq with initial, iInO, idHom465  symm466  exact equal467468theorem initialMorphism.comp (C i a b f : Set)469  requires category : Category(C)470  requires initial : Initial(C, i)471  requires bInO : b ∈ obj(C)472  requires fHom : f ∈ hom(C, a, b)473  shows f ∘ initialMorphism(C, i, a) =474    initialMorphism(C, i, b)475proof476  have aInO : a ∈ obj(C)477    have fInM := hom.in_morphisms with fHom478    have domIn := Category.dom_closed with category, fInM479    have domF := hom.dom with fHom480    rwa domF at domIn481  have aHom := initialMorphism.hom with initial, aInO482  have composite := hom.comp with category, fHom, aHom483  exact initialMorphism.eq with initial, bInO, composite484485-- In a category with a zero object, each hom-set has a zero morphism.486theorem ZeroObject.zero_morphism (C z a b : Set)487  requires category : Category(C)488  requires zero : ZeroObject(C, z)489  requires aInO : a ∈ obj(C)490  requires bInO : b ∈ obj(C)491  shows initialMorphism(C, z, b) ∘492    terminalMorphism(C, z, a) ∈ hom(C, a, b)493proof494  have initial := ZeroObject.initial with zero495  have terminal := ZeroObject.terminal with zero496  have toZero := terminalMorphism.hom with terminal, aInO497  have fromZero := initialMorphism.hom with initial, bInO498  exact hom.comp with category, fromZero, toZero499