σ_comp_πSummand_id_eq_zero — Mathlib

English

The component X.σ_i composed with a πSummand vanishes when i is the index of a non-identity summand of the splitting.

Русский

Компонент X.σ_i, композиция сπSummand, равен нулю для несовпадающих индексов суммирования разложения.

LaTeX

$$$X.σ_i \circ πSummand_A = 0$ whenever A ≠ Id$$

Lean4

@[reassoc (attr := simp)]
theorem σ_comp_πSummand_id_eq_zero {n : ℕ} (i : Fin (n + 1)) : X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0 :=
  by
  apply s.hom_ext'
  intro A
  dsimp only [SimplicialObject.σ]
  rw [comp_zero, s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op, cofan_inj_πSummand_eq_zero]
  rw [ne_comm]
  change ¬(A.epiComp (SimplexCategory.σ i).op).EqId
  rw [IndexSet.eqId_iff_len_eq]
  have h := SimplexCategory.len_le_of_epi A.e
  dsimp at h ⊢
  cutsat

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