English
Surjectivity preserved under localization composition.
Русский
Сюръективность сохраняется при композиции локализаций.
LaTeX
$$$ \\operatorname{Surjective}(f.map\\ hy\\ k) $$$
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_comp_map {A : Type*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R] (j : LocalizationMap U R)
{l : P →* A} (hl : ∀ w : T, l w ∈ U) :
(k.map hl j).comp (f.map hy k) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j :=
by
ext z
change j _ * _ = j (l _) * _
rw [mul_inv_left, ← mul_assoc, mul_inv_right]
change j _ * j (l (g _)) = j (l _) * _
rw [← map_mul j, ← map_mul j, ← l.map_mul, ← l.map_mul]
refine k.comp_eq_of_eq hl j ?_
rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_mul_right]
