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 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.
• TensorProduct.toIntegralClosure_bijective_of_smooth: If S is R-smooth, then TensorProduct.toIntegralClosure is bijective.

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.

theorem exists_derivative_mul_eq_and_isIntegral_coeff {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] {φ : Polynomial S →ₐ[R] B} (hφ : Function.Surjective ⇑φ) {f : Polynomial S} (hf : f.Monic) (hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)) (hfx : RingHom.ker φ.toRingHom = Ideal.span {f}) {y : B} (hy : IsIntegral R y) : ∃ (g : Polynomial S), φ (Polynomial.derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Let S be an R-algebra and f : S[X] be a monic polynomial with R-integral coefficients. Suppose y in B = S[X]/f is R-integral, then f' * y is the image of some g : S[X] with R-integral coefficients.

theorem mem_adjoin_map_integralClosure_of_isStandardEtale {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra.IsStandardEtale R S] (a : TensorProduct R S B) (hx : IsIntegral S a) : a ∈ Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))

Stacks Tag 03GE (without the generalization to arbitrary etale algebra)

theorem TensorProduct.toIntegralClosure_bijective_of_smooth {R : Type u_1} {S : Type u_2} {B : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra.Smooth R S] : Function.Bijective ⇑(toIntegralClosure R S B)