English
The indexed product of nontrivial rings is not local.
Русский
Индексированное произведение не тривиальных колец не локально.
LaTeX
$$$ \neg IsLocalRing (\prod_{i\in I} R_i) $ for nontrivial index set I.$$
Lean4
/-- For an index type `ι` with at least two elements and an indexed family of (semi)rings
`R : ι → Type*`, the indexed product (semi)ring `Π i, R i` is not local. -/
theorem not_isLocalRing_of_nontrivial_pi {ι : Type*} [Nontrivial ι] (R : ι → Type*) [∀ i, Semiring (R i)]
[∀ i, Nontrivial (R i)] : ¬IsLocalRing (Π i, R i) := by
classical
let ⟨i₁, i₂, hi⟩ := exists_pair_ne ι
have ha : ¬IsUnit (fun i ↦ if i = i₁ then 0 else 1 : Π i, R i) := fun h ↦
not_isUnit_zero (M₀ := R i₁) (by simpa using h.map (Pi.evalRingHom R i₁))
have hb : ¬IsUnit (fun i ↦ if i = i₁ then 1 else 0 : Π i, R i) := fun h ↦
not_isUnit_zero (M₀ := R i₂) (by simpa [hi.symm] using h.map (Pi.evalRingHom R i₂))
exact not_isLocalRing_def ha hb (by ext; dsimp; split <;> simp)
