Smooth base change commutes with integral closure

In this file we aim to prove that smooth base change commutes with integral closure. We define the map TensorProduct.toIntegralClosure : S ⊗[R] integralClosure R B →ₐ[S] integralClosure S (S ⊗[R] B) and (TODO) show that it is bijective when S is R-smooth.

Main results

• TensorProduct.toIntegralClosure_injective_of_flat: If S is R-flat, then TensorProduct.toIntegralClosure is injective.
• TensorProduct.toIntegralClosure_mvPolynomial_bijective: If S = MvPolynomial σ R, then TensorProduct.toIntegralClosure is bijective.
• TensorProduct.toIntegralClosure_bijective_of_isLocalization: If S = Localization M, then TensorProduct.toIntegralClosure is bijective.

TODO (@erdOne)

Show that TensorProduct.toIntegralClosure is bijective when S is R-smooth.

def TensorProduct.toIntegralClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (B : Type u_4) [CommRing B] [Algebra R B] : TensorProduct R S ↥(integralClosure R B) →ₐ[S] ↥(integralClosure S (TensorProduct R S B))

The comparison map from S ⊗[R] integralClosure R B to integralClosure S (S ⊗[R] B). This is injective when S is R-flat, and (TODO) bijective when S is R-smooth.

Equations

• TensorProduct.toIntegralClosure R S B = (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val).codRestrict (integralClosure S (TensorProduct R S B)) ⋯

theorem TensorProduct.toIntegralClosure_injective_of_flat {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Module.Flat R S] : Function.Injective ⇑(toIntegralClosure R S B)

theorem TensorProduct.toIntegralClosure_bijective_of_tower {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] {T : Type u_4} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (H : Function.Bijective ⇑(toIntegralClosure R S B)) (H' : Function.Bijective ⇑(toIntegralClosure S T (TensorProduct R S B))) : Function.Bijective ⇑(toIntegralClosure R T B)

"Base change preserves integral closure" is stable under composition.

theorem TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] {s : Set S} (hs : Ideal.span s = ⊤) (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommRing (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] [(r : ↑s) → Algebra R (Sᵣ r)] [∀ (r : ↑s), IsScalarTower R S (Sᵣ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)] (H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)) : Function.Bijective ⇑(toIntegralClosure R S B)

"Base change preserves integral closure" can be checked Zariski-locally.

theorem TensorProduct.toIntegralClosure_mvPolynomial_bijective {R : Type u_1} {B : Type u_3} [CommRing R] [CommRing B] [Algebra R B] {σ : Type u_4} : Function.Bijective ⇑(toIntegralClosure R (MvPolynomial σ R) B)

Base changing to MvPolynomial σ R preserves integral closure.

theorem TensorProduct.toIntegralClosure_bijective_of_isLocalization {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] (M : Submonoid R) [IsLocalization M S] : Function.Bijective ⇑(toIntegralClosure R S B)

Localization preserves integral closure.