shiftMap_comp — Mathlib

English

For a composable pair of morphisms f: X → Y and g: Y → Z with a shift n, the shift map of the composite equals the right-hand side of shifting f first then applying g, i.e., F.shiftMap (f ≫ g) a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g.

Русский

Для пары совместимых морфизмов f: X → Y и g: Y → Z сдвигом n, отображение сдвига композиции равно правой части: переносим сначала f, затем применяем g.

LaTeX

$$$F.shiftMap (f \gg g) a a' ha' = F.shiftMap f a a' ha' \gg (F.shift a').map g$$$

Lean4

@[reassoc]
theorem shiftMap_comp {X Y Z : C} {n : M} (f : X ⟶ Y⟦n⟧) (g : Y ⟶ Z) (a a' : M) (ha' : n + a = a') :
    F.shiftMap (f ≫ g⟦n⟧') a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g := by simp [shiftMap]

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