δ_comp_σ_succ — Mathlib

English

Let n be a natural number and i an index in Fin(n+1). Then the composition δ_{i+1} ∘ σ_i equals the identity on the n-simplex Δ^n.

Русский

Пусть n — натуральное число и i — индекс из Fin(n+1). Тогда композиция δ_{i+1} ∘ σ_i равна тождественному отображению на n-(simplex)Δ^n.

LaTeX

$$$\delta_{i+1} \circ \sigma_i = \mathrm{id}_{\Delta^n}$$$

Lean4

@[reassoc]
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 (mk n) :=
  by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_σ_succ

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