mem_canonicalEquiv_apply — Mathlib

English

Membership in the canonicalEquiv image equals the existence of a representative from the original ideal after localization.

Русский

Принадлежность к образу canonicalEquiv равна существованию представителя из исходного идеала после локализации.

LaTeX

$$$ x \\in canonicalEquiv S P P' I \\iff \\exists y \\in I, \\ IsLocalization.map P' (RingHom.id R) (y) = x $$$

Lean4

@[simp]
theorem mem_canonicalEquiv_apply {I : FractionalIdeal S P} {x : P'} :
    x ∈ canonicalEquiv S P P' I ↔
      ∃ y ∈ I,
        IsLocalization.map P' (RingHom.id R) (fun y (hy : y ∈ S) => show RingHom.id R y ∈ S from hy) (y : P) = x :=
  by
  rw [canonicalEquiv, mapEquiv_apply, mem_map]
  exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

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