Kan complexes

In this file, the abbreviation KanComplex is introduced for fibrant objects in the category SSet which is equipped with Kan fibrations.

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.

@[reducible, inline]

abbrev SSet.KanComplex (S : SSet) : Prop

A simplicial set S is a Kan complex if it is fibrant, which means that the projection S ⟶ ⊤_ _ has the right lifting property with respect to horn inclusions.

Equations

• S.KanComplex = HomotopicalAlgebra.IsFibrant S

theorem SSet.KanComplex.hornFilling {S : SSet} [S.KanComplex] {n : ℕ} {i : Fin (n + 2)} (σ₀ : (horn (n + 1) i).toSSet ⟶ S) : ∃ (σ : stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (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.