English
Let M be a multiplicative subset of a commutative ring R, and S, P, A be rings with ring maps making S a localization of R at M and A a localization of P at T, etc. If g: R →+* P and l: P →+* A induce maps of localizations and hy encodes the compatibility of M with T via g, then the composed localization map equals the localization map induced by the composite l ∘ g.
Русский
Пусть M — умножимое подмножество кольца R, и S, P, A — кольца, причём S является локализацией R в M, а A — локализацией P в T и т.д. При гомоморфизма g: R →+* P и l: P →+* A, которые индуцируют отображения локализаций и где hy задаёт совместимость M и T через g, композиция локализационных отображений равна отображению локализации, индуцированному составным отображением l ∘ g.
LaTeX
$$$$(\\mathrm{map}_W\\ l\\ hl) \\circ (\\mathrm{map}_Q\\ g\\ hy) = \\mathrm{map}_W\\big(l \\circ g\\big)\\big(\\lambda _ hx \\;{\\to}\\; hl( hy(hx) )\\big)$$$$
Lean4
/-- If `CommSemiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
theorem map_comp_map {A : Type*} [CommSemiring A] {U : Submonoid A} {W} [CommSemiring W] [Algebra A W]
[IsLocalization U W] {l : P →+* A} (hl : T ≤ U.comap l) :
(map W l hl).comp (map Q g hy : S →+* _) = map W (l.comp g) fun _ hx => hl (hy hx) :=
RingHom.ext fun x =>
Submonoid.LocalizationMap.map_map (P := P) (toLocalizationMap M S) (fun y => hy y.2) (toLocalizationMap U W)
(fun w => hl w.2) x
