Theorems · Theorem · commutative algebra

IsLocalization.algEquivOfAlgEquiv_eq_map

∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} {Q : Type u_8} [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] {h : R ≃ₐ[A] P}
  (H : Submonoid.map h M = T), ↑(IsLocalization.algEquivOfAlgEquiv S Q h H) = IsLocalization.map Q ↑h ⋯

Defined in

Mathlib.RingTheory.Localization.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerIsLocalizationCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerIsLocalization