injective_ringHom_or_subsingleton_codomain

English

Let R be a simple ring and S a nontrivial semiring. For any ring homomorphism f: R → S, either f is injective or S is a subsingleton.

Русский

Пусть R — простое кольцо и S — ненулевой полусколь, тогда любой кольцевой однородник f: R → S либо инъективен, либо S сводится к одному элементу.

LaTeX

$$If R is a simple ring and S is a nontrivial semiring, then for any f: R →+* S, Either Injective f or Subsingleton S.$$

Lean4

theorem injective_ringHom_or_subsingleton_codomain {R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S]
    (f : R →+* S) : Function.Injective f ∨ Subsingleton S :=
  simple.eq_bot_or_eq_top (TwoSidedIdeal.ker f) |>.imp (TwoSidedIdeal.ker_eq_bot _ |>.1)
    (fun h =>
      subsingleton_iff_zero_eq_one.1 <|
        by
        have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _
        rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem)

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