isLocalizedModule_iff_isLocalization'

English

For IsLocalizedModule S (IsScalarTower.toAlgHom R A A_s).toLinearMap, it is equivalent to IsLocalization S A_s via the specified tower relations.

Русский

Для IsLocalizedModule S (IsScalarTower.toAlgHom R A A_s).toLinearMap верно эквивалентно IsLocalization S A_s через заданную башню скаляров.

LaTeX

$$$\\IsLocalizedModule S\\big(\\IsScalarTower.toAlgHom R A A_s\\).toLinearMap \\iff \\IsLocalization S A_s.$$$

Lean4

/-- `A` is a localization of a commutative semiring `R` with respect to `S` iff
the associated linear map `R →ₗ[R] A` is a localization of modules with respect to `S`. -/
theorem isLocalizedModule_iff_isLocalization' : IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A :=
  by
  convert isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)
  exact (Submonoid.map_id S).symm

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