English
Associativity of induced maps on localizations.
Русский
Ассоциативность индуцированных отображений локализаций.
LaTeX
$$$ (k.map hl j).comp (f.map hy k) = f.map (fun x \\mapsto show l \\comp g x \\in U from hl ⟨g x, hy x⟩) j $$$
Lean4
/-- If `CommMonoid` homs `g : M →* P, l : P →* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
@[to_additive /-- If `AddCommMonoid` homs `g : M →+ 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*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R] (j : LocalizationMap U R) {l : P →* A}
(hl : ∀ w : T, l w ∈ U) (x) :
k.map hl j (f.map hy k x) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j x := by
-- Porting note: need to specify `k` explicitly
rw [← f.map_comp_map (k := k) hy j hl]
simp only [MonoidHom.coe_comp, comp_apply]
