comp_liftAddHom — Mathlib

English

Composition of a map with a lift distributes as a lifted map of compositions.

Русский

Сложение по композиции и подъёму гомоморфизма распределяется как подъем композиции.

LaTeX

$$$$ g .\mathrm{comp} (\mathrm{liftAddHom} f) = \mathrm{liftAddHom} (\lambda a, g . (f a)) . $$$$

Lean4

theorem comp_liftAddHom [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (f : α → M →+ N) :
    g.comp ((liftAddHom (α := α) (M := M) (N := N)) f) =
      (liftAddHom (α := α) (M := M) (N := P)) fun a => g.comp (f a) :=
  liftAddHom.symm_apply_eq.1 <|
    funext fun a => by rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

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