hornFilling — Mathlib

English

In the nerve of a category, the δ-face map preserves the underlying object structure via succAbove.

Русский

В нерве категории отображение δ сохраняет структуру объекта через succAbove.

LaTeX

$$$ ((\nerve C).δ i x).obj j = x.obj (i.succAbove j) $$$

Lean4

/-- A Kan complex `S` satisfies the following horn-filling condition:
for every nonzero `n : ℕ` and `0 ≤ i ≤ n`,
every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`. -/
theorem hornFilling {S : SSet.{u}} [KanComplex S] {n : ℕ} {i : Fin (n + 2)} (σ₀ : (Λ[n + 1, i] : SSet) ⟶ S) :
    ∃ σ : Δ[n + 1] ⟶ S, σ₀ = Λ[n + 1, i].ι ≫ σ :=
  by
  have sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from _) := ⟨by simp⟩
  exact ⟨sq'.lift, by simp⟩

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