CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality
theorem CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type v)}
(α : F₁ ⟶ F₂),
(CategoryTheory.CategoryOfElements.map α).op.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F₂) =
(CategoryTheory.CategoryOfElements.toCostructuredArrow F₁).comp (CategoryTheory.CostructuredArrow.map α)
This theorem states that for any category `C` and for any two Covariant functors `F₁` and `F₂` from the opposite of `C` to the category of types, and for any natural transformation `α` from `F₁` to `F₂`, the composition of the functor induced by the opposite of the natural transformation `α` and the functor converting elements of `F₂` to costructured arrows is equal to the composition of the functor converting elements of `F₁` to costructured arrows and the functor induced by `α`. In essence, this theorem asserts the naturality of the equivalence between the opposite of the category of elements and the pair `(yoneda, -)`.
More concisely: For any covariant functors F₁ and F₂ from the opposite of a category C to the category of types, and natural transformation α from F₁ to F₂, the opposites of their induced functors and the functor converting elements of F₂ to constructed arrows are naturally equal to the functor converting elements of F₁ to constructed arrows and their induced functors.
|
CategoryTheory.CategoryOfElements.to_fromCostructuredArrow_eq
theorem CategoryTheory.CategoryOfElements.to_fromCostructuredArrow_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.comp
(CategoryTheory.CategoryOfElements.toCostructuredArrow F) =
CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
This theorem states that for any category `C` and any functor `F` from the opposite of `C` to `Type v`, the composition of the right opposite of the functor resulting from applying `fromCostructuredArrow` to `F` and the functor resulting from applying `toCostructuredArrow` to `F` is equal to the identity functor on the category of costructured arrows with `CategoryTheory.yoneda` and `F`. This means that the process of going 'to' and 'from' costructured arrows via these functors results in no net change, similar to applying an operation and its inverse. This is an important property that supports the equivalence assertion in the comment, as equivalences are expected to have this round-trip property.
More concisely: For any category `C` and functor `F` from the opposite of `C` to `Type v`, the composition of `fromCostructuredArrow` applied to `F` and `toCostructuredArrow` applied to `F` is equal to the identity functor on the category of costructured arrows over `C` with respect to `F`.
|
CategoryTheory.CategoryOfElements.from_toCostructuredArrow_eq
theorem CategoryTheory.CategoryOfElements.from_toCostructuredArrow_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
(CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp.comp
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F) =
CategoryTheory.Functor.id F.Elements
The theorem `CategoryTheory.CategoryOfElements.from_toCostructuredArrow_eq` states that for any category `C` and functor `F` from the opposite of `C` to the category of types, the composition of the 'toCostructuredArrow' operation on `F` followed by the 'fromCostructuredArrow' operation on `F` is equivalent to the identity functor on the elements of `F`. In other words, these two operations, 'toCostructuredArrow' and 'fromCostructuredArrow', form an equivalence, or isomorphism, of categories, demonstrating a key property of the equivalence between the opposite of the category of elements of `F` and the functor category `(yoneda, F)`.
More concisely: For any category C and functor F from the opposite of C to Type, the compositions of F.toCostructuredArrow and F.fromCostructuredArrow are equal to the identity functor on the elements of F.
|