English
A ring R is simple if and only if for all S, any f: R →+* S is injective or S is subsingleton; equivalently, IsSimpleRing R holds exactly when every such map is either injective or codomain trivial.
Русский
Кольцо R простое тогда и только тогда, когда для всех S любой гамоморфизм f: R →+* S либо инъективен, либо кодомножество тривиально; эквивалентно IsSimpleRing R.
LaTeX
$$IsSimpleRing R ↔ ∀ {S}, [NonAssocSemiring S] (f : R →+* S), Injective f ∨ Subsingleton S$$
Lean4
theorem iff_injective_ringHom_or_subsingleton_codomain (R : Type u) [NonAssocRing R] [Nontrivial R] :
IsSimpleRing R ↔ ∀ {S : Type u} [NonAssocSemiring S] (f : R →+* S), Function.Injective f ∨ Subsingleton S
where
mp _ _ _ := injective_ringHom_or_subsingleton_codomain
mpr
H :=
of_eq_bot_or_eq_top fun I =>
H I.ringCon.mk' |>.imp
(fun h => le_antisymm (fun _ hx => TwoSidedIdeal.ker_eq_bot _ |>.2 h ▸ I.ker_ringCon_mk'.symm ▸ hx) bot_le)
(fun h => le_antisymm le_top fun x _ => I.mem_iff _ |>.2 (Quotient.eq'.1 (h.elim x 0)))
