cofan_inj_πSummand_eq_zero — Mathlib

English

In a split simplicial object, the identity morphism on X.obj Δ decomposes as a finite sum of the πSummand maps composed with the corresponding cofibration injections.

Русский

В расщепленном симплициальном объекте тождество X.obj Δ разлагается как конечная сумма применённых πSummand и соответствующих инъекций кофанов.

LaTeX

$$$\mathrm{Id}_{X(\Delta)} = \sum_{A \in \text{IndexSet } \Delta} \piSummand_A \circ (cofan\, Δ)_{inj_A}$$$

Lean4

@[reassoc (attr := simp)]
theorem cofan_inj_πSummand_eq_zero [HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A B : IndexSet Δ) (h : B ≠ A) :
    (s.cofan Δ).inj A ≫ s.πSummand B = 0 := by
  dsimp [πSummand]
  rw [ι_desc, dif_neg h.symm]

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