instIsScalarTowerLocalizationAtPrime

English

There is a scalar tower of rings R → Localization M → Localization.AtPrime p, i.e., R acts compatibly through localization at M and then AtPrime p.

Русский

Существует тензорная башня скаляров R → Localization M → Localization.AtPrime p.

LaTeX

$$IsScalarTower R (Localization M) (Localization.AtPrime p)$$

Lean4

instance (p : Ideal (Localization M)) [p.IsPrime] : IsScalarTower R (Localization M) (Localization.AtPrime p) :=
  IsScalarTower.of_algebraMap_eq' rfl

Похожие утверждения