English
There is a natural equivalence between semigroup homomorphisms α →ₙ* β and monoid homomorphisms WithOne α →* β, given by lift; its inverse sends a monoid homito back by composing with the canonical inclusion α → WithOne α.
Русский
Существует естественное эквивалентное соответствие между полугомоморфизмами секмогрупп α →ₙ* β и монойд-гомоморфизмами WithOne α →* β; это отображение lift, а обратное восстанавливается через композицию с вложением α → WithOne α.
LaTeX
$$$\mathrm{lift} : (\alpha \to_{\mathrm{n}*} \beta) \simeq (\mathrm{WithOne}\ \alpha \to_* \beta)$$$
Lean4
/-- Lift a semigroup homomorphism `f` to a bundled monoid homomorphism. -/
@[to_additive /-- Lift an additive semigroup homomorphism `f` to a bundled additive monoid homomorphism. -/
]
def lift : (α →ₙ* β) ≃ (WithOne α →* β)
where
toFun
f :=
{ toFun := fun x => Option.casesOn x 1 f, map_one' := rfl,
map_mul' := fun x y =>
WithOne.cases_on x (by rw [one_mul]; exact (one_mul _).symm)
(fun x => WithOne.cases_on y (by rw [mul_one]; exact (mul_one _).symm) (fun y => f.map_mul x y)) }
invFun F := F.toMulHom.comp coeMulHom
right_inv F := MonoidHom.ext fun x => WithOne.cases_on x F.map_one.symm (fun _ => rfl)
