Tensor products over a field that are domains

Let K be a field. If A is a K-algebra and L a K-algebra with A ⊗[K] L a domain, then B ⊗[K] L is again a domain for every localization B of A at nonzero elements, since it is the localization of A ⊗[K] L at their images, which stay nonzero because A ⟶ A ⊗[K] L is injective. In particular this passes from a domain A to its fraction field: if A ⊗[K] L is a domain then so is Frac(A) ⊗[K] L. This is how the function field of an integral scheme over K inherits "geometric integrality" from the coordinate rings of its affine opens.

As an instance of this, for any K-algebra D that is a domain and any set of variables σ, the tensor product K(X_σ) ⊗[K] D of D with the rational function field K(X_σ) = FractionRing (MvPolynomial σ K) is again a domain. Indeed, K[X_σ] ⊗[K] D is the polynomial ring D[X_σ], a domain.

Since every field extension is algebraic over a purely transcendental one, this is the purely transcendental half of the comparison between the irreducible components of a scheme over K and those of its extension of scalars to a field extension of K.

theorem TauCeti.isDomain_tensorProduct_of_isLocalization {K : Type u_1} [Field K] {A : Type u_2} [CommRing A] [Algebra K A] (M : Submonoid A) (hM : M ≤ nonZeroDivisors A) (B : Type u_3) [CommRing B] [Algebra K B] [Algebra A B] [IsScalarTower K A B] [IsLocalization M B] (L : Type u_4) [CommRing L] [Algebra K L] [IsDomain (TensorProduct K A L)] : IsDomain (TensorProduct K B L)

Let B be a localization of the K-algebra A at a submonoid of nonzero divisors. If A ⊗[K] L is a domain, then so is B ⊗[K] L.

instance TauCeti.isDomain_fractionRing_mvPolynomial_tensorProduct {K : Type u_1} [Field K] {σ : Type u_2} {D : Type u_3} [CommRing D] [IsDomain D] [Algebra K D] : IsDomain (TensorProduct K (FractionRing (MvPolynomial σ K)) D)

The tensor product of a domain over a field K with a rational function field over K is a domain.