Grace/Cumulus/Category/Natural.g17

Open in Workbench Download source

Imports

Functor · Set.Function.Space

Declarations

Source

1-- Natural transformations between functors2-- 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.Natural8import Functor9import Set.Function.Space1011-- η : F ⟹ G, for functors F G : C ⥤ D: a function η : obj(C) → mor(D) whose12-- component at a is a morphism η(a) : F(a) ⟶ G(a) and which commutes with13-- every morphism, η(b) ∘ F(f) = G(f) ∘ η(a). The categories are those of14-- the functors, so the predicate names only the three maps.15predicate NaturalTransformation (η F G : Set) :=16  ∀ C, ∀ D, F : C ⥤ D → G : C ⥤ D →17    (η : obj(C) → mor(D)) ∧ (∀ a ∈ obj(C), η(a) : F(a) ⟶ G(a)) ∧18    (∀ (a b ∈ obj(C)) (f : a ⟶ b), η(b) ∘ F(f) = G(f) ∘ η(a))1920notation mixfix "_ : _ ⟹ _" => NaturalTransformation2122-- The set of natural transformations from F to G.23def NatTrans (F G : Set) : Set :=24  { η ∈ functionSpace(Category.obj(src(F)), mor(tgt(F))) | η : F ⟹ G }2526predicate NaturalIsomorphism (η F G : Set) :=27  η : F ⟹ G ∧ ∀ a ∈ Category.obj(src(F)), Isomorphism(tgt(F), η(a))2829-- The constructor: a transformation is given by its components and the30-- naturality squares.31theorem NaturalTransformation.mk (η F G C D : Set)32  requires functorF : F : C ⥤ D33  requires functorG : G : C ⥤ D34  requires function : η : obj(C) → mor(D)35  requires components : ∀ a ∈ obj(C), η(a) : F(a) ⟶ G(a)36  requires naturality : ∀ (a b ∈ obj(C)) (f : a ⟶ b), η(b) ∘ F(f) = G(f) ∘ η(a)37  shows η : F ⟹ G38proof39  unfold NaturalTransformation40  intros C2 D2 functorF2 functorG241  obtain ⟨srcF, tgtF, rest⟩ := functorF42  obtain ⟨srcF2, tgtF2, rest2⟩ := functorF243  have sameSource : C2 = C by cc44  have sameTarget : D2 = D by cc45  rw under sameSource46  rw under sameTarget47  refine ⟨function, components, naturality⟩4849section TransformationLaws50variable (η F G C D : Set)51hypothesis functorF : F : C ⥤ D52hypothesis functorG : G : C ⥤ D53hypothesis natural : η : F ⟹ G5455theorem NaturalTransformation.function56  shows η : obj(C) → mor(D)57proof58  obtain ⟨function, components, naturality⟩ := natural with C, D, functorF, functorG59  exact function6061instance NaturalTransformation.component_hom (a : Set)62  requires aInO : a ∈ obj(C)63  shows η(a) : F(a) ⟶ G(a)64proof65  obtain ⟨function, components, naturality⟩ := natural with C, D, functorF, functorG66  exact components with a, aInO6768theorem NaturalTransformation.naturality (a b ∈ obj(C)) (f : a ⟶ b)69  shows η(b) ∘ F(f) = G(f) ∘ η(a)70proof71  obtain ⟨function, components, naturality⟩ := natural with C, D, functorF, functorG72  exact naturality with a, assumption, b, assumption, f, assumption7374theorem NaturalTransformation.component (a : Set)75  requires aInO : a ∈ obj(C)76  shows η(a) ∈ hom(D, F(a), G(a))77proof78  have component := NaturalTransformation.component_hom with *79  exact Morphism.hom with component8081theorem NaturalTransformation.component_closed (a : Set)82  requires aInO : a ∈ obj(C)83  shows η(a) ∈ mor(D)84proof85  have component := NaturalTransformation.component_hom with *86  exact Morphism.in_morphisms with component8788theorem NaturalTransformation.component_dom (a : Set)89  requires aInO : a ∈ obj(C)90  shows dom(D)(η(a)) = F(a)91proof92  have component := NaturalTransformation.component_hom with *93  exact Morphism.dom with component9495theorem NaturalTransformation.component_cod (a : Set)96  requires aInO : a ∈ obj(C)97  shows cod(D)(η(a)) = G(a)98proof99  have component := NaturalTransformation.component_hom with *100  exact Morphism.cod with component101102-- Naturality in hom-set form.103theorem NaturalTransformation.square (a b f : Set)104  requires fHom : f ∈ hom(C, a, b)105  shows η(b) ∘ F(f) = G(f) ∘ η(a)106proof107  have typed : f : a ⟶ b := Morphism.of_hom with fHom108  exact NaturalTransformation.naturality with *109110theorem NatTrans.of_transformation111  shows η ∈ NatTrans(F, G)112proof113  have srcF := Functor.source with functorF114  have tgtF := Functor.target with functorF115  have function := NaturalTransformation.function with *116  have bounded := functionSpace.mem_iff.backward with function117  rw [← srcF, ← tgtF] at bounded118  simp [NatTrans]119120end TransformationLaws121122theorem NatTrans.natural (η F G : Set)123  requires member : η ∈ NatTrans(F, G)124  shows η : F ⟹ G125proof126  simp [NatTrans] at member127  exact member.right128129-- The categorical rewrite set extended by the functor and transformation130-- laws: functoriality and naturality goals close by functor_simp when the131-- hom guards of the morphisms involved are in scope.132tactic functor_simp := simp [Category.id_left, Category.id_right, Category.assoc, Functor.map_id, Functor.map_comp, NaturalTransformation.naturality]133134-- Two transformations with the same components are equal.135theorem NaturalTransformation.ext (η θ F G C D : Set)136  requires functorF : F : C ⥤ D137  requires functorG : G : C ⥤ D138  requires etaNatural : η : F ⟹ G139  requires thetaNatural : θ : F ⟹ G140  requires same : ∀ a ∈ obj(C), η(a) = θ(a)141  shows η = θ142proof143  have etaFunction := NaturalTransformation.function with functorF, functorG, etaNatural144  have thetaFunction := NaturalTransformation.function with functorF, functorG, thetaNatural145  exact FunctionBetween.ext with etaFunction, thetaFunction, same146147-- The identity transformation of a functor.148defgraph identityTransformation (F : Set) (a ∈ Category.obj(src(F))) : mor(tgt(F)) :=149  id(tgt(F))(obj(F)(a))150requires functor : Functor(F, src(F), tgt(F))151proof152  have image := Functor.object_closed with functor, member153  have target := Functor.target_category with functor154  exact Category.id_closed with target, image155156section IdentityTransformation157variable (F C D : Set)158hypothesis functor : F : C ⥤ D159160theorem identityTransformation.component (a : Set)161  requires aInO : a ∈ obj(C)162  shows identityTransformation(F)(a) = id(D)(F(a))163proof164  have self := Functor.self with functor165  have srcF := Functor.source with functor166  have tgtF := Functor.target with functor167  have aInSrc : a ∈ obj(src(F)) by rwa srcF168  have value := identityTransformation.value with self, aInSrc169  rwa tgtF at value170171theorem identityTransformation.function_hom172  shows identityTransformation(F) : obj(C) → mor(D)173proof174  have self := Functor.self with functor175  have srcF := Functor.source with functor176  have tgtF := Functor.target with functor177  have function := identityTransformation.function with self178  rwa [srcF, tgtF] at function179180theorem identityTransformation.natural181  shows identityTransformation(F) : F ⟹ F182proof183  have function := identityTransformation.function_hom with functor184  apply NaturalTransformation.mk with functor, functor, function185  . intros a aIn186    rw identityTransformation.component187    synthesize188  . intros a aIn b bIn f fHom189    rw [identityTransformation.component, identityTransformation.component]190    category_simp191192end IdentityTransformation193194-- Vertical composition of transformations η : F ⟹ G and θ : G ⟹ H.195defgraph verticalComposition (η θ F G H : Set) (a ∈ Category.obj(src(F))) : mor(tgt(F)) :=196  comp(tgt(F))(θ(a), η(a))197requires functorF : Functor(F, src(F), tgt(F))198requires functorG : Functor(G, src(F), tgt(F))199requires functorH : Functor(H, src(F), tgt(F))200requires etaNatural : η : F ⟹ G201requires thetaNatural : θ : G ⟹ H202proof203  have etaHom := NaturalTransformation.component_hom with functorF, functorG, etaNatural, member204  have thetaHom := NaturalTransformation.component_hom with functorG, functorH, thetaNatural, member205  have composite : comp(tgt(F))(θ(a), η(a)) : F(a) ⟶ H(a) := Morphism.comp with *206  exact Morphism.in_morphisms with composite207208section VerticalComposition209variable (η θ F G H C D : Set)210hypothesis functorF : F : C ⥤ D211hypothesis functorG : G : C ⥤ D212hypothesis functorH : H : C ⥤ D213hypothesis etaNatural : η : F ⟹ G214hypothesis thetaNatural : θ : G ⟹ H215216theorem verticalComposition.component (a : Set)217  requires aInO : a ∈ obj(C)218  shows verticalComposition(η, θ, F, G, H)(a) = θ(a) ∘ η(a)219proof220  have srcF := Functor.source with functorF221  have tgtF := Functor.target with functorF222  have selfF := Functor.self with functorF223  have selfG : Functor(G, src(F), tgt(F)) by rwa [srcF, tgtF]224  have selfH : Functor(H, src(F), tgt(F)) by rwa [srcF, tgtF]225  have aInSrc : a ∈ obj(src(F)) by rwa srcF226  have value := verticalComposition.value with227    selfF, selfG, selfH, etaNatural, thetaNatural, aInSrc228  rwa tgtF at value229230theorem verticalComposition.function_hom231  shows verticalComposition(η, θ, F, G, H) : obj(C) → mor(D)232proof233  have srcF := Functor.source with functorF234  have tgtF := Functor.target with functorF235  have selfF := Functor.self with functorF236  have selfG : Functor(G, src(F), tgt(F)) by rwa [srcF, tgtF]237  have selfH : Functor(H, src(F), tgt(F)) by rwa [srcF, tgtF]238  have function := verticalComposition.function with selfF, selfG, selfH, etaNatural, thetaNatural239  rwa [srcF, tgtF] at function240241theorem verticalComposition.natural242  shows verticalComposition(η, θ, F, G, H) : F ⟹ H243proof244  have function : verticalComposition(η, θ, F, G, H) : obj(C) → mor(D) := verticalComposition.function_hom with *245  apply NaturalTransformation.mk with functorF, functorH, function246  . intros a aIn247    rw verticalComposition.component248    synthesize249  . intros a aIn b bIn f fHom250    rw [verticalComposition.component, verticalComposition.component]251    rw [Category.assoc, NaturalTransformation.naturality, ← Category.assoc, NaturalTransformation.naturality, Category.assoc]252    rfl253254end VerticalComposition255256-- Natural isomorphisms and their inverses.257section NaturalIsomorphismLaws258variable (η F G C D : Set)259hypothesis functorF : F : C ⥤ D260hypothesis functorG : G : C ⥤ D261262theorem NaturalIsomorphism.natural263  requires iso : NaturalIsomorphism(η, F, G)264  shows η : F ⟹ G265proof266  obtain ⟨natural, components⟩ := iso267  exact natural268269theorem NaturalIsomorphism.component (a : Set)270  requires iso : NaturalIsomorphism(η, F, G)271  requires aInO : a ∈ obj(C)272  shows Isomorphism(D, η(a))273proof274  obtain ⟨natural, components⟩ := iso275  have srcF := Functor.source with functorF276  have tgtF := Functor.target with functorF277  have aInSrc : a ∈ obj(src(F)) by rwa srcF278  have component := components with a, aInSrc279  rwa tgtF at component280281theorem NaturalIsomorphism.isomorphic (a : Set)282  requires iso : NaturalIsomorphism(η, F, G)283  requires aInO : a ∈ obj(C)284  shows Isomorphic(D, F(a), G(a))285proof286  have natural := NaturalIsomorphism.natural with functorF, functorG, iso287  have component := NaturalTransformation.component with functorF, functorG, natural, aInO288  have componentIso := NaturalIsomorphism.component with functorF, functorG, iso, aInO289  exact Isomorphic.of_hom with component, componentIso290291theorem NaturalIsomorphism.mk292  requires natural : η : F ⟹ G293  requires components : ∀ a ∈ obj(C), Isomorphism(D, η(a))294  shows NaturalIsomorphism(η, F, G)295proof296  have srcF := Functor.source with functorF297  have tgtF := Functor.target with functorF298  unfold NaturalIsomorphism299  rw under srcF300  rw under tgtF301  refine ⟨natural, components⟩302303end NaturalIsomorphismLaws304305-- The inverse of a natural isomorphism, componentwise.306defgraph inverseTransformation (η F G : Set) (a ∈ Category.obj(src(F))) : mor(tgt(F)) :=307  inverseMorphism(tgt(F), η(a))308requires functorF : Functor(F, src(F), tgt(F))309requires iso : NaturalIsomorphism(η, F, G)310proof311  have target := Functor.target_category with functorF312  obtain ⟨natural, components⟩ := iso313  have componentIso := components with a, member314  exact inverseMorphism.morphism with target, componentIso315316section InverseTransformation317variable (η F G C D : Set)318hypothesis functorF : F : C ⥤ D319hypothesis functorG : G : C ⥤ D320hypothesis iso : NaturalIsomorphism(η, F, G)321322theorem inverseTransformation.component (a : Set)323  requires aInO : a ∈ obj(C)324  shows inverseTransformation(η, F, G)(a) = inverseMorphism(D, η(a))325proof326  have srcF := Functor.source with functorF327  have tgtF := Functor.target with functorF328  have selfF := Functor.self with functorF329  have aInSrc : a ∈ obj(src(F)) by rwa srcF330  have value := inverseTransformation.value with selfF, iso, aInSrc331  rwa tgtF at value332333theorem inverseTransformation.function_hom334  shows inverseTransformation(η, F, G) : obj(C) → mor(D)335proof336  have srcF := Functor.source with functorF337  have tgtF := Functor.target with functorF338  have selfF := Functor.self with functorF339  have function := inverseTransformation.function with selfF, iso340  rwa [srcF, tgtF] at function341342theorem inverseTransformation.component_hom (a : Set)343  requires aInO : a ∈ obj(C)344  shows inverseTransformation(η, F, G)(a) : G(a) ⟶ F(a)345proof346  have target := Functor.target_category with functorF347  have natural := NaturalIsomorphism.natural with functorF, functorG, iso348  have component : η(a) : F(a) ⟶ G(a) :=349    NaturalTransformation.component_hom with functorF, functorG, natural, aInO350  have componentIso := NaturalIsomorphism.component with functorF, functorG, iso, aInO351  have pair := inverseMorphism.pair with target, componentIso352  rw inverseTransformation.component353  exact InversePair.inverse_of_hom with *354355theorem inverseTransformation.natural356  shows inverseTransformation(η, F, G) : G ⟹ F357proof358  have target := Functor.target_category with functorF359  have natural := NaturalIsomorphism.natural with functorF, functorG, iso360  have function := inverseTransformation.function_hom with functorF, functorG, iso361  apply NaturalTransformation.mk with functorG, functorF, function362  . intros a aIn363    exact inverseTransformation.component_hom with functorF, functorG, iso, aIn364  . intros a aIn b bIn f fHom365    have fHomSet : f ∈ hom(C, a, b) := Morphism.hom with fHom366    have etaA := NaturalTransformation.component with functorF, functorG, natural, aIn367    have etaB := NaturalTransformation.component with functorF, functorG, natural, bIn368    have isoA := NaturalIsomorphism.component with functorF, functorG, iso, aIn369    have isoB := NaturalIsomorphism.component with functorF, functorG, iso, bIn370    have pairA := inverseMorphism.pair with target, isoA371    have pairB := inverseMorphism.pair with target, isoB372    have imageF := Functor.hom with functorF, fHomSet373    have imageG := Functor.hom with functorG, fHomSet374    have square : η(b) ∘ F(f) = G(f) ∘ η(a) :=375      NaturalTransformation.naturality with functorF, functorG, natural, aIn, bIn, fHom376    rw [inverseTransformation.component, inverseTransformation.component]377    exact InversePair.transpose with target, pairA, pairB, etaA, etaB, imageF, imageG, square378379theorem inverseTransformation.natural_iso380  shows NaturalIsomorphism(inverseTransformation(η, F, G), G, F)381proof382  have target := Functor.target_category with functorF383  have natural := inverseTransformation.natural with functorF, functorG, iso384  apply NaturalIsomorphism.mk with functorG, functorF, natural385  intros a aIn386  have componentIso := NaturalIsomorphism.component with functorF, functorG, iso, aIn387  rw inverseTransformation.component388  exact inverseMorphism.isomorphism with target, componentIso389390theorem inverseTransformation.vertical_left391  shows verticalComposition(η, inverseTransformation(η, F, G), F, G, F) =392    identityTransformation(F)393proof394  have target := Functor.target_category with functorF395  have natural := NaturalIsomorphism.natural with functorF, functorG, iso396  have inverseNatural := inverseTransformation.natural with functorF, functorG, iso397  have composite := verticalComposition.natural with398    functorF, functorG, functorF, natural, inverseNatural399  have identityNatural := identityTransformation.natural with functorF400  apply NaturalTransformation.ext with functorF, functorF, composite, identityNatural401  intros a aIn402  have component : η(a) : F(a) ⟶ G(a) :=403    NaturalTransformation.component_hom with functorF, functorG, natural, aIn404  have componentIso := NaturalIsomorphism.component with functorF, functorG, iso, aIn405  have pair := inverseMorphism.pair with target, componentIso406  have left : inverseMorphism(D, η(a)) ∘ η(a) = id(D)(F(a)) := InversePair.left_hom with *407  rw [verticalComposition.component, inverseTransformation.component, identityTransformation.component]408  exact left409410theorem inverseTransformation.vertical_right411  shows verticalComposition(inverseTransformation(η, F, G), η, G, F, G) =412    identityTransformation(G)413proof414  have target := Functor.target_category with functorF415  have natural := NaturalIsomorphism.natural with functorF, functorG, iso416  have inverseNatural := inverseTransformation.natural with functorF, functorG, iso417  have composite := verticalComposition.natural with418    functorG, functorF, functorG, inverseNatural, natural419  have identityNatural := identityTransformation.natural with functorG420  apply NaturalTransformation.ext with functorG, functorG, composite, identityNatural421  intros a aIn422  have component : η(a) : F(a) ⟶ G(a) :=423    NaturalTransformation.component_hom with functorF, functorG, natural, aIn424  have componentIso := NaturalIsomorphism.component with functorF, functorG, iso, aIn425  have pair := inverseMorphism.pair with target, componentIso426  have right : η(a) ∘ inverseMorphism(D, η(a)) = id(D)(G(a)) := InversePair.right_hom with *427  rw [verticalComposition.component, inverseTransformation.component, identityTransformation.component]428  exact right429430end InverseTransformation431432-- The identity transformation is a natural isomorphism, and it is a unit433-- for vertical composition.434section IdentityLaws435variable (η F G C D : Set)436hypothesis functorF : F : C ⥤ D437hypothesis functorG : G : C ⥤ D438hypothesis natural : η : F ⟹ G439440theorem identityTransformation.natural_iso441  shows NaturalIsomorphism(identityTransformation(F), F, F)442proof443  have target := Functor.target_category with functorF444  have identityNatural := identityTransformation.natural with functorF445  apply NaturalIsomorphism.mk with functorF, functorF, identityNatural446  intros a aIn447  have image := Functor.object_closed with functorF, aIn448  rw identityTransformation.component449  exact Isomorphism.id with target, image450451theorem verticalComposition.identity_left452  shows verticalComposition(η, identityTransformation(G), F, G, G) = η453proof454  have identityNatural := identityTransformation.natural with functorG455  have composite := verticalComposition.natural with456    functorF, functorG, functorG, natural, identityNatural457  apply NaturalTransformation.ext with functorF, functorG, composite, natural458  intros a aIn459  have component : η(a) : F(a) ⟶ G(a) :=460    NaturalTransformation.component_hom with functorF, functorG, natural, aIn461  rw [verticalComposition.component, identityTransformation.component]462  category_simp463464theorem verticalComposition.identity_right465  shows verticalComposition(identityTransformation(F), η, F, F, G) = η466proof467  have identityNatural := identityTransformation.natural with functorF468  have composite := verticalComposition.natural with469    functorF, functorF, functorG, identityNatural, natural470  apply NaturalTransformation.ext with functorF, functorG, composite, natural471  intros a aIn472  have component : η(a) : F(a) ⟶ G(a) :=473    NaturalTransformation.component_hom with functorF, functorG, natural, aIn474  rw [verticalComposition.component, identityTransformation.component]475  category_simp476477end IdentityLaws478