Preimage_of_Subring_under_Ring_Homomorphism_is_Subring
Provedproofwikiring-homomorphismssubrings
Let be a ring homomorphism. Let be a subring of . Then is a subring of such that .
Preamble
import Mathlib.RingTheory.Ideal.Quotient.Basic
Formal statement
theorem Preimage_of_Subring_under_Ring_Homomorphism_is_Subring {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : RingHom R₁ R₂) (S : Subring R₂) : ∃ T : Subring R₁, ∀ x, x ∈ T ↔ f x ∈ S := by sorrySource