shiftMap_comp' — Mathlib

English

A variant of shift map behavior: the shift map of a composite equals the composite of a shift map with a shifted map, i.e., F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'.

Русский

Вариант поведения shift map: отображение сдвига композиции равно композиции отображения сдвига и shiftMap второго звена.

LaTeX

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

Lean4

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

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