Kan complexes #
In this file we give the definition of Kan complexes.
In Mathlib/AlgebraicTopology/Quasicategory/Basic.lean
we show that every Kan complex is a quasicategory.
TODO #
- Show that the singular simplicial set of a topological space is a Kan complex.
A simplicial set S is a Kan complex if it 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.
- hornFilling ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (σ₀ : SSet.horn (n + 1) i ⟶ S) : ∃ (σ : SSet.standardSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion (n + 1) i) σ