mem_map_algebraMap_iff — Mathlib

English

Characterization of when mk' lies in a mapped ideal via algebraMap.

Русский

Характеризация принадлежности mk' образованному элементу через algebraMap в отображенный идеал.

LaTeX

$$mk'_mem_map_algebraMap_iff I x s$$

Lean4

theorem mem_map_algebraMap_iff {I : Ideal R} {z} :
    z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x : I × M, z * algebraMap R S x.2 = algebraMap R S x.1 :=
  by
  constructor
  · change _ → z ∈ map_ideal M S I
    refine fun h => Ideal.mem_sInf.1 h fun z hz => ?_
    obtain ⟨y, hy⟩ := hz
    let Z : { x // x ∈ I } := ⟨y, hy.left⟩
    use ⟨Z, 1⟩
    simp [Z, hy.right]
  · rintro ⟨⟨a, s⟩, h⟩
    rw [← Ideal.unit_mul_mem_iff_mem _ (map_units S s), mul_comm]
    exact h.symm ▸ Ideal.mem_map_of_mem _ a.2

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