decomposition_id — Mathlib

English

In a split simplicial object, the injection along a cofan composed with a πSummand equals the identity on the corresponding summand when summing over the index set.

Русский

В расщепленном симплициальном объекте инъекция вдоль кофана, умноженная на πSummand, равна тождественному отображению на соответствующем суммоделе при суммировании по индексу.

LaTeX

$$$(s.cofan \Delta).inj A \circ s.πSummand A = \mathrm{Id}$ на соответствующем summand, summed over A.$$

Lean4

theorem decomposition_id (Δ : SimplexCategoryᵒᵖ) : 𝟙 (X.obj Δ) = ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A :=
  by
  apply s.hom_ext'
  intro A
  dsimp
  erw [comp_id, comp_sum, Finset.sum_eq_single A, cofan_inj_πSummand_eq_id_assoc]
  · intro B _ h₂
    rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ h₂, zero_comp]
  · simp

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