English
If R is a nonlocal commutative ring, there exist two fields K1,K2 and a surjective ring homomorphism f: R → K1 × K2.
Русский
Если R является нелокальным коммутативным кольцом, то существует два поля K1, K2 и сюръективное кольцо-гомоморфизм f: R → K1 × K2.
LaTeX
$$$\\exists K_1 K_2 \\; (\\text{Field }K_1) (\\text{Field }K_2) \\; (f : R \\to+* K_1 \\times K_2), \\mathrm{Surjective}(f)$$$
Lean4
/-- There exists a surjective ring homomorphism from a non-local commutative ring onto a product
of two fields. -/
theorem exists_surjective_of_not_isLocalRing.{u} {R : Type u} [CommRing R] [Nontrivial R] (h : ¬IsLocalRing R) :
∃ (K₁ K₂ : Type u) (_ : Field K₁) (_ : Field K₂) (f : R →+* K₁ × K₂), Function.Surjective f := by
/- get two different maximal ideals and project on the product of quotients -/
obtain ⟨m₁, m₂, _, _, hm₁m₂⟩ := (not_isLocalRing_tfae.out 0 2).mp h
let e := Ideal.quotientInfEquivQuotientProd m₁ m₂ <| Ideal.isCoprime_of_isMaximal hm₁m₂
let f := e.toRingHom.comp <| Ideal.Quotient.mk (m₁ ⊓ m₂)
use R ⧸ m₁, R ⧸ m₂, Ideal.Quotient.field m₁, Ideal.Quotient.field m₂, f
apply Function.Surjective.comp e.surjective Ideal.Quotient.mk_surjective
