ker_isRadical_iff_reduced_of_surjective

English

Let f: R → S be a surjective ring homomorphism. Then the kernel of f is a radical ideal if and only if S is reduced (no nonzero nilpotents).

Русский

Пусть $f: R \to S$ — сюръективный кольцевой гомоморфизм. Тогда ядро $f$ радikalно тогда и только тогда, когда $S$ редуцированно (нет ненулевых нильпотентов).

LaTeX

$$(ker f).IsRadical ↔ IsReduced S, given surjective f$$

Lean4

theorem ker_isRadical_iff_reduced_of_surjective {S F} [CommSemiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S]
    {f : F} (hf : Function.Surjective f) : (RingHom.ker f).IsRadical ↔ IsReduced S :=
  by
  simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]
  rfl

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