Theorems · Theorem · commutative algebra

IsLocalization.integralClosure

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rf : Type u_5}
  {Sf : Type u_6} [inst_3 : CommRing Rf] [inst_4 : CommRing Sf] [inst_5 : Algebra R Rf] [inst_6 : Algebra S Sf]
  [inst_7 : Algebra Rf Sf] [inst_8 : Algebra R Sf] [IsScalarTower R S Sf] [inst_10 : IsScalarTower R Rf Sf]
  (M : Submonoid R) [IsLocalization M Rf] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sf]
  [inst_13 : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
  [IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf]
  [IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)],
  IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) ↥(integralClosure Rf Sf)

Taking integral closure commutes with localizations.

Defined in

Mathlib.RingTheory.Localization.Integral

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalizationIsLocalizationAlgebraIsScalarTowerIsScalarTower