The meta properties of surjective ring homomorphisms.

Main results

Let R be a commutative ring, M be a submonoid of R.

• surjective_localizationPreserves : M⁻¹R →+* M⁻¹S is surjective if R →+* S is surjective.
• surjective_ofLocalizationSpan : R →+* S is surjective if there exists a set { r } that spans R such that Rᵣ →+* Sᵣ is surjective.
• surjective_localRingHom_of_surjective : A surjective ring homomorphism R →+* S induces a surjective homomorphism R_{f⁻¹(P)} →+* S_P for every prime ideal P of S.

theorem RingHom.surjective_stableUnderComposition : StableUnderComposition fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f

theorem RingHom.surjective_respectsIso : RespectsIso fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f

theorem RingHom.surjective_isStableUnderBaseChange : IsStableUnderBaseChange fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f

theorem RingHom.surjective_localizationPreserves : LocalizationPreserves fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f

M⁻¹R →+* M⁻¹S is surjective if R →+* S is surjective.

theorem RingHom.surjective_ofLocalizationSpan : OfLocalizationSpan fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f

R →+* S is surjective if there exists a set { r } that spans R such that Rᵣ →+* Sᵣ is surjective.

theorem RingHom.surjective_localRingHom_of_surjective {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Function.Surjective ⇑f) (P : Ideal S) [P.IsPrime] : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)

A surjective ring homomorphism R →+* S induces a surjective homomorphism R_{f⁻¹(P)} →+* S_P for every prime ideal P of S.