Basic

📁 Source: Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean

Statistics

Metric	Count
Definitions preadditiveCoyonedaIso, preadditiveCoyoneda, preadditiveCoyonedaObj, preadditiveYoneda, preadditiveYonedaMap, preadditiveYonedaObj	6
Theorems additive_coyonedaObj, additive_coyonedaObj', additive_yonedaObj, additive_yonedaObj', faithful_preadditiveCoyoneda, faithful_preadditiveYoneda, full_preadditiveCoyoneda, full_preadditiveYoneda, preadditiveCoyonedaObj_map, preadditiveCoyonedaObj_obj_carrier, preadditiveCoyonedaObj_obj_isAddCommGroup, preadditiveCoyonedaObj_obj_isModule, preadditiveCoyoneda_obj, preadditiveYonedaMap_app, preadditiveYonedaObj_map, preadditiveYonedaObj_obj_carrier, preadditiveYonedaObj_obj_isAddCommGroup, preadditiveYonedaObj_obj_isModule, preadditiveYoneda_obj, whiskering_preadditiveCoyoneda, whiskering_preadditiveYoneda	21
Total	27

AddCommGrpCat

Definitions

Name	Category	Theorems
preadditiveCoyonedaIso 📖	CompOp	—

CategoryTheory

Definitions

Name	Category	Theorems
preadditiveCoyoneda 📖	CompOp	12 math math: isSeparator_iff_faithful_preadditiveCoyoneda, Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, faithful_preadditiveCoyoneda, preservesLimits_preadditiveCoyoneda_obj, whiskering_linearCoyoneda₂, additive_coyonedaObj', full_preadditiveCoyoneda, Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj, Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda, preadditiveCoyoneda_obj, Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, whiskering_preadditiveCoyoneda
preadditiveCoyonedaObj 📖	CompOp	16 math math: preadditiveCoyonedaObj_map, IsGrothendieckAbelian.GabrielPopescu.full, isSeparator_iff_faithful_preadditiveCoyonedaObj, Abelian.full_comp_preadditiveCoyonedaObj, IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, preservesHomology_preadditiveCoyonedaObj_of_projective, Abelian.preadditiveCoyonedaObj_map_surjective, preadditiveCoyonedaObj_obj_carrier, preadditiveCoyonedaObj_obj_isModule, preservesLimits_preadditiveCoyonedaObj, additive_coyonedaObj, preadditiveCoyoneda_obj, preadditiveCoyonedaObj_obj_isAddCommGroup, IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj
preadditiveYoneda 📖	CompOp	17 math math: isCoseparator_iff_faithful_preadditiveYoneda, Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, preadditiveYoneda_obj, Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, preadditiveYonedaMap_app, Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda, additive_yonedaObj', faithful_preadditiveYoneda, Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, whiskering_preadditiveYoneda, preservesLimits_preadditiveYoneda_obj, Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, full_preadditiveYoneda, Pretriangulated.preadditiveYoneda_shiftMap_apply, whiskering_linearYoneda₂, Pretriangulated.preadditiveYoneda_map_distinguished, Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj
preadditiveYonedaMap 📖	CompOp	1 math math: preadditiveYonedaMap_app
preadditiveYonedaObj 📖	CompOp	12 math math: additive_yonedaObj, preadditiveYonedaObj_obj_carrier, preadditiveYoneda_obj, preadditiveYonedaMap_app, preadditiveYonedaObj_obj_isModule, Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj', preservesFiniteColimits_preadditiveYonedaObj_of_injective, preservesLimits_preadditiveYonedaObj, preservesHomology_preadditiveYonedaObj_of_injective, preadditiveYonedaObj_obj_isAddCommGroup, isCoseparator_iff_faithful_preadditiveYonedaObj, preadditiveYonedaObj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additive_coyonedaObj 📖	mathematical	—	Functor.Additive ModuleCat MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd ModuleCat.moduleCategory ModuleCat.instPreadditive preadditiveCoyonedaObj	—	Preadditive.add_comp Preadditive.comp_add
additive_coyonedaObj' 📖	mathematical	—	Functor.Additive AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive Functor.obj Opposite Category.opposite Functor Functor.category preadditiveCoyoneda	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Preadditive.add_comp Preadditive.comp_add
additive_yonedaObj 📖	mathematical	—	Functor.Additive Opposite ModuleCat End Category.toCategoryStruct Preadditive.instRingEnd Category.opposite ModuleCat.moduleCategory instPreadditiveOpposite ModuleCat.instPreadditive preadditiveYonedaObj	—	Preadditive.add_comp
additive_yonedaObj' 📖	mathematical	—	Functor.Additive Opposite AddCommGrpCat Category.opposite AddCommGrpCat.instCategory instPreadditiveOpposite AddCommGrpCat.instPreadditive Functor.obj Functor Functor.category preadditiveYoneda	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Preadditive.add_comp
faithful_preadditiveCoyoneda 📖	mathematical	—	Functor.Faithful Opposite Category.opposite Functor AddCommGrpCat AddCommGrpCat.instCategory Functor.category preadditiveCoyoneda	—	Functor.Faithful.of_comp_eq Coyoneda.coyoneda_faithful whiskering_preadditiveCoyoneda
faithful_preadditiveYoneda 📖	mathematical	—	Functor.Faithful Functor Opposite Category.opposite AddCommGrpCat AddCommGrpCat.instCategory Functor.category preadditiveYoneda	—	Functor.Faithful.of_comp_eq Yoneda.yoneda_faithful whiskering_preadditiveYoneda
full_preadditiveCoyoneda 📖	mathematical	—	Functor.Full Opposite Category.opposite Functor AddCommGrpCat AddCommGrpCat.instCategory Functor.category preadditiveCoyoneda	—	Coyoneda.coyoneda_full Functor.Full.of_comp_faithful Functor.faithful_whiskeringRight_obj instFaithfulForget
full_preadditiveYoneda 📖	mathematical	—	Functor.Full Functor Opposite Category.opposite AddCommGrpCat AddCommGrpCat.instCategory Functor.category preadditiveYoneda	—	Yoneda.yoneda_full Functor.Full.of_comp_faithful Functor.faithful_whiskeringRight_obj instFaithfulForget
preadditiveCoyonedaObj_map 📖	mathematical	—	Functor.map ModuleCat MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd ModuleCat.moduleCategory preadditiveCoyonedaObj ModuleCat.ofHom Quiver.Hom CategoryStruct.toQuiver Preadditive.homGroup moduleEndLeft Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup CategoryStruct.comp Preadditive.add_comp	—	—
preadditiveCoyonedaObj_obj_carrier 📖	mathematical	—	ModuleCat.carrier MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd Functor.obj ModuleCat ModuleCat.moduleCategory preadditiveCoyonedaObj Quiver.Hom CategoryStruct.toQuiver	—	—
preadditiveCoyonedaObj_obj_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd Functor.obj ModuleCat ModuleCat.moduleCategory preadditiveCoyonedaObj Preadditive.homGroup	—	—
preadditiveCoyonedaObj_obj_isModule 📖	mathematical	—	ModuleCat.isModule MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd Functor.obj ModuleCat ModuleCat.moduleCategory preadditiveCoyonedaObj moduleEndLeft	—	—
preadditiveCoyoneda_obj 📖	mathematical	—	Functor.obj Opposite Category.opposite Functor AddCommGrpCat AddCommGrpCat.instCategory Functor.category preadditiveCoyoneda Functor.comp ModuleCat MulOpposite End Category.toCategoryStruct Opposite.unop MulOpposite.instRing Preadditive.instRingEnd ModuleCat.moduleCategory preadditiveCoyonedaObj forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier ModuleCat.hasForgetToAddCommGroup	—	—
preadditiveYonedaMap_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite AddCommGrpCat AddCommGrpCat.instCategory Functor.obj Functor Functor.category preadditiveYoneda Functor.comp Functor.op preadditiveYonedaMap AddCommGrpCat.ofHom ModuleCat.carrier End Category.toCategoryStruct Preadditive.instRingEnd ModuleCat ModuleCat.moduleCategory preadditiveYonedaObj ModuleCat.isAddCommGroup Functor.mapAddHom Opposite.unop	—	—
preadditiveYonedaObj_map 📖	mathematical	—	Functor.map Opposite Category.opposite ModuleCat End Category.toCategoryStruct Preadditive.instRingEnd ModuleCat.moduleCategory preadditiveYonedaObj ModuleCat.ofHom Quiver.Hom CategoryStruct.toQuiver Opposite.unop Preadditive.homGroup Preadditive.moduleEndRight Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup CategoryStruct.comp Quiver.Hom.unop	—	—
preadditiveYonedaObj_obj_carrier 📖	mathematical	—	ModuleCat.carrier End Category.toCategoryStruct Preadditive.instRingEnd Functor.obj Opposite Category.opposite ModuleCat ModuleCat.moduleCategory preadditiveYonedaObj Quiver.Hom CategoryStruct.toQuiver Opposite.unop	—	—
preadditiveYonedaObj_obj_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup End Category.toCategoryStruct Preadditive.instRingEnd Functor.obj Opposite Category.opposite ModuleCat ModuleCat.moduleCategory preadditiveYonedaObj Preadditive.homGroup Opposite.unop	—	—
preadditiveYonedaObj_obj_isModule 📖	mathematical	—	ModuleCat.isModule End Category.toCategoryStruct Preadditive.instRingEnd Functor.obj Opposite Category.opposite ModuleCat ModuleCat.moduleCategory preadditiveYonedaObj Preadditive.moduleEndRight Opposite.unop	—	—
preadditiveYoneda_obj 📖	mathematical	—	Functor.obj Functor Opposite Category.opposite AddCommGrpCat AddCommGrpCat.instCategory Functor.category preadditiveYoneda Functor.comp ModuleCat End Category.toCategoryStruct Preadditive.instRingEnd ModuleCat.moduleCategory preadditiveYonedaObj forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier ModuleCat.hasForgetToAddCommGroup	—	—
whiskering_preadditiveCoyoneda 📖	mathematical	—	Functor.comp Opposite Category.opposite Functor AddCommGrpCat AddCommGrpCat.instCategory Functor.category types preadditiveCoyoneda Functor.obj Functor.whiskeringRight forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier coyoneda	—	—
whiskering_preadditiveYoneda 📖	mathematical	—	Functor.comp Functor Opposite Category.opposite AddCommGrpCat AddCommGrpCat.instCategory Functor.category types preadditiveYoneda Functor.obj Functor.whiskeringRight forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier yoneda	—	—

---

← Back to Index