Ring_Epimorphism_Preserves_Ideals

Proved

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

ideal-theoryproofwikiring-epimorphisms

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring epimorphism. Let $J$ be an ideal of $R_1$ . Then $\phi \sqbrk J$ is an ideal of $R_2$ .

Preamble

import Mathlib.RingTheory.Ideal.Basic

Formal statement

theorem Ring_Epimorphism_Preserves_Ideals {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : R₁ →+* R₂) (hf : Function.Surjective f) (I : Ideal R₁) : ∃ J : Ideal R₂, (↑J : Set R₂) = f '' (↑I : Set R₁) := by sorry

Source

https://proofwiki.org/wiki/Ring_Epimorphism_Preserves_Ideals

View graph