ιSummand_comp_d_comp_πSummand_eq_zero

English

As in the previous statement, but in the associative form with the indexed Δ and the corresponding i, the composition (s.cofan).inj A ≫ K[X].d i k ≫ s.πSummand (IndexSet.id(op⟨k⟩)) equals zero for non-identity A; the associativity is used to reduce to the previous case.

Русский

Как и в предыдущем утверждении, в ассоциативной форме для индексированного Δ и i композиция равна нулю для неидентичного A: (s.cofan).inj A ≫ K[X].d i k ≫ s.πSummand(IndexSet.id(op⟨k⟩)) = 0.

LaTeX

$$$ (s.cofan).inj_A \circ K[X].d_{i,k} \circ πSummand_{Id} = 0$ для неидентичного A$$

Lean4

theorem ιSummand_comp_d_comp_πSummand_eq_zero (j k : ℕ) (A : IndexSet (op ⦋j⦌)) (hA : ¬A.EqId) :
    (s.cofan _).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0 :=
  by
  rw [A.eqId_iff_mono] at hA
  rw [← assoc, ← s.comp_PInfty_eq_zero_iff, assoc, ← PInfty.comm j k, s.cofan_inj_eq, assoc,
    degeneracy_comp_PInfty_assoc X j A.e hA, zero_comp, comp_zero]

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