CategoryTheory.coconeOfRepresentable_naturality
theorem CategoryTheory.coconeOfRepresentable_naturality :
∀ {C : Type u₁} [inst : CategoryTheory.SmallCategory C] {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ (Type u₁)} (α : P₁ ⟶ P₂)
(j : P₁.Elementsᵒᵖ),
CategoryTheory.CategoryStruct.comp ((CategoryTheory.coconeOfRepresentable P₁).ι.app j) α =
(CategoryTheory.coconeOfRepresentable P₂).ι.app ((CategoryTheory.CategoryOfElements.map α).op.obj j)
This theorem, named `CategoryTheory.coconeOfRepresentable_naturality`, states that for any small category `C`, and any two presheaves `P₁` and `P₂` over `C`, along with a natural transformation `α` between these presheaves, and any object `j` in the category of elements of the presheaf `P₁`, the composition of the morphism represented by `j` in the cocone constructed from `P₁` with the natural transformation `α` equals the morphism represented by the object in the category of elements of `P₂` that corresponds to `j` through the functor induced by `α`. In other words, the morphisms (or "legs") of the cocones constructed from the representable presheaves are natural in the choice of presheaf, meaning that changing the presheaf with a natural transformation preserves the structure of the cocone.
More concisely: For any small category $C$, presheaves $P\_1$ and $P\_2$ over $C$, and natural transformation $\alpha$ between them, the morphism from the object $j$ in the cocone of $P\_1$ to the object $\alpha(j)$ in the cocone of $P\_2$ is equal to the composition of the morphism from $j$ in $P\_1$ to the object it represents in $C$, and the morphism from that object to $\alpha(j)$ in $P\_2$.
|
CategoryTheory.ColimitAdj.restrictYonedaHomEquiv_natural
theorem CategoryTheory.ColimitAdj.restrictYonedaHomEquiv_natural :
∀ {C : Type u₁} [inst : CategoryTheory.SmallCategory C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{u₁, u₂} ℰ]
(A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (E₁ E₂ : ℰ) (g : E₁ ⟶ E₂)
{c : CategoryTheory.Limits.Cocone ((CategoryTheory.CategoryOfElements.π P).leftOp.comp A)}
(t : CategoryTheory.Limits.IsColimit c) (k : c.pt ⟶ E₁),
(CategoryTheory.ColimitAdj.restrictYonedaHomEquiv A P E₂ t) (CategoryTheory.CategoryStruct.comp k g) =
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ColimitAdj.restrictYonedaHomEquiv A P E₁ t) k)
((CategoryTheory.ColimitAdj.restrictedYoneda A).map g)
This theorem, `CategoryTheory.ColimitAdj.restrictYonedaHomEquiv_natural`, asserts the naturality of a bijection (`restrictYonedaHomEquiv`) in the context of category theory. More specifically, given a small category `C`, a category `ℰ`, two functors `A` from `C` to `ℰ` and `P` from the opposite category of `C` to `Type u₁`, two objects `E₁` and `E₂` in `ℰ`, a morphism `g` from `E₁` to `E₂`, a cocone `c` for the functor composition of the functor `A` and the left opposite of the functor `CategoryOfElements.π P`, and a morphism `k` from the apex of the cocone `c` to `E₁`, if the cocone `c` is a colimit cocone, then the function `restrictYonedaHomEquiv` from `E₂` to `t` applied to the composition of `k` and `g` is equivalent to the composition of the function `restrictYonedaHomEquiv` from `E₁` to `t` applied to `k`, and the function `restrictedYoneda` from `A` applied to `g`. This demonstrates the naturality of the bijection `restrictYonedaHomEquiv` with respect to the morphism `g`.
More concisely: Given functors A from a small category C to a category ℰ and P from the opposite category of C to Type u₁, if a cocone c for the functor composition of A and the left opposite of πP is a colimit cocone and g is a morphism from an object E₁ to E₂ in ℰ with apex k in c, then the restriction of the Yoneda equivalence from E₂ to the terminal object t is naturally equal to the composition of the restriction of the Yoneda equivalence from E₁ to t and the restriction of A on g.
|
CategoryTheory.coconeOfRepresentable_ι_app
theorem CategoryTheory.coconeOfRepresentable_ι_app :
∀ {C : Type u₁} [inst : CategoryTheory.SmallCategory C] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁))
(j : P.Elementsᵒᵖ),
(CategoryTheory.coconeOfRepresentable P).ι.app j = CategoryTheory.yonedaEquiv.symm j.unop.snd
This theorem provides an explicit formula for the legs of a specific cocone in category theory, namely the `coconeOfRepresentable`. Given a small category `C`, a functor `P` from the opposite of `C` to the universe `Type u₁`, and an object `j` in the opposite of the elements of `P`, the morphism from the apex of the cocone to `j` in the diagram of `coconeOfRepresentable P` is equal to the application of the inverse of the Yoneda equivalence to the second component of the unpacked object `j`. In other words, it describes the specific way in which this cocone is mapped into the diagram of `P`.
More concisely: Given a small category C, a functor P from C^op to Type u₁, and an object j in C, the morphism from the apex of the coconeOfRepresentable P to j is the application of the inverse of the Yoneda embedding to the second component of j.
|