karoubi_alternatingFaceMapComplex_d

English

In Karoubi context, the alternating face map complex preserves the Karoubi-structure on objects and morphisms.

Русский

В контексте Карауби чередующийся лицевой отображающий комплекс сохраняет структуру Карауби на объектах и морфизмах.

LaTeX

$$$((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n+1) n).f = P.p.app (op ⟦n+1⟧) \circ ((AlternatingFaceMapComplex.obj P.X).d (n+1) n)$$$

Lean4

theorem karoubi_alternatingFaceMapComplex_d (P : Karoubi (SimplicialObject C)) (n : ℕ) :
    ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
      P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n :=
  by
  dsimp
  simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum, Karoubi.zsmul_hom,
    Preadditive.comp_zsmul]
  rfl

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