σ_comp_σ — Mathlib

English

For n, and indices i, j in Fin(n+1) with i ≤ j, the degeneracy maps commute according to σ_i.castSucc ∘ σ_j = σ_j.succ ∘ σ_i.

Русский

Для n и индексов i, j ∈ Fin(n+1) при i ≤ j выполняется σ_i.castSucc ∘ σ_j = σ_j.succ ∘ σ_i.

LaTeX

$$$\sigma_{i}^{\mathrm{castSucc}} \circ \sigma_j = \sigma_{j+1} \circ \sigma_i \quad\text{если } i \le j$$$

Lean4

@[reassoc]
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) : σ i.castSucc ≫ σ j = σ j.succ ≫ σ i :=
  by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.σ_comp_σ H

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