Lemmas regarding the prime spectrum of tensor products

Main result

• PrimeSpectrum.embedding_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 (PrimeSpectrum.tensorProductTo R S T)

theorem PrimeSpectrum.embedding_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₁ : PrimeSpectrum (TensorProduct R S T)) (p₂ : PrimeSpectrum (TensorProduct R S T)) (h : PrimeSpectrum.tensorProductTo R S T p₁ = PrimeSpectrum.tensorProductTo R S T p₂) : p₁ ≤ p₂

theorem PrimeSpectrum.embedding_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) : Embedding (PrimeSpectrum.tensorProductTo R S T)