lift_swap — Mathlib

English

Let f:M →* P, g₁:N →* P, g₂: from N to P be monoid homomorphisms. Then f ∘ lift g₁ g₂ = lift (f ∘ g₁) (f ∘ g₂); i.e., composition distributes over lift.

Русский

Пусть f:M →* P, g₁:N →* P, g₂: N →* P. Тогда f ∘ (lift g₁ g₂) = lift (f ∘ g₁) (f ∘ g₂); то есть композиция с f распространяется на lift.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem lift_swap (f : M →* P) (g : N →* P) (x : N ∗ M) : lift f g (swap N M x) = lift g f x :=
  DFunLike.congr_fun (lift_comp_swap f g) x

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