isoOfSameRadical — Mathlib

English

If two ideals have the same radical, the local cohomology objects are canonically isomorphic for all i.

Русский

Если два идеала имеют один и тот же радикал, локальная когомология для них изоморфна для всех i.

LaTeX

$$isoOfSameRadical J K i$$

Lean4

/-- The natural isomorphism between local cohomology defined using the `of_self_le_radical`
diagram, assuming `J.radical = K.radical`. -/
def isoOfSameRadical (hJK : J.radical = K.radical) (i : ℕ) : ofSelfLERadical J i ≅ ofSelfLERadical K i :=
  (isoOfFinal.{u, u, u} (SelfLERadical.cast hJK.symm) _ _).symm

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