Theorems · Theorem · commutative algebra

IsLocalization.Away.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] (f : R)
  [IsLocalization.Away f Rf] [IsLocalization.Away ((algebraMap R S) f) 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.Away ((algebraMap R ↥(integralClosure R S)) f) ↥(integralClosure Rf Sf)

Defined in

Mathlib.RingTheory.Localization.Integral

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalization.AwayIsLocalization.AwayAlgebraIsScalarTowerIsScalarTower