Ring Homomorphisms surjective on stalks #
In this file, we prove some results on ring homomorphisms surjective on stalks, to be used in the development of immersions in algebraic geometry.
A ring homomorphism R →+* S is surjective on stalks if R_p →+* S_q is surjective for all pairs
of primes p = f⁻¹(q). We show that this property is stable under composition and base change, and
that surjections and localizations satisfy this.
theorem
RingHom.surjective_localRingHom_iff
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
(P : Ideal S)
[P.IsPrime]
:
Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔ ∀ (s : S), ∃ (x : R) (r : R), ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
R_p →+* S_q is surjective if and only if
every x : S is of the form f x / f r for some f r ∉ q.
This is useful when proving SurjectiveOnStalks.
theorem
RingHom.surjectiveOnStalks_iff_forall_maximal
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
:
f.SurjectiveOnStalks ↔ ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
theorem
RingHom.surjectiveOnStalks_of_surjective
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
(h : Function.Surjective ⇑f)
:
theorem
RingHom.SurjectiveOnStalks.comp
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{T : Type u_3}
[CommRing T]
{g : S →+* T}
{f : R →+* S}
(hg : g.SurjectiveOnStalks)
(hf : f.SurjectiveOnStalks)
:
(g.comp f).SurjectiveOnStalks
theorem
RingHom.SurjectiveOnStalks.localRingHom_surjective
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
(hf : f.SurjectiveOnStalks)
(P : Ideal R)
[P.IsPrime]
(Q : Ideal S)
[Q.IsPrime]
(e : P = Ideal.comap f Q)
:
Function.Surjective ⇑(Localization.localRingHom P Q f e)
theorem
RingHom.SurjectiveOnStalks.exists_mul_eq_tmul
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{T : Type u_3}
[CommRing T]
[Algebra R T]
[Algebra R S]
(hf₂ : (algebraMap R T).SurjectiveOnStalks)
(x : TensorProduct R S T)
(J : Ideal T)
(hJ : J.IsPrime)
:
If R → T is surjective on stalks, and J is some prime of T,
then every element x in S ⊗[R] T satisfies (1 ⊗ r • t) * x = a ⊗ t for some
r : R, a : S, and t : T such that r • t ∉ J.
theorem
RingHom.surjectiveOnStalks_of_isLocalization
{R : Type u_1}
[CommRing R]
(M : Submonoid R)
(S : Type u_2)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
:
(algebraMap R S).SurjectiveOnStalks
theorem
RingHom.SurjectiveOnStalks.baseChange
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{T : Type u_3}
[CommRing T]
[Algebra R T]
[Algebra R S]
(hf : (algebraMap R T).SurjectiveOnStalks)
:
(algebraMap S (TensorProduct R S T)).SurjectiveOnStalks
theorem
RingHom.SurjectiveOnStalks.baseChange'
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{T : Type u_3}
[CommRing T]
[Algebra R T]
[Algebra R S]
(hf : (algebraMap R S).SurjectiveOnStalks)
:
theorem
RingHom.SurjectiveOnStalks.tensorProductMap
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{T : Type u_3}
[CommRing T]
{S' : Type u_4}
{T' : Type u_5}
[CommRing S']
[CommRing T']
[Algebra R S]
[Algebra R T]
[Algebra R S']
[Algebra R T']
{f : S →ₐ[R] S'}
(Hf : f.SurjectiveOnStalks)
{g : T →ₐ[R] T'}
(Hg : g.SurjectiveOnStalks)
:
theorem
RingHom.surjectiveOnStalks_iff_of_isLocalHom
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
[IsLocalRing S]
[IsLocalHom f]
: