English
Composition of the two localization lifts yields the identity on N.
Русский
Композиция двух локализационных подъёмов даёт тождественное отображение на N.
LaTeX
$$$ \\forall z,\\ k.lift f.map_units ( f.lift k.map_units z ) = z $$$
Lean4
/-- Given two Localization maps `f : M →* N, k : M →* P` for a Submonoid `S ⊆ M`, the hom
from `P` to `N` induced by `f` is left inverse to the hom from `N` to `P` induced by `k`. -/
@[to_additive (attr := simp) /-- Given two Localization maps `f : M →+ N, k : M →+ P` for a Submonoid `S ⊆ M`, the hom
from `P` to `N` induced by `f` is left inverse to the hom from `N` to `P` induced by `k`. -/
]
theorem lift_left_inverse {k : LocalizationMap S P} (z : N) : k.lift f.map_units (f.lift k.map_units z) = z :=
(DFunLike.congr_fun (lift_comp_lift_eq f k f.map_units) z).trans (lift_id f z)
