English
Let M be a commutative monoid, and let x ∈ M and y ∈ M. Given localization maps F : AwayMap x N and G : AwayMap (x·y) P away from x and from x y respectively, there is a canonical monoid homomorphism from N to P obtained by transporting along these localizations.
Русский
Пусть M — коммутативный моноид, x ∈ M и y ∈ M. При данных локализационных картах F : AwayMap x N и G : AwayMap (x·y) P, локализация порождает канонический гомоморфизм моноидов от N к P, получаемый переносом через локализации соответствующим образом.
LaTeX
$$$ awayToAwayRight(y, G) : \mathrm{MonoidHom}(N, P) $$$
Lean4
/-- Given `x y : M` and Localization maps `F : M →* N, G : M →* P` away from `x` and `x * y`
respectively, the homomorphism induced from `N` to `P`. -/
noncomputable def awayToAwayRight (y : M) (G : AwayMap (x * y) P) : N →* P :=
F.lift x <|
show IsUnit (G x) from
isUnit_of_mul_eq_one (G x) (G.mk' y ⟨x * y, mem_powers _⟩) <| by rw [mul_mk'_eq_mk'_of_mul, mk'_self]
