Theorems · Definition · category theory
CategoryTheory.preadditiveYonedaObj
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Preadditive C] → (Y : C) → CategoryTheory.Functor Cᵒᵖ (ModuleCat (CategoryTheory.End Y))The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an
object X to the End Y-module of morphisms X ⟶ Y.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- Opposite.unopproof · cited by 2,231
- ModuleCatstatement · cited by 1,429
- Quiver.Hom.unopproof · cited by 903
- ModuleCat.ofproof · cited by 594
- ModuleCat.ofHomproof · cited by 200
- CategoryTheory.Endstatement and proof · cited by 169
Cited by8
Results whose statement or proof uses this declaration.
- CategoryTheory.preadditiveYonedaproof · cited by 17
- CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj'statement and proof · cited by 1
- CategoryTheory.preadditiveYoneda_objstatement · cited by 1
- CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObjstatement and proof · cited by 0
- CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObjstatement and proof · cited by 0
- CategoryTheory.preadditiveYonedaMap_appstatement · cited by 0
- CategoryTheory.preadditiveYonedaObj_mapstatement and proof · cited by 0
- CategoryTheory.preadditiveYonedaObj_obj_carrierstatement and proof · cited by 0