English
Local cohomology defined via the self-le radical diagram is isomorphic to the standard local cohomology for Noetherian rings.
Русский
Локальная когомология, определяемая через диаграмму selfLERadical, изоморфна стандартной локальной когомогенности для Нётеровых колец.
LaTeX
$$$\\text{localCohomology.ofSelfLERadical } J i \\cong \\text{localCohomology. } J i$$$
Lean4
/-- `localCohomology J i` is `i`-th the local cohomology module of a module `M` over
a commutative ring `R` with support in the ideal `J` of `R`, defined as the direct limit
of `Ext^i(R/J^t, M)` over all powers `t : ℕ`. -/
def localCohomology (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
ofDiagram (idealPowersDiagram J) i
