Image_of_Preimage_of_Subring_under_Ring_Epimorphism

Proved

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

proofwikiring-epimorphismssubrings

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring epimorphism. Let $S_2$ be a subring of $R_2$ . Then $\phi \sqbrk {\phi^{-1} \sqbrk {S_2} } = S_2$

Preamble

import Mathlib.Data.Set.Function
import Mathlib.RingTheory.Ideal.Basic

Formal statement

theorem Image_of_Preimage_of_Subring_under_Ring_Epimorphism {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : R₁ →+* R₂) (hf : Function.Surjective f) (S : Set R₂) : f '' (f ⁻¹' S) = S := by sorry

Source

https://proofwiki.org/wiki/Image_of_Preimage_of_Subring_under_Ring_Epimorphism

View graph