English
The commutativity statement for localization away from x within S1 and away from y within S2 extends to a joint localization away from algebraMap_R S2 x in T.
Русский
Согласованность локализаций в рамках двух переменных x и y переносится на совместную локализацию away от algebraMap_R S2 x в T.
LaTeX
$$IsLocalization.Away (algebraMap_R S1 y) T$$
Lean4
/-- 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`. -/
theorem commutes {R : Type*} [CommSemiring R] (S₁ S₂ T : Type*) [CommSemiring S₁] [CommSemiring S₂] [CommSemiring T]
[Algebra R S₁] [Algebra R S₂] [Algebra R T] [Algebra S₁ T] [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 :=
by
haveI : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T :=
by
simp only [Algebra.algebraMapSubmonoid, Submonoid.map_powers]
infer_instance
convert IsLocalization.commutes S₁ S₂ T (Submonoid.powers x) (Submonoid.powers y)
ext x
simp [Algebra.algebraMapSubmonoid]
