English
Lift a monoid homomorphism f from FreeMonoid(M ⊕ N) to P to a monoid hom M ∗ N →* P, under additional hypotheses on its behavior on the left and right generators.
Русский
Поднять моноид-гомоморфизм f: FreeMonoid(M ⊕ N) →* P до гомоморфизма M ∗ N →* P, при условии на поведение на левых и правых генераторах.
LaTeX
$$$\mathrm{clift}: (F : FreeMonoid(M\oplus N) \to_* P) \to (h_M, h_N, h_M', h_N') \mapsto M\ast N \to_* P$ с любыми дополнительными условиями.$$
Lean4
/-- Lift a monoid homomorphism `FreeMonoid (M ⊕ N) →* P` satisfying additional properties to
`M ∗ N →* P`. In many cases, `Coprod.lift` is more convenient.
Compared to `Coprod.lift`,
this definition allows a user to provide a custom computational behavior.
Also, it only needs `MulOneClass` assumptions while `Coprod.lift` needs a `Monoid` structure.
-/
@[to_additive /-- Lift an additive monoid homomorphism `FreeAddMonoid (M ⊕ N) →+ P` satisfying
additional properties to `AddMonoid.Coprod M N →+ P`.
Compared to `AddMonoid.Coprod.lift`,
this definition allows a user to provide a custom computational behavior.
Also, it only needs `AddZeroClass` assumptions
while `AddMonoid.Coprod.lift` needs an `AddMonoid` structure. -/
]
def clift (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (of (.inl 1)) = 1) (hN₁ : f (of (.inr 1)) = 1)
(hM : ∀ x y, f (of (.inl (x * y))) = f (of (.inl x) * of (.inl y)))
(hN : ∀ x y, f (of (.inr (x * y))) = f (of (.inr x) * of (.inr y))) : M ∗ N →* P :=
Con.lift _ f <| sInf_le ⟨hM, hN, hM₁.trans (map_one f).symm, hN₁.trans (map_one f).symm⟩
