sigmaToPi_injective — Mathlib

English

The map sigmaToPi from a family of rings to their product is injective on the prime spectrum level.

Русский

Отображение sigmaToPi от семейства колец к их произведению инъективно на уровне спектра простых.

LaTeX

$$$(\\sigmaToPi R) \\text{ is injective}$$$

Lean4

theorem sigmaToPi_injective : (sigmaToPi R).Injective := fun ⟨i, p⟩ ⟨j, q⟩ eq ↦ by
  classical
  obtain rfl | ne := eq_or_ne i j
  · congr; ext x
    simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq
  · refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
    have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
    simpa [← eq, Function.update_of_ne ne]

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