idealMap_isLocalizedModule — Mathlib

English

For any ideal I of R, the span of I in a localization by M is the localization of I at M; i.e., the localized image of I coincides with the localization of I.

Русский

Для любого идеала $I$ кольца $R$ локализация по $M$ порождает локализацию $I$ по $M$; то есть локализация образа $I$ совпадает с локализацией $I$.

LaTeX

$$$\\operatorname{Loc}_M(I) = I_{M}$$$

Lean4

/-- The span of `I` in a localization of `R` at `M` is the localization of `I` at `M`. -/
-- TODO: golf using `Ideal.localized'_eq_map`

instance idealMap_isLocalizedModule (I : Ideal R) : IsLocalizedModule M (Algebra.idealMap I (S := S))
    where
  map_units
    x :=
    (Module.End.isUnit_iff _).mpr
      ⟨fun a b e ↦ Subtype.ext ((map_units S x).mul_right_injective (by simpa [Algebra.smul_def] using congr(($e).1))),
        fun a ↦
        ⟨⟨_, Ideal.mul_mem_left _ (map_units S x).unit⁻¹.1 a.2⟩, Subtype.ext (by simp [Algebra.smul_def, ← mul_assoc])⟩⟩
  surj
    y :=
    have ⟨x, hx⟩ := (mem_map_algebraMap_iff M S).mp y.property
    ⟨x, Subtype.ext (by simp [Submonoid.smul_def, Algebra.smul_def, mul_comm, hx])⟩
  exists_of_eq h := ⟨_, Subtype.ext (exists_of_eq congr(($h).1)).choose_spec⟩

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