instIsLocalizedModuleLinearMapOfIsLocalization

English

If IsLocalization S A is given, then IsLocalizedModule S (IsScalarTower.toAlgHom R A A_s).toLinearMap holds.

Русский

Если дана локализация S по A, то существует локализационная структура модуля для линейного отображения через тензор-представление башни скаляров.

LaTeX

$$$[IsLocalization\\ S\\ A]\\Rightarrow IsLocalizedModule\\ S\\big(\\IsScalarTower.toAlgHom R A A_s\\big).toLinearMap.$$$

Lean4

instance [IsLocalization S A] : IsLocalizedModule S (Algebra.linearMap R A) :=
  (isLocalizedModule_iff_isLocalization' S _).mpr inferInstance

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