ofSelfLERadical — Mathlib

English

Local cohomology modules depend only on the radical of the ideals; hence if J.radical = K.radical then J i ≅ K i for all i.

Русский

Локальная когомология зависит только от радикала идеалов; следовательно, если J.radical = K.radical, то J_i ≅ K_i для всех i.

LaTeX

$$$\\text{isoOfSameRadical } J K i : \\text{localCohomology } J i \\cong \\text{localCohomology } K i$$$

Lean4

/-- Local cohomology as the direct limit of `Ext^i(R/J', M)` over *all* ideals `J'` with radical
containing `J`. -/
def ofSelfLERadical (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
  ofDiagram.{u} (selfLERadicalDiagram.{u} J) i

Похожие утверждения