English
In a split simplicial object, for a non-identity summand A of j, the composition (s.cofan).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id(op⟨k⟩)) equals zero; this expresses vanishing of non-identity summands under the boundary maps.
Русский
В расщепленном симплициальном объекте для неидентичного сумманта A в j, композиция (s.cofan).inj A ≫ K[X].d j k ≫ s.πSummand(IndexSet.id(op⟨k⟩)) равна нулю; выражает исчезновение неидентичных суммантов под границными отображениями.
LaTeX
$$$(s.cofan).inj_A \circ K[X].d_{j, k} \circ πSummand_{Id} = 0$ при hA$$
Lean4
/-- The differentials `s.d i j : s.N i ⟶ s.N j` on nondegenerate simplices of a split
simplicial object are induced by the differentials on the alternating face map complex. -/
@[simp]
noncomputable def d (i j : ℕ) : s.N i ⟶ s.N j :=
(s.cofan _).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌))
