English
There is a canonical monoid homomorphism swap: Coprod M N → Coprod N M, swapping the two summands (sending inl m to inr m and inr n to inl n).
Русский
Существует каноническое отображение-моноид swap: Coprod M N → Coprod N M, которое переставляет две составные части (inl m ↦ inr m, inr n ↦ inl n).
LaTeX
$$$ \mathrm{swap}_{M,N} : \mathrm{Coprod}(M,N) \to \mathrm{Coprod}(N,M) $$$
Lean4
/-- Map `M ∗ N` to `N ∗ M` by applying `Sum.swap` to each element of the underlying list.
See also `MulEquiv.coprodComm` for a `MulEquiv` version. -/
@[to_additive /-- Map `AddMonoid.Coprod M N` to `AddMonoid.Coprod N M`
by applying `Sum.swap` to each element of the underlying list.
See also `AddEquiv.coprodComm` for an `AddEquiv` version. -/
]
def swap : M ∗ N →* N ∗ M :=
clift (mk.comp <| FreeMonoid.map Sum.swap)
(by simp only [MonoidHom.comp_apply, map_of, Sum.swap_inl, mk_of_inr, map_one])
(by simp only [MonoidHom.comp_apply, map_of, Sum.swap_inr, mk_of_inl, map_one])
(fun x y => by simp only [MonoidHom.comp_apply, map_of, Sum.swap_inl, mk_of_inr, map_mul])
(fun x y => by simp only [MonoidHom.comp_apply, map_of, Sum.swap_inr, mk_of_inl, map_mul])
