Theorems · Theorem · commutative algebra

IsLocalization.Away.commutes

∀ {R : Type u_5} [inst : CommSemiring R] (S₁ : Type u_6) (S₂ : Type u_7) (T : Type u_8) [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : CommSemiring T] [inst_4 : Algebra R S₁] [inst_5 : Algebra R S₂]
  [inst_6 : Algebra R T] [inst_7 : Algebra S₁ T] [inst_8 : Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T]
  (x y : R) [IsLocalization.Away x S₁] [IsLocalization.Away y S₂] [IsLocalization.Away ((algebraMap R S₂) x) T],
  IsLocalization.Away ((algebraMap R S₁) y) T

If S₁ is the localization of R away from f and S₂ is the localization away from g, then any localization T of S₂ away from f is also a localization of S₁ away from g.

Defined in

Mathlib.RingTheory.Localization.Away.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringCommSemiringAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalization.AwayIsLocalization.AwayIsLocalization.Away