English
The lift respects mk' construction: f.lift hg (f.mk' x y) equals g x times (g y)^{-1}.
Русский
Подъем сохраняет конструкцию mk': 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`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N, v : P`, we have
`f.lift hg z = v ↔ g x = g y * v`, where `x : M, y ∈ S` are such that `z * f y = f x`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an
`AddCommMonoid` map `g : M →+ P` induces a map `f.lift hg : N →+ P` then for all
`z : N, v : P`, we have `f.lift hg z = v ↔ g x = g y + v`, where `x : M, y ∈ S` are such that
`z + f y = f x`. -/
]
theorem lift_spec (z v) : f.lift hg z = v ↔ g (f.sec z).1 = g (f.sec z).2 * v :=
mul_inv_left hg _ _ v
