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]
:
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_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.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_iff_of_isLocalHom
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
[IsLocalRing S]
[IsLocalHom f]
:
@[deprecated RingHom.surjectiveOnStalks_iff_of_isLocalHom (since := "2024-10-10")]
theorem
RingHom.surjectiveOnStalks_iff_of_isLocalRingHom
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
[IsLocalRing S]
[IsLocalHom f]
: