Lemmas regarding the prime spectrum of tensor products

Main result

• PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks: If R →+* T is surjective on stalks (see Mathlib/RingTheory/SurjectiveOnStalks.lean), then Spec(S ⊗[R] T) → Spec S × Spec T is a topological embedding (where Spec S × Spec T is the Cartesian product with the product topology).

noncomputable def PrimeSpectrum.tensorProductTo (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (x : PrimeSpectrum (TensorProduct R S T)) : PrimeSpectrum S × PrimeSpectrum T

The canonical map from Spec(S ⊗[R] T) to the Cartesian product Spec S × Spec T.

Equations

• PrimeSpectrum.tensorProductTo R S T x = (PrimeSpectrum.comap (algebraMap S (TensorProduct R S T)) x, PrimeSpectrum.comap Algebra.TensorProduct.includeRight.toRingHom x)

theorem PrimeSpectrum.continuous_tensorProductTo (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] : Continuous (tensorProductTo R S T)

theorem PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) (p₁ p₂ : PrimeSpectrum (TensorProduct R S T)) (h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂) : p₁ ≤ p₂

theorem PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) : Topology.IsEmbedding (tensorProductTo R S T)