English
For any x ∈ M, y ∈ S, f.lift hg (f.mk' x y) equals g x times the inverse of g y.
Русский
Для любых x ∈ M, y ∈ S, f.lift hg (f.mk' x y) = g x · (g y)^{-1}.
LaTeX
$$$ f.lift hg (f.mk' x y) = g x \cdot (g y)^{-1} $$$
Lean4
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g y` is invertible for all `y : S`, the homomorphism induced from
`N` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : M, y ∈ S`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`. -/
]
theorem lift_mk' (x y) : f.lift hg (f.mk' x y) = g x * (IsUnit.liftRight (g.restrict S) hg y)⁻¹ :=
(mul_inv hg).2 <| f.eq_of_eq hg <| by simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
