instIsScalarTowerSubtypeMemSubmoduleOfNatLocalization

English

There is a canonical IsScalarTower structure relating 𝒜0, HomogeneousLocalization 𝒜 x, and Localization x.

Русский

Существует каноническая структура IsScalarTower между 𝒜0, HomogeneousLocalization 𝒜 x и Localization x.

LaTeX

$$$\\text{IsScalarTower}(\\mathcal{A}_0, \\mathrm{HomogeneousLocalization}(\\mathcal{A},x), \\mathrm{Localization}(x))$$$

Lean4

instance : IsScalarTower (𝒜 0) (HomogeneousLocalization 𝒜 x) (Localization x) :=
  .of_algebraMap_eq' rfl

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