English
Let f:M →* P, g:N →* P. The map (lift f g).comp (swap N M) equals lift g f; i.e., the lifting is compatible with swapping the inputs.
Русский
Пусть f:M →* P, g:N →* P. Отображение (lift f g) ∘ (swap N M) равняется lift g f; то есть lift совместим с перестановкой аргументов.
LaTeX
$$$\\\\forall f:M \\\\to^* P\\\\, \\\\forall g:N \\\\to^* P\\\\, ((lift f g).\\\\circ (\\\\mathrm{swap} \\\\ N \\\\ M)) = lift g f.$$$
Lean4
@[to_additive]
theorem comp_lift {P' : Type*} [Monoid P'] (f : P →* P') (g₁ : M →* P) (g₂ : N →* P) :
f.comp (lift g₁ g₂) = lift (f.comp g₁) (f.comp g₂) :=
hom_ext (by rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]) <| by
rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]
