English
Lift a pair of monoid homomorphisms f: M →* P and g: N →* P to a monoid homomorphism lift f g : (M ∗ N) →* P.
Русский
Поднять пару гомоморфизмов моноидов f: M →* P и g: N →* P до моноидного гомоморфизма lift f g : (M ∗ N) →* P.
LaTeX
$$$ \mathrm{lift}(f,g) : (M \ast N) \to* P $$$
Lean4
/-- Lift a pair of monoid homomorphisms `f : M →* P`, `g : N →* P`
to a monoid homomorphism `M ∗ N →* P`.
See also `Coprod.clift` for a version that allows custom computational behavior
and works for a `MulOneClass` codomain.
-/
@[to_additive /-- Lift a pair of additive monoid homomorphisms `f : M →+ P`, `g : N →+ P`
to an additive monoid homomorphism `AddMonoid.Coprod M N →+ P`.
See also `AddMonoid.Coprod.clift` for a version that allows custom computational behavior
and works for an `AddZeroClass` codomain. -/
]
def lift (f : M →* P) (g : N →* P) : (M ∗ N) →* P :=
clift (FreeMonoid.lift <| Sum.elim f g) (map_one f) (map_one g) (map_mul f) (map_mul g)
