cofan_inj_comp_PInfty_eq_zero — Mathlib

English

Composing the PInfty projection with the πSummand corresponding to the identity yields the same projection, i.e., PInfty.f_n composed with πSummand_id equals πSummand_id.

Русский

Сочетая PInfty и πSummand для идентичности, получаем ту же проекцию: PInfty.f_n ∘ πSummand_id = πSummand_id.

LaTeX

$$$PInfty.f n \circ πSummand(Id) = πSummand(Id)$$$

Lean4

/-- If a simplicial object `X` in an additive category is split,
then `PInfty` vanishes on all the summands of `X _⦋n⦌` which do
not correspond to the identity of `⦋n⦌`. -/
theorem cofan_inj_comp_PInfty_eq_zero {X : SimplicialObject C} (s : SimplicialObject.Splitting X) {n : ℕ}
    (A : SimplicialObject.Splitting.IndexSet (op ⦋n⦌)) (hA : ¬A.EqId) : (s.cofan _).inj A ≫ PInfty.f n = 0 :=
  by
  rw [SimplicialObject.Splitting.IndexSet.eqId_iff_mono] at hA
  rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e hA, comp_zero]

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