δ_comp_δ' — Mathlib

English

A generic δ-δ' relation for the first simplicial identity in a simplicial object: δ_j ≫ δ_i = δ_{i.castSucc} ≫ δ_j under a suitable order constraint.

Русский

Универсальное отношение δ-δ' для первой симпликал-идентичности: δ_j ∘ δ_i = δ_{castSucc(i)} ∘ δ_j при условии порядка.

LaTeX

$$$X.\delta_j \circ X.\delta_i = X.\delta_{i.castSucc} \circ X.\delta_j$$$

Lean4

@[reassoc]
theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
    X.δ j ≫ X.δ i = X.δ (Fin.castSucc i) ≫ X.δ (j.pred fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) :=
  by
  dsimp [δ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]

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