Basic

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

Statistics

Metric	Count
Definitions	0
Theorems preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, preservesHomology_preadditiveCoyonedaObj_of_projective, projective_of_preservesFiniteColimits_preadditiveCoyonedaObj	3
Total	3

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteColimits_preadditiveCoyonedaObj_of_projective 📖	mathematical	—	Limits.PreservesFiniteColimits ModuleCat MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd Abelian.toPreadditive ModuleCat.moduleCategory preadditiveCoyonedaObj	—	Functor.preservesFiniteColimits_of_preservesHomology additive_coyonedaObj preservesHomology_preadditiveCoyonedaObj_of_projective Abelian.hasZeroObject Limits.hasFiniteCoproducts_of_hasFiniteColimits Abelian.hasFiniteColimits Abelian.has_cokernels
preservesHomology_preadditiveCoyonedaObj_of_projective 📖	mathematical	—	Functor.PreservesHomology ModuleCat MulOpposite End Category.toCategoryStruct MulOpposite.instRing Preadditive.instRingEnd Abelian.toPreadditive ModuleCat.moduleCategory Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive preadditiveCoyonedaObj Functor.preservesZeroMorphisms_of_additive additive_coyonedaObj	—	Functor.preservesHomology_of_preservesEpis_and_kernels Functor.preservesZeroMorphisms_of_additive additive_coyonedaObj Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits Limits.PreservesLimits.preservesFiniteLimits preservesLimits_preadditiveCoyonedaObj
projective_of_preservesFiniteColimits_preadditiveCoyonedaObj 📖	mathematical	—	Projective	—	Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj Functor.preservesZeroMorphisms_of_additive additive_coyonedaObj Functor.preservesHomologyOfExact Limits.PreservesLimits.preservesFiniteLimits preservesLimits_preadditiveCoyonedaObj Functor.instPreservesEpimorphisms Abelian.hasZeroObject ModuleCat.instHasZeroObject

---

← Back to Index