Basic

📁 Source: Mathlib/CategoryTheory/Abelian/Injective/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems injective_of_preservesFiniteColimits_preadditiveYonedaObj, preservesFiniteColimits_preadditiveYonedaObj_of_injective, preservesHomology_preadditiveYonedaObj_of_injective	3
Total	3

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_of_preservesFiniteColimits_preadditiveYonedaObj 📖	mathematical	—	Injective	—	Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' Functor.preservesZeroMorphisms_of_additive additive_yonedaObj Functor.preservesHomologyOfExact Limits.PreservesLimits.preservesFiniteLimits preservesLimits_preadditiveYonedaObj Functor.instPreservesEpimorphisms Limits.hasZeroObject_op Abelian.hasZeroObject ModuleCat.instHasZeroObject
preservesFiniteColimits_preadditiveYonedaObj_of_injective 📖	mathematical	—	Limits.PreservesFiniteColimits Opposite Category.opposite ModuleCat End Category.toCategoryStruct Preadditive.instRingEnd Abelian.toPreadditive ModuleCat.moduleCategory preadditiveYonedaObj	—	Functor.preservesFiniteColimits_of_preservesHomology additive_yonedaObj preservesHomology_preadditiveYonedaObj_of_injective Limits.hasZeroObject_op Abelian.hasZeroObject Limits.hasFiniteCoproducts_of_hasFiniteColimits Limits.hasFiniteColimits_opposite Abelian.hasFiniteLimits Abelian.has_cokernels
preservesHomology_preadditiveYonedaObj_of_injective 📖	mathematical	—	Functor.PreservesHomology Opposite ModuleCat End Category.toCategoryStruct Preadditive.instRingEnd Abelian.toPreadditive Category.opposite ModuleCat.moduleCategory Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive preadditiveYonedaObj Functor.preservesZeroMorphisms_of_additive instPreadditiveOpposite additive_yonedaObj	—	Functor.preservesHomology_of_preservesEpis_and_kernels Functor.preservesZeroMorphisms_of_additive additive_yonedaObj Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits Limits.PreservesLimits.preservesFiniteLimits preservesLimits_preadditiveYonedaObj

---

← Back to Index