map_add_hom_app — Mathlib

English

For shifts a and b, the image under F of the hom from the sum-shift corresponds to a composite involving the shifted hom, plus the action of the isomorphisms that track the interaction between the two shifts and shiftFunctor.

Русский

Для сдвигов a и b образ гомоморфизма от суммы сдвигов под F задаётся через композицию, включающую сдвинутые гомоморфизмы и изоморфизмы, отслеживающие взаимодействие двух сдвигов и shiftFunctor.

LaTeX

$$$ F.map ((add hF s i a b).hom.app X) = (i (a + b)).hom.app X ≫ (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ ((i a).inv.app X)⟦b⟧' ≫ (i b).inv.app ((s a).obj X) $$$

Lean4

@[simp]
theorem map_add_hom_app (a b : A) (X : C) :
    F.map ((add hF s i a b).hom.app X) =
      (i (a + b)).hom.app X ≫
        (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ ((i a).inv.app X)⟦b⟧' ≫ (i b).inv.app ((s a).obj X) :=
  by
  dsimp [add]
  simp

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