English
Flipping the two-argument structure of monoid homomorphisms is itself a monoid homomorphism. Specifically, the map flipHom: (M →* N →* P) →* N →* M →* P satisfies toFun = MonoidHom.flip and preserves the monoid structure.
Русский
Переворот пары аргументов гомоморфизмов Моноидов сам по себе образует гомоморфизм моноидов. Точнее, flipHom: (M →* N →* P) →* N →* M →* P задаётся как toFun = MonoidHom.flip и сохраняет структуру моноида.
LaTeX
$$$\\mathrm{flipHom} : (M \\to^* N \\to^* P) \\to^* N \\to^* M \\to^* P, \\quad \\mathrm{flipHom}(F) = \\mathrm{MonoidHom.flip}(F).$$$
Lean4
/-- Flipping arguments of monoid morphisms (`MonoidHom.flip`) as a monoid morphism. -/
@[to_additive (attr := simps) /-- Flipping arguments of additive monoid morphisms (`AddMonoidHom.flip`)
as an additive monoid morphism. -/
]
def flipHom {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} : (M →* N →* P) →* N →* M →* P
where
toFun := MonoidHom.flip
map_one' := rfl
map_mul' _ _ := rfl
