localizationLocalizationSubmodule

English

Localizing w.r.t. M and then w.r.t. N is equal to the localization with respect to the submonoid localizationLocalizationSubmodule(M,N).

Русский

Локализация по M затем по N равна локализации по подмодулю локализации localizationLocalizationSubmodule(M,N).

LaTeX

$$$\mathrm{localizationLocalizationSubmodule}\ M\ N = \mathrm{Submonoid.comap}(\mathrm{algebraMap} R S)\big(\mathrm{SemilatticeSup.toMax.max}\ N\ (\mathrm{Submonoid.map}(\mathrm{algebraMap} R S)\ M)\big)$$$

Lean4

/-- Localizing w.r.t. `M ⊆ R` and then w.r.t. `N ⊆ S = M⁻¹R` is equal to the localization of `R`
w.r.t. this module. See `localization_localization_isLocalization`.
-/
@[nolint unusedArguments]
def localizationLocalizationSubmodule : Submonoid R :=
  (N ⊔ M.map (algebraMap R S)).comap (algebraMap R S)

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