Integral closures and base change of the fraction field

Let A be a domain with fraction field K, and let L be an algebraic extension of K. Every element of L is an element of the integral closure of A in L divided by an element of A. Hence the integral closure spans L over K, and, for any K-algebra K', the tensor product K' ⊗[K] L is spanned over K' by the elements 1 ⊗ b with b in the integral closure of A in L.

Main results

• TauCeti.span_integralClosure_eq_top: the integral closure of A in L spans L over K.
• TauCeti.span_one_tmul_integralClosure_eq_top: the elements 1 ⊗ b, for b in the integral closure of A in L, span K' ⊗[K] L over K'.

theorem TauCeti.span_integralClosure_eq_top {A : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [Algebra.IsAlgebraic K L] : Submodule.span K ↑(integralClosure A L) = ⊤

The integral closure of A in L spans L over K: every element of L is an element of the integral closure divided by a nonzero element of A.

theorem TauCeti.span_one_tmul_integralClosure_eq_top {A : Type u_1} {K : Type u_2} {L : Type u_3} {K' : Type u_4} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [Algebra.IsAlgebraic K L] [CommRing K'] [Algebra K K'] : Submodule.span K' (Set.range fun (b : ↥(integralClosure A L)) => 1 ⊗ₜ[K] ↑b) = ⊤

The elements 1 ⊗ b, for b in the integral closure of A in L, span K' ⊗[K] L over K'.