CategoryTheory.whiskering_preadditiveCoyoneda
theorem CategoryTheory.whiskering_preadditiveCoyoneda :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
CategoryTheory.preadditiveCoyoneda.comp
((CategoryTheory.whiskeringRight C AddCommGroupCat (Type v)).obj (CategoryTheory.forget AddCommGroupCat)) =
CategoryTheory.coyoneda
The theorem `CategoryTheory.whiskering_preadditiveCoyoneda` states that for any category `C` that is preadditive (i.e., its hom-sets have the structure of an additive commutative group and composition of morphisms distributes over addition), composing the preadditive yoneda embedding with the forgetful functor (which forgets the additive group structure and views the morphism sets just as sets) gives us the regular Yoneda embedding. This means that the process of 'forgetting' the additive structure does not affect the essential nature of the Yoneda embedding, which relates a category to its presheaves. Here, `AddCommGroupCat` is the category of additive commutative groups and group morphisms, `CategoryTheory.forget` is the functor that forgets some structure, and `CategoryTheory.coyoneda` is the co-Yoneda embedding functor.
More concisely: The preadditive Yoneda embedding is equal to the regular Yoneda embedding after forgetting the additive group structure in a preadditive category.
|
CategoryTheory.whiskering_preadditiveYoneda
theorem CategoryTheory.whiskering_preadditiveYoneda :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
CategoryTheory.preadditiveYoneda.comp
((CategoryTheory.whiskeringRight Cᵒᵖ AddCommGroupCat (Type v)).obj (CategoryTheory.forget AddCommGroupCat)) =
CategoryTheory.yoneda
The theorem `CategoryTheory.whiskering_preadditiveYoneda` asserts that for any category `C` of type `u` that is both a category and preadditive, the composition of the preadditive Yoneda embedding and the forgetful functor (when applied to the category of additive commutative groups) is equivalent to the regular Yoneda embedding. Here, whiskering refers to the process of 'decorating' or modifying a functor with additional structure. In this case, the theorem relates the process of adding preadditive structure to the Yoneda embedding and then forgetting about the added structure back to the original Yoneda embedding.
More concisely: For any preadditive category `C`, the preadditive Yoneda embedding and the forgetful functor from the category of additive commutative groups to `C`, followed by the regular Yoneda embedding, are equivalent.
|