Abelian

📁 Source: Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean

Statistics

Metric	Count
Definitions instAbelian	1
Theorems instIsNormalEpiCategory, instIsNormalMonoCategory	2
Total	3

PresheafOfModules

Definitions

Name	Category	Theorems
instAbelian 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsNormalEpiCategory 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory PresheafOfModules instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.kernel.condition CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape evaluation_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits AddCommGrpCat.hasColimitsOfSize evaluation_preservesLimit
instIsNormalMonoCategory 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory PresheafOfModules instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	hasColimit ModuleCat.preservesColimit_restrictScalars AddCommGrpCat.hasColimit UnivLE.small univLE_of_max UnivLE.self ModuleCat.HasColimit.instHasColimit CategoryTheory.Limits.cokernel.condition small_subtype small_Pi CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation evaluation_preservesColimit

---

← Back to Index