English
Suppose N is a submonoid of S and T is a localization of S at N. If every unit of S lies in N, then the localization comap construction from R to T yields a localization of R at the comap of N, i.e., N.comap(algebraMap_R_S) localizes to T.
Русский
Пусть N — подмонойд S, T — локализация S по N, и все единицы S лежат в N. Тогда локализация через N.comap(algebraMap_R_S) является локализацией R в T.
LaTeX
$$$IsLocalization\left(N^{\mathrm{comap}}\circ (algebraMap\ R\ S), T\right)$ при условии $\forall x\in S, IsUnit(x)\Rightarrow x\in N$.$$
Lean4
/-- Given submodules `M ⊆ R` and `N ⊆ S = M⁻¹R`, with `f : R →+* S` the localization map, if
`N` contains all the units of `S`, then `N ⁻¹ S = T = (f⁻¹ N) ⁻¹ R`. I.e., the localization of a
localization is a localization.
-/
theorem localization_localization_isLocalization_of_has_all_units [IsLocalization N T] (H : ∀ x : S, IsUnit x → x ∈ N) :
IsLocalization (N.comap (algebraMap R S)) T :=
by
convert localization_localization_isLocalization M N T using 1
dsimp [localizationLocalizationSubmodule]
congr
symm
rw [sup_eq_left]
rintro _ ⟨x, hx, rfl⟩
exact H _ (IsLocalization.map_units _ ⟨x, hx⟩)
