isoOfSameRadical — Mathlib

English

Local cohomology agrees on ideals with the same radical; i.e., LocCoh(J,i) ≅ LocCoh(K,i) if J.radical = K.radical.

Русский

Локальная когомология согласуется на идеалах с одинаковым радикалом; LocCoh(J,i) ≅ LocCoh(K,i) при J.radical = K.radical.

LaTeX

$$isoOfSameRadical J K i$$

Lean4

/-- Local cohomology agrees on ideals with the same radical. -/
def isoOfSameRadical [IsNoetherian R R] (hJK : J.radical = K.radical) (i : ℕ) :
    localCohomology J i ≅ localCohomology K i :=
  (isoSelfLERadical J i).symm ≪≫ SelfLERadical.isoOfSameRadical hJK i ≪≫ isoSelfLERadical K i

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