Abelian

📁 Source: Mathlib/CategoryTheory/Sites/Abelian.lean

Statistics

Metric	Count
Definitions Abelian, sheafIsAbelian	2
Theorems presheafToSheaf_additive	1
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
Abelian 📖	CompData	—
sheafIsAbelian 📖	CompOp	2 math math: Sheaf.instIsGrothendieckAbelian, Sheaf.isGrothendieckAbelian_of_essentiallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presheafToSheaf_additive 📖	mathematical	—	Functor.Additive Functor Opposite Category.opposite Sheaf Functor.category Sheaf.instCategorySheaf functorCategoryPreadditive Abelian.toPreadditive instPreadditiveSheaf presheafToSheaf instHasWeakSheafifyOfHasSheafify	—	Functor.additive_of_preservesBinaryBiproducts instHasWeakSheafifyOfHasSheafify Abelian.hasBinaryBiproducts Functor.preservesZeroMorphisms_of_preserves_terminal_object Limits.HasZeroObject.instFunctor Abelian.hasZeroObject Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf Limits.preservesBinaryBiproducts_of_preservesBinaryProducts

---

← Back to Index