instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom

English

Under the given hypotheses, the map from R to the larger structure given by the tower is a localization with respect to the nonzero divisors of R. In particular, the S′-structure together with the tower R ⟶ S ⟶ S′ exhibits S′ as the localization of R at the multiplicative set of nonzero divisors.

Русский

При данных гипотезах отображение из R в более крупную структуру, заданную башней, является локализацией по множителю не нулевых делителей R. В частности, структура S′ вместе с вилкой R ⟶ S ⟶ S′ образует локализацию S′ по множеству невырожденных делителей R.

LaTeX

$$$\operatorname{IsLocalizedModule}\bigl(\operatorname{nonZeroDivisors}(R)\bigr)\bigl(\operatorname{IsScalarTower.toAlgHom}(R,S,S').toLinearMap\bigr)$$

Lean4

instance : IsLocalizedModule R⁰ (IsScalarTower.toAlgHom R S S').toLinearMap :=
  isLocalizedModule_iff_isLocalization.mpr inferInstance

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