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	5 math math: GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, Sheaf.instIsGrothendieckAbelian, GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, Sheaf.isGrothendieckAbelian_of_essentiallySmall, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presheafToSheaf_additive 📖	mathematical	—	Functor.Additive Functor Opposite Category.opposite Sheaf Functor.category ObjectProperty.FullSubcategory.category Presheaf.IsSheaf functorCategoryPreadditive Abelian.toPreadditive Preadditive.fullSubcategory 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