Documentation Verification Report

ElladicCohomology

📁 Source: Mathlib/AlgebraicGeometry/Sites/ElladicCohomology.lean

Statistics

Metric	Count
Definitions `EllAdicCohomology`, `ellAdicSheaf`, `instAddCommGroupEllAdicCohomology`	3
Theorems `instIsGrothendieckAbelianSheafProEtTopologyAb`, `instSubsingletonEllAdicCohomologyOfIsEmptyCarrierCarrierCommRingCat`, `isZero_ellAdicSheaf_of_isEmpty`	3
Total	6

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`EllAdicCohomology` 📖	CompOp	1 math math: `instSubsingletonEllAdicCohomologyOfIsEmptyCarrierCarrierCommRingCat`
`ellAdicSheaf` 📖	CompOp	1 math math: `isZero_ellAdicSheaf_of_isEmpty`
`instAddCommGroupEllAdicCohomology` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsGrothendieckAbelianSheafProEtTopologyAb` 📖	mathematical	—	`CategoryTheory.IsGrothendieckAbelian` `CategoryTheory.Sheaf` `ProEt` `instCategoryProEt` `ProEt.topology` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `AddCommGrpCat.hasLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `AddCommGrpCat` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `UnivLE.small` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `CategoryTheory.GrothendieckTopology.Cover` `Preorder.smallCategory` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits`	—	`CategoryTheory.essentiallySmall_of_small_of_locallySmall` `UnivLE.small` `UnivLE.self` `CategoryTheory.locallySmall_of_univLE` `univLE_of_max` `CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall` `instIsGrothendieckAbelianAddCommGrpCat` `AddCommGrpCat.hasLimitsOfShape` `CategoryTheory.StructuredArrow.instSmallOfLocallySmall` `Opposite.small` `CategoryTheory.instLocallySmallOpposite` `CategoryTheory.locallySmall_of_essentiallySmall` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` `CategoryTheory.Functor.IsLocallyFull.of_full` `CategoryTheory.Equivalence.full_inverse` `CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Functor.IsLocallyFaithful.of_faithful` `CategoryTheory.Equivalence.faithful_inverse` `AddCommGrpCat.hasLimit` `small_subtype` `small_Pi` `AddCommGrpCat.hasColimitsOfShape` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits` `CategoryTheory.Limits.hasCountableLimits_of_hasLimits` `AddCommGrpCat.hasLimits`
`instSubsingletonEllAdicCohomologyOfIsEmptyCarrierCarrierCommRingCat` 📖	mathematical	—	`EllAdicCohomology`	—	`CategoryTheory.Sheaf.subsingleton_H_of_isZero` `CategoryTheory.Functor.map_isZero` `CategoryTheory.Functor.preservesZeroMorphisms_of_full` `CategoryTheory.instFullSheafSheafComposeOfFaithful` `AddCommGrpCat.instFullUliftFunctor` `AddCommGrpCat.instFaithfulUliftFunctor` `isZero_ellAdicSheaf_of_isEmpty`
`isZero_ellAdicSheaf_of_isEmpty` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `CategoryTheory.Sheaf` `ProEt` `instCategoryProEt` `ProEt.topology` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `ellAdicSheaf`	—	`CategoryTheory.Limits.IsTerminal.isZero` `ProEt.topology_eq_top_of_isEmpty`

---

← Back to Index