Equivalence between IsLocalizedModule and IsLocalization #
theorem
isLocalizedModule_iff_isLocalization
{R : Type u_1}
[CommSemiring R]
{S : Submonoid R}
{A : Type u_2}
{Aₛ : Type u_3}
[CommSemiring A]
[Algebra R A]
[CommSemiring Aₛ]
[Algebra A Aₛ]
[Algebra R Aₛ]
[IsScalarTower R A Aₛ]
:
IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
instance
instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
{A : Type u_2}
{Aₛ : Type u_3}
[CommSemiring A]
[Algebra R A]
[CommSemiring Aₛ]
[Algebra A Aₛ]
[Algebra R Aₛ]
[IsScalarTower R A Aₛ]
[IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ]
:
IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap
theorem
isLocalizedModule_iff_isLocalization'
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
(A : Type u_2)
[CommSemiring A]
[Algebra R A]
:
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.
instance
instIsLocalizedModuleLinearMapOfIsLocalization
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
(A : Type u_2)
[CommSemiring A]
[Algebra R A]
[IsLocalization S A]
:
IsLocalizedModule S (Algebra.linearMap R A)
theorem
IsLocalization.mk'_algebraMap_eq_mk'
{R : Type u_1}
[CommSemiring R]
{S : Submonoid R}
{A : Type u_2}
{Aₛ : Type u_3}
[CommSemiring A]
[Algebra R A]
[CommSemiring Aₛ]
[Algebra A Aₛ]
[Algebra R Aₛ]
[IsScalarTower R A Aₛ]
[IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ]
{x : A}
{s : ↥S}
:
mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s
IsLocalization.mk' agrees with IsLocalizedModule.mk'.
theorem
IsLocalization.mk'_eq_mk'
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
(A : Type u_2)
[CommSemiring A]
[Algebra R A]
[IsLocalization S A]
(x : R)
(s : ↥S)
:
IsLocalization.mk' agrees with IsLocalizedModule.mk'.