CategoryTheory.OverPresheafAux.YonedaCollection.mk_fst
theorem CategoryTheory.OverPresheafAux.YonedaCollection.mk_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
{F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
(s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))),
(CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).fst = s
This theorem states that for any category `C`, functor `A` from the opposite category of `C` to the category of types, a functor `F` from the opposite category of costructured arrows from the Yoneda embedding to `A` to the category of types, and an object `X` of `C`, if we have a natural transformation `s` from the Yoneda functor at `X` to `A`, and an object `x` of the functor `F` at the opposite of a costructured arrow constructed from `s`, then the first component of the YonedaCollection constructed from `s` and `x` is `s`. In other words, the first component of a YonedaCollection is the natural transformation used to construct it.
More concisely: For any category C, functor A from C��opp to Type, functor F from (C��opp ⥤ Arrows (Yoneda C)) to Type, object X of C, natural transformation s from Yoneda X to A, and object x of F at the opposite of a constructed arrow from s, the first component of the YonedaCollection constructed from s and x is s.
|
CategoryTheory.OverPresheafAux.OverArrows.app_val
theorem CategoryTheory.OverPresheafAux.OverArrows.app_val :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
{X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} (p : CategoryTheory.OverPresheafAux.OverArrows η s),
η.app (Opposite.op X) p.val = CategoryTheory.yonedaEquiv s
This theorem states the defining property of the function `OverArrows.val` in the category theory context. Specifically, it says that for any object `X` in a category `C`, any functors `A` and `F` from the opposite of `C` to `Type v`, a natural transformation `η` from `F` to `A`, a natural transformation `s` from the Yoneda embedding of `X` to `A`, and an element `p` of type `OverArrows η s`, the application of `η` at `X` acting on `OverArrows.val p` is equivalent to the Yoneda equivalence of `s`. In other words, it gives a condition that the "value" of an element of the `OverArrows` construction under `η` corresponds to its representation under the Yoneda embedding.
More concisely: For any object X in a category C, functors A and F from the opposite of C to Type v, natural transformations η from F to A and s from the Yoneda embedding of X to A, and an element p of type OverArrows η s, we have η (X (OverArrows.val p)) ≈ s.
|
CategoryTheory.OverPresheafAux.OverArrows.ext
theorem CategoryTheory.OverPresheafAux.OverArrows.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
{X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {u v : CategoryTheory.OverPresheafAux.OverArrows η s},
u.val = v.val → u = v
The theorem `CategoryTheory.OverPresheafAux.OverArrows.ext` states that for any category `C`, functors `A` and `F` from the opposite of `C` to `Type v`, morphism `η` from `F` to `A`, object `X` in `C`, morphism `s` from the Yoneda embedding of `X` to `A`, and for any two elements `u` and `v` of the type `CategoryTheory.OverPresheafAux.OverArrows η s`, if the value of `u` and `v` under the `CategoryTheory.OverPresheafAux.OverArrows.val` function are equal, then `u` and `v` must be equal. In other words, this theorem asserts that the function `CategoryTheory.OverPresheafAux.OverArrows.val` is injective.
More concisely: For any category C, functors A and F from C\^op to Type v, morphism η from F to A, and objects X in C, if the Yoneda morphism s from X to A and morphisms u and v in the over-category of arrows from η to s have equal images under the val function, then u and v are equal.
|
CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst
theorem CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
{F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
(s : CategoryTheory.yoneda.obj X ⟶ A)
(p : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s),
CategoryTheory.OverPresheafAux.YonedaCollection.fst p.val = s
The theorem `CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst` states that for any category `C`, functor `A` from the opposite of `C` to the type `v`, functor `F` from the opposite of the category of costructured arrows from `yoneda A` to `A` to type `v`, and object `X` in `C`, the first component of the value of any element `p` in the OverArrows of the natural transformation from `yonedaCollectionPresheaf A F` to `A` applied to a morphism `s` from `yoneda.obj X` to `A`, is equal to `s`. This theorem is using the Yoneda lemma to establish a relationship between the components of elements in a Yoneda collection and the morphisms in the category.
More concisely: For any category C, functor A, functor F, object X in C, and element p in the OverArrows of the natural transformation from yonedaCollectionPresheaf A F to A at the morphism s from yoneda.obj X to A, the first component of p equals s.
|