English
If S is the localization of R at M and T is a localization of S at N, then the localization of S at N (via localizationLocalizationSubmodule M N) is again a localization: there is a canonical IsLocalization structure on LocalizationLocalizationSubmodule(M,N) with target T.
Русский
Если S есть локализация R в M, и T — локализация S по N, то локализация S по N, обозначаемая localizationLocalizationSubmodule(M,N), снова является локализацией: существует каноническая структура IsLocalization на LocalizationLocalizationSubmodule(M,N) относительно T.
LaTeX
$$$IsLocalization\left(localizationLocalizationSubmodule\,M\,N\right)\; T$$$
Lean4
/-- Given submodules `M ⊆ R` and `N ⊆ S = M⁻¹R`, with `f : R →+* S` the localization map, we have
`N ⁻¹ S = T = (f⁻¹ (N • f(M))) ⁻¹ R`. I.e., the localization of a localization is a localization.
-/
theorem localization_localization_isLocalization [IsLocalization N T] :
IsLocalization (localizationLocalizationSubmodule M N) T
where
map_units := localization_localization_map_units M N T
surj := localization_localization_surj M N T
exists_of_eq := localization_localization_exists_of_eq M N T _ _
