Grace/Cumulus/Category/HomFunctor.g17

Open in Workbench Download source

Imports

SetMorphism

Declarations

Source

1-- The covariant hom functor hom(a, −) into the category of sets2-- 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.HomFunctor8import SetMorphism910-- Post-composition with g : b ⟶ c, as the function hom(C, a, b) → hom(C, a, c)11-- sending f to g ∘ f.12defgraph postComposition (C a b c g : Set) (f ∈ hom(C, a, b)) : hom(C, a, c) := g ∘ f13requires category : Category(C)14requires gHom : g ∈ hom(C, b, c)15proof16  exact hom.comp with category, gHom, member1718section PostComposition19variable (C a : Set)20hypothesis category : Category(C)2122theorem postComposition.apply (b c : Set) (g : b ⟶ c) (f : Set)23  requires fHom : f ∈ hom(C, a, b)24  shows postComposition(C, a, b, c, g)(f) = g ∘ f25proof26  have gHom : g ∈ hom(C, b, c) := Morphism.hom with *27  exact postComposition.value with category, gHom, fHom2829theorem postComposition.function_hom (b c g : Set)30  requires gHom : g ∈ hom(C, b, c)31  shows postComposition(C, a, b, c, g) : hom(C, a, b) → hom(C, a, c)32proof33  exact postComposition.function with category, gHom3435-- Post-composition with an identity is the identity, and post-composition36-- with a composite is the composite of the post-compositions.37theorem postComposition.identity (b : Set)38  requires bInO : b ∈ obj(C)39  shows postComposition(C, a, b, b, id(C)(b)) = identity(hom(C, a, b))40proof41  have idHom := hom.id with category, bInO42  have idTyped : id(C)(b) : b ⟶ b := Morphism.of_hom with idHom43  have function : postComposition(C, a, b, b, id(C)(b)) : hom(C, a, b) → hom(C, a, b) :=44    postComposition.function_hom with category, idHom45  have identityFunction := identity.function at hom(C, a, b)46  apply FunctionBetween.ext with function, identityFunction47  intros f fHom48  have value := postComposition.apply with category, idTyped, fHom49  have unit := Category.id_left_hom with category, fHom50  have idValue := identity.apply with fHom51  rw [value, unit, idValue]52  rfl5354theorem postComposition.compose (b c d g h : Set)55  requires hHom : h ∈ hom(C, c, d)56  requires gHom : g ∈ hom(C, b, c)57  shows postComposition(C, a, b, d, h ∘ g) =58    compose(postComposition(C, a, c, d, h), postComposition(C, a, b, c, g),59      hom(C, a, b), hom(C, a, c), hom(C, a, d))60proof61  have hgHom := hom.comp with category, hHom, gHom62  have hTyped : h : c ⟶ d := Morphism.of_hom with hHom63  have gTyped : g : b ⟶ c := Morphism.of_hom with gHom64  have hgTyped : h ∘ g : b ⟶ d := Morphism.of_hom with hgHom65  have composite : postComposition(C, a, b, d, h ∘ g) : hom(C, a, b) → hom(C, a, d) :=66    postComposition.function_hom with category, hgHom67  have hFunction : postComposition(C, a, c, d, h) : hom(C, a, c) → hom(C, a, d) :=68    postComposition.function_hom with category, hHom69  have gFunction : postComposition(C, a, b, c, g) : hom(C, a, b) → hom(C, a, c) :=70    postComposition.function_hom with category, gHom71  have composed := compose.function with gFunction, hFunction72  apply FunctionBetween.ext with composite, composed73  intros f fHom74  have gfHom := hom.comp with category, gHom, fHom75  have compositeValue := postComposition.apply with category, hgTyped, fHom76  have composedValue := compose.apply with gFunction, hFunction, fHom77  have gValue := postComposition.apply with category, gTyped, fHom78  have hValue := postComposition.apply with category, hTyped, gfHom79  have assoc := Category.assoc_hom with category, hHom, gHom, fHom80  rw [compositeValue, composedValue, gValue, hValue, assoc]81  rfl8283end PostComposition8485-- When the morphisms of C lie in U, every hom-set is an object of Sets(U).86theorem hom.object (C U a b : Set)87  requires small : mor(C) ⊆ U88  shows hom(C, a, b) ∈ 𝒫(U)89proof90  have subset := hom.subset at C, a, b91  have bounded := Subset.transitive with subset, small92  exact powerset.membership_iff.backward with bounded9394-- The hom functor hom(a, −): an object b goes to the hom-set hom(C, a, b),95-- a morphism g to post-composition with g between the hom-sets at its96-- endpoints.97defgraph homObjects (C U a : Set) (b ∈ Category.obj(C)) : 𝒫(U) := hom(C, a, b)98requires small : mor(C) ⊆ U99proof100  exact hom.object with small101102defgraph homMorphisms (C U a : Set) (g ∈ mor(C)) : setsMorphisms(U) :=103  setArrow(U, hom(C, a, cod(C)(g)),104    postComposition(C, a, dom(C)(g), cod(C)(g), g))105requires category : Category(C)106requires small : mor(C) ⊆ U107proof108  have gHom := hom.of_morphism at C, g with member109  have domIn := hom.object at C, U, a, dom(C)(g) with small110  have codIn := hom.object at C, U, a, cod(C)(g) with small111  have function := postComposition.function at112    C, a, dom(C)(g), cod(C)(g), g with category, gHom113  have mapIn := functionSpace.mem_iff.backward with function114  exact setsMorphisms.arrow with domIn, codIn, mapIn115116def homFunctor (C U a : Set) : Set :=117  Functor.mk(homObjects(C, U, a), homMorphisms(C, U, a), C, Sets(U))118119section HomFunctor120variable (C U a : Set)121hypothesis category : Category(C)122hypothesis small : mor(C) ⊆ U123124theorem homFunctor.obj (b : Set)125  requires bInO : b ∈ obj(C)126  shows obj(homFunctor(C, U, a))(b) = hom(C, a, b)127proof128  have value := homObjects.value at C, U, a, b with small, bInO129  simp [homFunctor, Functor.mk.obj, value]130131theorem homFunctor.map (g : Set)132  requires gInM : g ∈ mor(C)133  shows map(homFunctor(C, U, a))(g) =134    setArrow(U, hom(C, a, cod(C)(g)), postComposition(C, a, dom(C)(g), cod(C)(g), g))135proof136  have value := homMorphisms.value at C, U, a, g with category, small, gInM137  simp [homFunctor, Functor.mk.map, value]138139theorem homFunctor.map_hom (b c : Set) (g : b ⟶ c)140  shows map(homFunctor(C, U, a))(g) = setArrow(U, hom(C, a, c), postComposition(C, a, b, c, g))141proof142  have gHom : g ∈ hom(C, b, c) := Morphism.hom with *143  obtain ⟨gInM, domG, codG⟩ := hom.membership.forward with gHom144  have value := homFunctor.map at C, U, a, g with category, small, gInM145  rw [domG, codG] at value146  exact value147148-- The image of g : b ⟶ c is a morphism hom(C, a, b) ⟶ hom(C, a, c) of Sets(U).149instance homFunctor.map_typed (b c ∈ obj(C)) (g : b ⟶ c)150  shows Morphism(Sets(U), map(homFunctor(C, U, a))(g), hom(C, a, b), hom(C, a, c))151proof152  have sets := Sets.category at U153  have gHomSet : g ∈ hom(C, b, c) := Morphism.hom with *154  have homB := hom.object at C, U, a, b with small155  have homC := hom.object at C, U, a, c with small156  have function := postComposition.function_hom at C, a, b, c, g with category, gHomSet157  have arrow := Sets.arrow_hom with sets, homB, homC, function158  rw homFunctor.map_hom159  exact arrow160161theorem homFunctor.object_function162  shows obj(homFunctor(C, U, a)) : obj(C) → obj(Sets(U))163proof164  have function := homObjects.function at C, U, a with small165  unfold homFunctor166  rw [Functor.mk.obj, Sets.obj]167  exact function168169theorem homFunctor.morphism_function170  shows map(homFunctor(C, U, a)) : mor(C) → mor(Sets(U))171proof172  have function := homMorphisms.function at C, U, a with category, small173  unfold homFunctor174  rw [Functor.mk.map, Sets.mor]175  exact function176177theorem homFunctor.functor178  requires aInO : a ∈ obj(C)179  shows homFunctor(C, U, a) : C ⥤ Sets(U)180proof181  have sets := Sets.category at U182  have srcLaw : src(homFunctor(C, U, a)) = C183    simp [homFunctor, Functor.mk.src]184  have tgtLaw : tgt(homFunctor(C, U, a)) = Sets(U)185    simp [homFunctor, Functor.mk.tgt]186  have objects := homFunctor.object_function at C, U, a with category, small187  have morphisms := homFunctor.morphism_function at C, U, a with category, small188  have shape : Functor.Data(homFunctor(C, U, a)) by simp [homFunctor, Functor.mk.data]189  unfold Functor190  refine ⟨shape, category, sets, objects, morphisms, ?_, ?_, ?_, srcLaw, tgtLaw⟩191  . intros b bIn c cIn g gHom192    have gHomSet : g ∈ hom(C, b, c) := Morphism.hom with gHom193    have homB := hom.object at C, U, a, b with small194    have homC := hom.object at C, U, a, c with small195    have function := postComposition.function_hom at C, a, b, c, g with category, gHomSet196    have arrow := Sets.arrow_hom with sets, homB, homC, function197    rw [homFunctor.obj, homFunctor.obj, homFunctor.map_hom]198    exact arrow199  . intros b bIn200    have idHom := hom.id with category, bIn201    have homB := hom.object at C, U, a, b with small202    have identityValue := setsIdentity.value with homB203    have postIdentity := postComposition.identity at C, a, b with category, bIn204    rw [homFunctor.obj, homFunctor.map_hom, postIdentity, Sets.id, identityValue]205    rfl206  . intros b bIn c cIn d dIn f fHom g gHom207    have fHomSet : f ∈ hom(C, b, c) := Morphism.hom with fHom208    have gHomSet : g ∈ hom(C, c, d) := Morphism.hom with gHom209    have gfHomSet : g ∘ f ∈ hom(C, b, d) := hom.comp with category, gHomSet, fHomSet210    have homB := hom.object at C, U, a, b with small211    have homC := hom.object at C, U, a, c with small212    have homD := hom.object at C, U, a, d with small213    have fFunction := postComposition.function_hom at C, a, b, c, f with category, fHomSet214    have gFunction := postComposition.function_hom at C, a, c, d, g with category, gHomSet215    have fMapIn := functionSpace.mem_iff.backward with fFunction216    have gMapIn := functionSpace.mem_iff.backward with gFunction217    have composite := setsComposition.arrow with homB, homC, homD, fMapIn, gMapIn218    have postComposite := postComposition.compose at C, a, b, c, d, f, g with category, gHomSet, fHomSet219    rw [homFunctor.map_hom, homFunctor.map_hom, homFunctor.map_hom, postComposite]220    rw [Sets.comp, composite]221    rfl222223end HomFunctor224225-- The contravariant hom functor hom(−, a) is the hom functor of the226-- opposite category.227theorem homFunctor.contravariant (C U a : Set)228  requires category : Category(C)229  requires small : mor(C) ⊆ U230  requires aInO : a ∈ obj(C)231  shows homFunctor(opposite(C), U, a) : opposite(C) ⥤ Sets(U)232proof233  have opposite := Category.opposite with category234  have smallOpposite : mor(opposite(C)) ⊆ U by opposite_projections235  have aInOpposite : a ∈ obj(opposite(C)) by opposite_projections236  exact homFunctor.functor with opposite, smallOpposite, aInOpposite237