πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty

English

For a non-identity index A in a splitting, the composition (s.cofan Δ).inj A ≫ PInfty.f n equals zero, i.e., PInfty annihilates non-identity summands when precomposed with the corresponding injection.

Русский

Для неидентичного индекса A в разложении композиция (s.cofan Δ).inj A ≫ PInfty.f n равна нулю; то есть PInfty аннигилирует неидентичную часть, когда её инъекция применяется до PInfty.

LaTeX

$$$ (s.cofan Δ).inj A \circ PInfty.f n = 0$ для не-Identity A$$

Lean4

@[reassoc (attr := simp)]
theorem πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty (n : ℕ) :
    s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan _).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n = PInfty.f n :=
  by
  conv_rhs => rw [← id_comp (PInfty.f n)]
  dsimp only [AlternatingFaceMapComplex.obj_X]
  rw [s.decomposition_id, Preadditive.sum_comp]
  rw [Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)), assoc]
  rintro A (hA : ¬A.EqId)
  rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

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