lift_comp_swap — Mathlib

English

Let M,N,P be monoids and f:M →* P, g:N →* P. Then (lift f g) ∘ (swap N M) = lift g f; i.e., the lift is symmetric with respect to swapping the summands.

Русский

Пусть M, N, P — моноиды и f:M →* P, g:N →* P. Тогда (lift f g) ∘ (swap N M) = lift g f; то есть при обмене компонент копруд тоже сохраняется.

LaTeX

$$$\\\\forall f:M \\\\to^* P\\\\, \\\\forall g:N \\\\to^* P\\\\, (\\\\mathrm{lift} \\\\ f \\\\ g) \\\\circ (\\\\mathrm{swap} \\\\ N \\\\ M) = \\\\mathrm{lift} \\\\ g \\\\ f.$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_comp_swap (f : M →* P) (g : N →* P) : (lift f g).comp (swap N M) = lift g f :=
  hom_ext rfl rfl

Похожие утверждения