Smooth base change preserves integral closedness

If R is integrally closed in an R-algebra B and S is a smooth R-algebra, then S is integrally closed in S ⊗[R] B. This is the form of Mathlib's theorem that smooth base change commutes with integral closure (TensorProduct.toIntegralClosure_bijective_of_smooth, Stacks 0CBF) used to show that étale algebras over normal domains are normal: for B the fraction field of an integrally closed domain R, S is integrally closed in its generic fibre.

Main results

• TauCeti.Algebra.Smooth.isIntegrallyClosedIn_tensorProduct: a smooth algebra S over R is integrally closed in S ⊗[R] B whenever R is integrally closed in B. It is an instance.
• IsIntegral.exists_includeRight_eq: the same with the factors in the other order: every element of B ⊗[R] S integral over R comes from S.

References

• Stacks Project, Lemma 10.147.5.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Common/EtaleNormal.lean: Algebra.Smooth.isIntegrallyClosedIn_tensorProduct generalizes its Pcf.Stacks.isIntegrallyClosedIn_tensor_fractionRing_of_smooth from the fraction field of an integrally closed domain to any algebra in which R is integrally closed.

instance TauCeti.Algebra.Smooth.isIntegrallyClosedIn_tensorProduct {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [IsIntegrallyClosedIn R B] [Algebra.Smooth R S] : IsIntegrallyClosedIn S (TensorProduct R S B)

A smooth R-algebra S is integrally closed in S ⊗[R] B whenever R is integrally closed in B.

theorem IsIntegral.exists_includeRight_eq {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [IsIntegrallyClosedIn R B] [Algebra.Smooth R S] {z : TensorProduct R B S} (hz : IsIntegral R z) : ∃ (s : S), Algebra.TensorProduct.includeRight s = z

Every element of B ⊗[R] S that is integral over R comes from the smooth R-algebra S, when R is integrally closed in B. This is TauCeti.Algebra.Smooth.isIntegrallyClosedIn_tensorProduct with the factors in the other order.