Theorems · Theorem · commutative algebra

TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway

∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {s : Set S},
  Ideal.span s = ⊤ →
    ∀ (Sᵣ : ↑s → Type u_4) [inst_5 : (r : ↑s) → CommRing (Sᵣ r)] [inst_6 : (r : ↑s) → Algebra S (Sᵣ r)]
      [inst_7 : (r : ↑s) → Algebra R (Sᵣ r)] [∀ (r : ↑s), IsScalarTower R S (Sᵣ r)]
      [∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)],
      (∀ (r : ↑s), Function.Bijective ⇑(TensorProduct.toIntegralClosure R (Sᵣ r) B)) →
        Function.Bijective ⇑(TensorProduct.toIntegralClosure R S B)

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

Defined in

Mathlib.RingTheory.Smooth.IntegralClosure

Cited by

1 results in Mathlib

Foundations

Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization.Away