Relative algebraic closure and extension of scalars to an algebraically closed field

Let K / k be a field extension and L an algebraically closed field containing k. If K ⊗[k] L is a domain, then k is algebraically closed in K: the relative algebraic closure algebraicClosure k K is ⊥.

Indeed, E = algebraicClosure k K is algebraic over k, and L ⊗[k] E embeds in the domain L ⊗[k] K because every k-module is flat. So L ⊗[k] E is a domain that is integral over the algebraically closed field L, hence equal to L; comparing dimensions, [E : k] = 1.

This is the field-theoretic content of the fact that the function field of a geometrically integral scheme over k contains no nontrivial algebraic extension of k: there K ⊗[k] L is a localization of the ring of functions on an affine open of the base change of the scheme to L, which is integral.

Main results

• TauCeti.algebraicClosure_eq_bot_of_isDomain_tensorProduct: if K ⊗[k] L is a domain for an algebraically closed field L over k, then algebraicClosure k K = ⊥.

theorem TauCeti.algebraicClosure_eq_bot_of_isDomain_tensorProduct {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (L : Type u_3) [Field L] [Algebra k L] [IsAlgClosed L] [IsDomain (TensorProduct k K L)] : algebraicClosure k K = ⊥

If K ⊗[k] L is a domain for some algebraically closed field L over k, then k is algebraically closed in K.