map_fst_prod — Mathlib

English

The image of the product ideal I × J under the projection fst is precisely I.

Русский

Образ произведения идеалов I и J по проекции fst равен I.

LaTeX

$$$\\operatorname{map} (\\text{fst}) (I \\mathrm{prod} J) = I$$$

Lean4

@[simp]
theorem map_fst_prod (I : Ideal R) (J : Ideal S) : map (RingHom.fst R S) (prod I J) = I :=
  by
  ext x
  rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩

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