English
For x ∈ R and y ∈ M, the lift sends the basic localization element mk'(S, x, y) to g(x) times the inverse of the image of y in P, i.e., g(x) · (g(y))^{-1}.
Русский
Для x ∈ R и y ∈ M отображение lift отправляет базовый элемент локализации mk'(S, x, y) в произведение g(x) на (g(y))^{-1}.
LaTeX
$$$ \\mathrm{lift}\\;hg\\; (\\mathrm{mk}'\\; S\\; x\\; y) = g x \\cdot \\big( g y \\big)^{-1}, \\quad y \\in M, \\ x \\in R. $$$
Lean4
/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →+* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` sending `z : S` to `g x * (g y)⁻¹`, where `(x, y) : R × M` are such that
`z = f x * (f y)⁻¹`. -/
noncomputable def lift {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) : S →+* P :=
{ (toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg with
map_add' := by
intro x y
dsimp
rw [(toLocalizationMap M S).lift₀_def, (toLocalizationMap M S).lift_spec, mul_add, mul_comm, eq_comm,
lift_spec_mul_add, add_comm, mul_comm, mul_assoc, mul_comm, mul_assoc, lift_spec_mul_add]
simp_rw [← mul_assoc]
change g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _
simp_rw [← map_mul g, ← map_add g]
apply eq_of_eq (S := S) hg
simp only [sec_spec', toLocalizationMap_sec, map_add, map_mul]
ring }
