Theorems · Theorem · commutative algebra

IsLocalization.commutes

∀ {R : Type u_1} [inst : CommSemiring R] (S₁ : Type u_4) (S₂ : Type u_5) (T : Type u_6) [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]
  (M₁ M₂ : Submonoid R) [IsLocalization M₁ S₁] [IsLocalization M₂ S₂]
  [IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T], IsLocalization (Algebra.algebraMapSubmonoid S₁ M₂) T

If S₁ is the localization of R at M₁ and S₂ is the localization of R at M₂, then every localization T of S₂ at M₁ is also a localization of S₁ at M₂, in other words M₁⁻¹M₂⁻¹R can be identified with M₂⁻¹M₁⁻¹R.

Defined in

Mathlib.RingTheory.Localization.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringCommSemiringAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalizationIsLocalizationIsLocalization