Theorems · Theorem · commutative algebra

IsLocalization.algEquiv_comp_algebraMap

∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₙ : Type u_5) (Rₘ' : Type u_6) (Sₙ' : Type u_7) [inst_3 : CommSemiring Rₘ]
  [inst_4 : CommSemiring Sₙ] [inst_5 : CommSemiring Rₘ'] [inst_6 : CommSemiring Sₙ'] [inst_7 : Algebra R Rₘ]
  [inst_8 : Algebra S Sₙ] [inst_9 : Algebra R Rₘ'] [inst_10 : Algebra S Sₙ'] [inst_11 : Algebra R Sₙ]
  [inst_12 : Algebra Rₘ Sₙ] [inst_13 : Algebra Rₘ' Sₙ'] [inst_14 : Algebra R Sₙ'] (N : Submonoid S)
  [inst_15 : IsLocalization M Rₘ] [inst_16 : IsLocalization N Sₙ] [inst_17 : IsLocalization M Rₘ']
  [inst_18 : IsLocalization N Sₙ'] [IsScalarTower R Rₘ Sₙ] [IsScalarTower R S Sₙ] [IsScalarTower R Rₘ' Sₙ']
  [IsScalarTower R S Sₙ'],
  (↑(IsLocalization.algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ) =
    (algebraMap Rₘ' Sₙ').comp ↑(IsLocalization.algEquiv M Rₘ Rₘ')

Defined in

Mathlib.RingTheory.Localization.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringCommSemiringCommSemiringCommSemiringAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraIsLocalizationIsLocalizationIsLocalizationIsLocalizationIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTower