Grace/Cumulus/Category/Yoneda.g17

Open in Workbench Download source

Imports

HomFunctor · Cardinal.Finite

Declarations

Source

1-- The Yoneda lemma2-- 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.Yoneda8import HomFunctor9import Cardinal.Finite1011-- For a functor F : C ⥤ Sets(U), an object a, and x ∈ F(a): the12-- transformation hom(a, −) ⟹ F whose component at b sends f : a ⟶ b to13-- F(f)(x).14defgraph yonedaComponent (C U F a x b : Set) (f ∈ hom(C, a, b)) : F(b) := F(f)(x)15requires functor : F : C ⥤ Sets(U)16requires aInO : a ∈ obj(C)17requires bInO : b ∈ obj(C)18requires xIn : x ∈ F(a)19proof20  have fHom : f : a ⟶ b := Morphism.of_hom with member21  have image : F(f) : F(a) ⟶ F(b) := Functor.map_hom with *22  exact Sets.apply_closed with *2324defgraph yonedaTransformation (C U F a x : Set) (b ∈ Category.obj(C)) : mor(Sets(U)) :=25  setArrow(U, F(b), yonedaComponent(C, U, F, a, x, b))26requires functor : F : C ⥤ Sets(U)27requires small : mor(C) ⊆ U28requires aInO : a ∈ obj(C)29requires xIn : x ∈ F(a)30proof31  have homIn := hom.object at C, U, a, b with small32  have objectIn : F(b) ∈ obj(Sets(U)) := Functor.object_closed with *33  have function := yonedaComponent.function at C, U, F, a, x, b with functor, aInO, member, xIn34  have mapIn := functionSpace.mem_iff.backward with function35  rw Sets.obj at objectIn36  rw Sets.mor37  exact setsMorphisms.arrow with homIn, objectIn, mapIn3839section YonedaTransformation40variable (C U F a : Set)41hypothesis functor : F : C ⥤ Sets(U)42hypothesis small : mor(C) ⊆ U43hypothesis aInO : a ∈ obj(C)4445theorem yonedaComponent.apply (x b f : Set)46  requires xIn : x ∈ F(a)47  requires bInO : b ∈ obj(C)48  requires fHom : f ∈ hom(C, a, b)49  shows yonedaComponent(C, U, F, a, x, b)(f) = F(f)(x)50proof51  exact yonedaComponent.value at C, U, F, a, x, b, f with functor, aInO, bInO, xIn, fHom5253theorem yonedaTransformation.component (x b : Set)54  requires xIn : x ∈ F(a)55  requires bInO : b ∈ obj(C)56  shows yonedaTransformation(C, U, F, a, x)(b) =57    setArrow(U, F(b), yonedaComponent(C, U, F, a, x, b))58proof59  exact yonedaTransformation.value at C, U, F, a, x, b with functor, small, aInO, xIn, bInO6061instance yonedaTransformation.component_hom (x b : Set)62  requires xIn : x ∈ F(a)63  requires bInO : b ∈ obj(C)64  shows yonedaTransformation(C, U, F, a, x)(b) : hom(C, a, b) ⟶ F(b)65proof66  have sets := Sets.category at U67  have homIn := hom.object at C, U, a, b with small68  have objectIn : F(b) ∈ obj(Sets(U)) := Functor.object_closed with *69  have function := yonedaComponent.function at C, U, F, a, x, b with functor, aInO, bInO, xIn70  rw Sets.obj at objectIn71  rw yonedaTransformation.component72  exact Sets.arrow_hom with sets, homIn, objectIn, function7374theorem yonedaTransformation.function_hom (x : Set)75  requires xIn : x ∈ F(a)76  shows yonedaTransformation(C, U, F, a, x) : obj(C) → mor(Sets(U))77proof78  exact yonedaTransformation.function at C, U, F, a, x with functor, small, aInO, xIn7980-- The naturality square at g : b ⟶ c, applied to f ∈ hom(a, b), reads81-- F(g ∘ f)(x) = F(g)(F(f)(x)), which is functoriality of F.82theorem yonedaTransformation.natural (x : Set)83  requires xIn : x ∈ F(a)84  shows yonedaTransformation(C, U, F, a, x) : homFunctor(C, U, a) ⟹ F85proof86  have sets := Sets.category at U87  have homF : homFunctor(C, U, a) : C ⥤ Sets(U) := homFunctor.functor with *88  apply NaturalTransformation.mk with homF, functor89  . exact yonedaTransformation.function_hom with *90  . intros b bIn91    rw homFunctor.obj92    exact yonedaTransformation.component_hom with *93  . intros b bIn c cIn g gHom94    have left : yonedaTransformation(C, U, F, a, x)(c) ∘ homFunctor(C, U, a)(g) : hom(C, a, b) ⟶ F(c) by synthesize95    have right : F(g) ∘ yonedaTransformation(C, U, F, a, x)(b) : hom(C, a, b) ⟶ F(c) by synthesize96    apply Sets.ext with left, right, sets97    intros f fHom98    have fTyped : f : a ⟶ b := Morphism.of_hom with fHom99    have fImage : F(f) : F(a) ⟶ F(b) := Functor.map_hom with *100    have gImage : F(g) : F(b) ⟶ F(c) := Functor.map_hom with *101    simp [Sets.comp_apply, homFunctor.map_hom, Sets.arrow_apply, postComposition.apply, yonedaTransformation.component, yonedaComponent.apply, Functor.map_comp]102103end YonedaTransformation104105-- The Yoneda map sends a transformation η : hom(a, −) ⟹ F to the value106-- of its component at a on the identity of a; its inverse sends x ∈ F(a)107-- to the transformation above.108defgraph yonedaMap (C U F a : Set) (η ∈ NatTrans(homFunctor(C, U, a), F)) : F(a) :=109  η(a)(id(C)(a))110requires functor : F : C ⥤ Sets(U)111requires small : mor(C) ⊆ U112requires aInO : a ∈ obj(C)113proof114  have category := Functor.source_category with functor115  have homF := homFunctor.functor with category, small, aInO116  have natural := NatTrans.natural with member117  have component : η(a) : homFunctor(C, U, a)(a) ⟶ F(a) :=118    NaturalTransformation.component_hom with *119  have idHom : id(C)(a) ∈ hom(C, a, a) := hom.id with category, aInO120  rw homFunctor.obj at component121  exact Sets.apply_closed with *122123defgraph yonedaInverse (C U F a : Set) (x ∈ F(a)) : NatTrans(homFunctor(C, U, a), F) :=124  yonedaTransformation(C, U, F, a, x)125requires functor : F : C ⥤ Sets(U)126requires small : mor(C) ⊆ U127requires aInO : a ∈ obj(C)128proof129  have category := Functor.source_category with functor130  have homF := homFunctor.functor with category, small, aInO131  have natural := yonedaTransformation.natural with functor, small, aInO, member132  exact NatTrans.of_transformation with homF, functor, natural133134section YonedaLemma135variable (C U F a : Set)136hypothesis functor : F : C ⥤ Sets(U)137hypothesis small : mor(C) ⊆ U138hypothesis aInO : a ∈ obj(C)139140theorem yonedaMap.apply (η : Set)141  requires natural : η : homFunctor(C, U, a) ⟹ F142  shows yonedaMap(C, U, F, a)(η) = η(a)(id(C)(a))143proof144  have category := Functor.source_category with functor145  have homF := homFunctor.functor with category, small, aInO146  have member := NatTrans.of_transformation with homF, functor, natural147  exact yonedaMap.value at C, U, F, a, η with functor, small, aInO, member148149theorem yonedaInverse.apply (x : Set)150  requires xIn : x ∈ F(a)151  shows yonedaInverse(C, U, F, a)(x) = yonedaTransformation(C, U, F, a, x)152proof153  exact yonedaInverse.value at C, U, F, a, x with functor, small, aInO, xIn154155theorem yonedaMap.in (η : Set)156  requires natural : η : homFunctor(C, U, a) ⟹ F157  shows yonedaMap(C, U, F, a)(η) ∈ F(a)158proof159  have homF : homFunctor(C, U, a) : C ⥤ Sets(U) := homFunctor.functor with *160  have member := NatTrans.of_transformation with homF, functor, natural161  have function := yonedaMap.function at C, U, F, a with functor, small, aInO162  exact FunctionBetween.apply_closed with function, member163164-- The component at b of a transformation η : hom(a, −) ⟹ F, as a morphism165-- hom(C, a, b) ⟶ F(b) of Sets(U).166theorem NaturalTransformation.yoneda_component_hom (η b : Set)167  requires natural : η : homFunctor(C, U, a) ⟹ F168  requires bInO : b ∈ obj(C)169  shows η(b) : hom(C, a, b) ⟶ F(b)170proof171  have homF : homFunctor(C, U, a) : C ⥤ Sets(U) := homFunctor.functor with *172  have component : η(b) : homFunctor(C, U, a)(b) ⟶ F(b) :=173    NaturalTransformation.component_hom with *174  rwa homFunctor.obj at component175176-- Naturality of η : hom(a, −) ⟹ F at f : a ⟶ b, applied to id(a): every177-- component is determined by the value of the component at a on id(a).178theorem NaturalTransformation.yoneda_component (η b f : Set)179  requires natural : η : homFunctor(C, U, a) ⟹ F180  requires bInO : b ∈ obj(C)181  requires fHom : f ∈ hom(C, a, b)182  shows η(b)(f) = F(f)(η(a)(id(C)(a)))183proof184  have sets := Sets.category at U185  have homF : homFunctor(C, U, a) : C ⥤ Sets(U) := homFunctor.functor with *186  have idHom : id(C)(a) ∈ hom(C, a, a) := hom.id with *187  have fTyped : f : a ⟶ b := Morphism.of_hom with fHom188  have etaA : η(a) : hom(C, a, a) ⟶ F(a) := NaturalTransformation.yoneda_component_hom with *189  have etaB : η(b) : hom(C, a, b) ⟶ F(b) := NaturalTransformation.yoneda_component_hom with *190  have square : η(b) ∘ homFunctor(C, U, a)(f) = F(f) ∘ η(a) := NaturalTransformation.naturality with *191  have applied : (η(b) ∘ homFunctor(C, U, a)(f))(id(C)(a)) = (F(f) ∘ η(a))(id(C)(a))192    rw square193    rfl194  simpa [Sets.comp_apply, homFunctor.map_hom, Sets.arrow_apply, postComposition.apply, Category.id_right] using applied195196-- Round trip on F(a): the component at a of the transformation of x,197-- applied to id(a), is F(id(a))(x) = x.198theorem yonedaMap.inverse (x : Set)199  requires xIn : x ∈ F(a)200  shows yonedaMap(C, U, F, a)(yonedaInverse(C, U, F, a)(x)) = x201proof202  have category := Functor.source_category with functor203  have sets := Sets.category at U204  have natural := yonedaTransformation.natural with *205  have idHom : id(C)(a) ∈ hom(C, a, a) := hom.id with category, aInO206  have objectIn : F(a) ∈ obj(Sets(U)) := Functor.object_closed with *207  rw Sets.obj at objectIn208  rw [yonedaInverse.apply, yonedaMap.apply, yonedaTransformation.component]209  simp [Sets.arrow_apply, yonedaComponent.apply, Functor.map_id, Sets.id_apply]210211-- Round trip on transformations: naturality of η at f ∈ hom(a, b), applied212-- to id(a), gives η(b)(f) = F(f)(η(a)(id(a))).213theorem yonedaInverse.map (η : Set)214  requires natural : η : homFunctor(C, U, a) ⟹ F215  shows yonedaInverse(C, U, F, a)(yonedaMap(C, U, F, a)(η)) = η216proof217  have sets := Sets.category at U218  have homF : homFunctor(C, U, a) : C ⥤ Sets(U) := homFunctor.functor with *219  have xIn : yonedaMap(C, U, F, a)(η) ∈ F(a) := yonedaMap.in with *220  have inverseNatural := yonedaTransformation.natural with functor, small, aInO, xIn221  rw yonedaInverse.apply222  apply NaturalTransformation.ext with homF, functor, inverseNatural, natural223  intros b bIn224  have left := yonedaTransformation.component_hom with functor, small, aInO, xIn, bIn225  have right : η(b) : hom(C, a, b) ⟶ F(b) := NaturalTransformation.yoneda_component_hom with *226  apply Sets.ext with left, right, sets227  intros f fHom228  have core := NaturalTransformation.yoneda_component with *229  rw [yonedaTransformation.component, Sets.arrow_apply, yonedaComponent.apply, yonedaMap.apply, core]230  rfl231232theorem yonedaMap.bijective233  shows BijectiveBetween(yonedaMap(C, U, F, a), NatTrans(homFunctor(C, U, a), F), F(a))234proof235  have function := yonedaMap.function at C, U, F, a with functor, small, aInO236  have inverse := yonedaInverse.function at C, U, F, a with functor, small, aInO237  have leftLaw : ∀ η ∈ NatTrans(homFunctor(C, U, a), F),238    yonedaInverse(C, U, F, a)(yonedaMap(C, U, F, a)(η)) = η239    intros η member240    have natural := NatTrans.natural with member241    exact yonedaInverse.map with functor, small, aInO, natural242  have rightLaw : ∀ x ∈ F(a), yonedaMap(C, U, F, a)(yonedaInverse(C, U, F, a)(x)) = x243    intros x xIn244    exact yonedaMap.inverse with functor, small, aInO, xIn245  exact Bijective.of_two_sided_inverse with function, inverse, leftLaw, rightLaw246247end YonedaLemma248249-- The Yoneda lemma: for a functor F from a small category C, whose250-- morphisms lie in U, into the category of sets below U, and an object a,251-- the natural transformations hom(a, −) ⟹ F are in bijection with F(a).252theorem yoneda (C U F a : Set)253  requires functor : F : C ⥤ Sets(U)254  requires small : mor(C) ⊆ U255  requires aInO : a ∈ obj(C)256  shows NatTrans(homFunctor(C, U, a), F) ≃ F(a)257proof258  have bijective := yonedaMap.bijective with functor, small, aInO259  witness yonedaMap(C, U, F, a)260  exact bijective261262-- The Yoneda embedding is fully faithful: transformations between two263-- hom functors hom(a, −) ⟹ hom(b, −) correspond to morphisms b ⟶ a.264theorem yoneda.hom_functors (C U a b : Set)265  requires category : Category(C)266  requires small : mor(C) ⊆ U267  requires aInO : a ∈ obj(C)268  requires bInO : b ∈ obj(C)269  shows NatTrans(homFunctor(C, U, a), homFunctor(C, U, b)) ≃ hom(C, b, a)270proof271  have functor := homFunctor.functor with category, small, bInO272  have equipotent := yoneda with functor, small, aInO273  have object := homFunctor.obj at C, U, b, a with category, small, aInO274  rw object at equipotent275  exact equipotent276