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'.