English
Local cohomology with respect to J depends only on the radical of J; hence if J.radical = K.radical then LocCoh(J,i) ≅ LocCoh(K,i).
Русский
Локальная когомология по J зависит только от радикала J; следовательно LocCoh(J,i) ≅ LocCoh(K,i) при J.radical = K.radical.
LaTeX
$$isoOfSameRadical J K i$$
Lean4
/-- Local cohomology (defined in terms of powers of `J`) agrees with local
cohomology computed over all ideals with radical containing `J`. -/
def isoSelfLERadical (J : Ideal.{u} R) [IsNoetherian.{u, u} R R] (i : ℕ) :
localCohomology.ofSelfLERadical.{u} J i ≅ localCohomology.{u} J i :=
(localCohomology.isoOfFinal.{u, u, 0} (idealPowersToSelfLERadical.{u} J) (selfLERadicalDiagram.{u} J) i).symm ≪≫
HasColimit.isoOfNatIso.{0, 0, u + 1, u + 1} (Iso.refl.{u + 1, u + 1} _)
