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.

def RingHom.SurjectiveOnStalks {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : Prop

A ring homomorphism R →+* S is surjective on stalks if R_p →+* S_q is surjective for all pairs of primes p = f⁻¹(q).

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_ideal {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} : f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ (x : R) (r : R), ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

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_iff_forall_maximal' {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} : f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ (x : R) (r : R), ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

theorem RingHom.surjectiveOnStalks_of_exists_div {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} (h : ∀ (x : S), ∃ (r : R) (s : R), IsUnit (f s) ∧ f s * x = f r) : f.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) : f.SurjectiveOnStalks

theorem RingEquiv.surjectiveOnStalks {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) : e.toRingHom.SurjectiveOnStalks

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.of_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.comp f).SurjectiveOnStalks) : g.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) : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t

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) : Algebra.TensorProduct.includeRight.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) : (Algebra.TensorProduct.map f 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] : f.SurjectiveOnStalks ↔ Function.Surjective ⇑f