Theorems · Theorem · algebraic topology

SSet.KanComplex.hornFilling

∀ {S : SSet} [S.KanComplex] {n : ℕ} {i : Fin (n + 2)} (σ₀ : (SSet.horn (n + 1) i).toSSet ⟶ S),
  ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn (n + 1) i).ι σ

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.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Cited by

0 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SSet.KanComplex