Documentation Verification Report

LocalCohomology

📁 Source: Mathlib/Algebra/Homology/LocalCohomology.lean

Statistics

Metric	Count
Definitions `localCohomology`, `SelfLERadical`, `cast`, `castEquivalence`, `inhabited`, `isoOfSameRadical`, `diagram`, `diagramComp`, `idealPowersDiagram`, `idealPowersToSelfLERadical`, `instCategorySelfLERadical`, `isoOfFinal`, `isoOfSameRadical`, `isoSelfLERadical`, `ofDiagram`, `ofSelfLERadical`, `ringModIdeals`, `selfLERadicalDiagram`	18
Theorems `cast_isEquivalence`, `hasColimitDiagram`, `ideal_powers_initial`	3
Total	21

(root)

Definitions

Name	Category	Theorems
`localCohomology` 📖	CompOp	—

localCohomology

Definitions

Name	Category	Theorems
`SelfLERadical` 📖	CompOp	2 math math: `ideal_powers_initial`, `SelfLERadical.cast_isEquivalence`
`diagram` 📖	CompOp	1 math math: `hasColimitDiagram`
`diagramComp` 📖	CompOp	—
`idealPowersDiagram` 📖	CompOp	—
`idealPowersToSelfLERadical` 📖	CompOp	1 math math: `ideal_powers_initial`
`instCategorySelfLERadical` 📖	CompOp	2 math math: `ideal_powers_initial`, `SelfLERadical.cast_isEquivalence`
`isoOfFinal` 📖	CompOp	—
`isoOfSameRadical` 📖	CompOp	—
`isoSelfLERadical` 📖	CompOp	—
`ofDiagram` 📖	CompOp	—
`ofSelfLERadical` 📖	CompOp	—
`ringModIdeals` 📖	CompOp	—
`selfLERadicalDiagram` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimitDiagram` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.Functor.category` `diagram`	—	`CategoryTheory.Limits.functorCategoryHasColimit` `ModuleCat.HasColimit.instHasColimit` `AddCommGrpCat.hasColimit` `Opposite.small` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`ideal_powers_initial` 📖	mathematical	—	`CategoryTheory.Functor.Initial` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Nat.instPreorder` `SelfLERadical` `instCategorySelfLERadical` `idealPowersToSelfLERadical`	—	`CategoryTheory.zigzag_isConnected` `IsScalarTower.right` `Ideal.exists_pow_le_of_le_radical_of_fg` `CategoryTheory.ObjectProperty.FullSubcategory.property` `isNoetherian_def` `Relation.ReflTransGen.single` `le_total`

localCohomology.SelfLERadical

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	1 math math: `cast_isEquivalence`
`castEquivalence` 📖	CompOp	—
`inhabited` 📖	CompOp	—
`isoOfSameRadical` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_isEquivalence` 📖	mathematical	`Ideal.radical` `CommRing.toCommSemiring`	`CategoryTheory.Functor.IsEquivalence` `localCohomology.SelfLERadical` `localCohomology.instCategorySelfLERadical` `cast`	—	`CategoryTheory.Equivalence.isEquivalence_functor`

---

← Back to Index