Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Sites/SheafCohomology/Basic.lean

Statistics

Metric	Count
Definitions `H`, `H'`, `cohomologyFunctor`, `cohomologyPresheaf`, `cohomologyPresheafFunctor`, `instAddCommGroupH`, `instAdditiveAddCommGrpCatCohomologyFunctor`	7
Theorems `cohomologyFunctor_obj`, `subsingleton_H_of_isZero`	2
Total	9

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`H` 📖	CompOp	2 math math: `cohomologyFunctor_obj`, `subsingleton_H_of_isZero`
`H'` 📖	CompOp	10 math math: `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply`
`cohomologyFunctor` 📖	CompOp	1 math math: `cohomologyFunctor_obj`
`cohomologyPresheaf` 📖	CompOp	2 math math: `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply`
`cohomologyPresheafFunctor` 📖	CompOp	—
`instAddCommGroupH` 📖	CompOp	—
`instAdditiveAddCommGrpCatCohomologyFunctor` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cohomologyFunctor_obj` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`AddCommGrpCat.carrier` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `cohomologyFunctor` `H`	—	—
`subsingleton_H_of_isZero` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian` `CategoryTheory.Limits.IsZero`	`H`	—	`cohomologyFunctor_obj` `AddCommGrpCat.subsingleton_of_isZero` `CategoryTheory.Functor.map_isZero` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`

---

← Back to Index