English
Given g: R →+* P and l: P →+* A inducing localization maps, the map corresponding to the composed homomorphism l ∘ g coincides with the composition of the individual localization maps.
Русский
Пусть даны гомоморфизмы g: R →+* P и l: P →+* A, индуцирующие отображения локализаций; отображение локализации, соответствующее составному гомоморфизму l ∘ g, совпадает с композицией отдельных локализационных отображений.
LaTeX
$$$$\\mathrm{map}_W(l, hl) \\; (\\mathrm{map}_Q(g, hy)\\; x) = \\mathrm{map}_W(l \\circ g)\\big(\\lambda x. hl( hy(x) )\\big)\\, x$$$$
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_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) (x : S) :
map W l hl (map Q g hy x) = map W (l.comp g) (fun _ hx => hl (hy hx)) x := by rw [← map_comp_map (Q := Q) hy hl];
rfl
