symm_apply_mem_of_equiv_iff — Mathlib

English

Let f: R ≃+* S be a ring isomorphism and I an ideal of R. For every y in S, y belongs to the image I mapped along f precisely when its preimage under f, f^{-1}(y), lies in I; equivalently, y ∈ I.map f iff f^{-1}(y) ∈ I.

Русский

Пусть f: R ≃+* S — кольцевое изоморфизм, и I — идеал R. Тогда для любого y ∈ S верно: y ∈ I.map f тогда и только тогда, когда f^{-1}(y) ∈ I.

LaTeX

$$$y \\in \\operatorname{map} f I \\;\\iff\\; f^{-1}(y) \\in I$$$

Lean4

@[simp]
theorem symm_apply_mem_of_equiv_iff {I : Ideal R} {f : R ≃+* S} {y : S} : f.symm y ∈ I ↔ y ∈ I.map f := by
  rw [← comap_symm, mem_comap]

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