English
Given f:S LocalizationMap N and g:S.LocalizationMap P, f.lift maps f.mk' x y to g.mk' x y.
Русский
Пусть f: S LocalizationMap N и g: S LocalizationMap P, тогда f.lift отображает f.mk' x y в g.mk' x y.
LaTeX
$$$ f.lift g.map_units (f.mk' x y) = g.mk' x y $$$
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` sending `z : N` to `g x * (g y)⁻¹`, where `(x, y) : M × S` are such that
`z = f x * (f y)⁻¹`. -/
@[to_additive /-- Given a localization map `f : M →+ N` for a submonoid `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` sending `z : N` to `g x - g y`, where `(x, y) : M × S` are such that
`z = f x - f y`. -/
]
noncomputable def lift : N →* P
where
toFun z := g (f.sec z).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec z).2)⁻¹
map_one' := by rw [mul_inv_left, mul_one]; exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])
map_mul' x
y :=
by
rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ← mul_assoc, ←
mul_assoc, mul_inv_right hg]
repeat rw [← g.map_mul]
refine f.eq_of_eq hg ?_
simp_rw [map_mul, sec_spec', ← toMonoidHom_apply]
ac_rfl
