Kernel_of_Ring_Epimorphism_is_Ideal

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

ideal-theoryproofwikiquotient-ringsring-epimorphisms

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring epimorphism. Then The kernel of $\phi$ is an ideal of $R_1$ . There is a unique ring isomorphism $g: R_1 / K \to R_2$ such that $g \circ q_K = \phi$ $\phi$ is a ring isomorphism $K = \set {0_{R_1} }$ .

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.Ideal.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.Ideal.Basic

theorem Kernel_of_Ring_Epimorphism_is_Ideal {R S : Type _} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective f) : ∃ I : Ideal R, (∀ x, f x = 0 ↔ x ∈ I) := by sorry

Source

https://proofwiki.org/wiki/Kernel_of_Ring_Epimorphism_is_Ideal

View graph