English
Given a localization map F away from x and a map g with g(x) invertible, there exists a unique homomorphism from N to P extending g, i.e., a lift F.lift x hg: N →* P with F.lift x hg ∘ F = g.
Русский
Дано локализационная карта F away от x и отображение g с invertible g(x); существует единственный гомоморфизм l: N → P, который расширяет g, т.е. l ∘ F = g.
LaTeX
$$∃! l: N →* P, l ∘ F = g$$
Lean4
/-- Given `x : M`, a Localization map `F : M →* N` away from `x`, and a map of `CommMonoid`s
`g : M →* P` such that `g x` is invertible, the homomorphism induced from `N` to `P` sending
`z : N` to `g y * (g x)⁻ⁿ`, where `y : M, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`. -/
noncomputable def lift (hg : IsUnit (g x)) : N →* P :=
Submonoid.LocalizationMap.lift F fun y ↦
show IsUnit (g y.1) by
obtain ⟨n, hn⟩ := y.2
rw [← hn, g.map_pow]
exact IsUnit.pow n hg
