English
Let M,N be monoids. The natural inclusion inl: M →* M × N maps m to (m,1), providing the left embedding of M into the product.
Русский
Пусть M,N — моноиды. Натуральное включение inl: M →* M × N отправляет m в (m,1), образуя левую вложенность M в произведение.
LaTeX
$$$ \\operatorname{inl}: M \\to M \\times N ,\\quad \\operatorname{inl}(m) = (m,1). $$$
Lean4
/-- Given monoids `M`, `N`, the natural inclusion homomorphism from `M` to `M × N`. -/
@[to_additive /-- Given additive monoids `A`, `B`, the natural inclusion homomorphism
from `A` to `A × B`. -/
]
def inl : M →* M × N :=
{ toFun := fun x => (x, 1), map_one' := rfl, map_mul' := fun _ _ => Prod.ext rfl (one_mul 1).symm }
