Yoneda

📁 Source: Mathlib/CategoryTheory/Triangulated/Yoneda.lean

Statistics

Metric	Count
Definitions instShiftSequenceAddCommGrpCatObjOppositeFunctorPreadditiveCoyonedaInt, instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt	2
Theorems instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda, instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda, preadditiveCoyoneda_homologySequenceδ_apply, preadditiveYoneda_homologySequenceδ_apply, preadditiveYoneda_map_distinguished, preadditiveYoneda_shiftMap_apply	6
Total	8

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
instShiftSequenceAddCommGrpCatObjOppositeFunctorPreadditiveCoyonedaInt 📖	CompOp	2 math math: CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, preadditiveCoyoneda_homologySequenceδ_apply
instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt 📖	CompOp	3 math math: CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, preadditiveYoneda_homologySequenceδ_apply, preadditiveYoneda_shiftMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsHomological AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveCoyoneda AddCommGrpCat.instAbelian	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.additive_coyonedaObj' CategoryTheory.ShortComplex.ab_exact_iff Triangle.coyoneda_exact₂
instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsHomological Opposite AddCommGrpCat CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt AddCommGrpCat.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveYoneda CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite Opposite.instAdditiveOppositeShiftFunctorInt Opposite.instOpposite AddCommGrpCat.instAbelian	—	CategoryTheory.Limits.hasZeroObject_op Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.additive_yonedaObj' CategoryTheory.ShortComplex.ab_exact_iff Triangle.yoneda_exact₂ unop_distinguished
preadditiveCoyoneda_homologySequenceδ_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.shift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveCoyoneda Int.instAddMonoid instShiftSequenceAddCommGrpCatObjOppositeFunctorPreadditiveCoyonedaInt Triangle.obj₃ Triangle.obj₁ AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.homologySequenceδ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.shiftFunctor CategoryTheory.Functor.map Triangle.mor₃ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.Category.assoc
preadditiveYoneda_homologySequenceδ_apply 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.shift CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveYoneda Opposite.instHasShiftOppositeInt instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt Triangle.obj₃ Triangle triangleCategory CategoryTheory.Equivalence.functor triangleOpEquivalence Opposite.op Triangle.obj₁ AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.homologySequenceδ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Triangle.mor₃ CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	preadditiveYoneda_shiftMap_apply Equiv.injective Equiv.apply_symm_apply
preadditiveYoneda_map_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Triangle Set Set.instMembership distinguishedTriangles	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive CategoryTheory.ShortComplex.map Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op shortComplexOfDistTriangle CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveYoneda CategoryTheory.Functor.IsHomological.toPreservesZeroMorphisms Opposite.instHasShiftOppositeInt CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite Opposite.instAdditiveOppositeShiftFunctorInt Opposite.instOpposite AddCommGrpCat.instAbelian instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda	—	CategoryTheory.Functor.map_distinguished_op_exact instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda
preadditiveYoneda_shiftMap_apply 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.shift CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveYoneda Opposite.instHasShiftOppositeInt instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.shiftMap CategoryTheory.ShiftedHom.comp Opposite.unop Equiv CategoryTheory.ShiftedHom Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.ShiftedHom.opEquiv	—	CategoryTheory.ShiftedHom.opEquiv_symm_apply_comp

---

← Back to Index