σ_comp_σ — Mathlib

English

The fifth cosimplicial identity: σ_{i.castSucc} ≫ σ_j = σ_{j.succ} ≫ σ_i for i ≤ j.

Русский

Пятое косимпликсальное тождество: σ_{i.castSucc} ∘ σ_j = σ_{j.succ} ∘ σ_i при i ≤ j.

LaTeX

$$$\sigma_{i.castSucc} \circ \sigma_j = \sigma_{j.succ} \circ \sigma_i\quad (i \le j)$$$

Lean4

/-- The fifth cosimplicial identity -/
@[reassoc]
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) : X.σ (Fin.castSucc i) ≫ X.σ j = X.σ j.succ ≫ X.σ i :=
  by
  dsimp [δ, σ]
  simp only [← X.map_comp, SimplexCategory.σ_comp_σ H]

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