Quasicategories

In this file we define quasicategories, a common model of infinity categories. We show that every Kan complex is a quasicategory.

In Mathlib/AlgebraicTopology/Nerve.lean we show (TODO) that the nerve of a category is a quasicategory.

TODO

• Generalize the definition to higher universes. See the corresponding TODO in Mathlib/AlgebraicTopology/KanComplex.lean.

class SSet.Quasicategory (S : SSet) : Prop

A simplicial set S is a quasicategory if it satisfies the following horn-filling condition: for every n : ℕ and 0 < i < n, every map of simplicial sets σ₀ : Λ[n, i] → S can be extended to a map σ : Δ[n] → S.

[Kerodon, 003A]

• hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : SSet.horn (n + 2) i ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ (σ : SSet.standardSimplex.obj (SimplexCategory.mk (n + 2)) ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion (n + 2) i) σ

theorem SSet.Quasicategory.hornFilling {S : SSet} [S.Quasicategory] ⦃n : ℕ⦄ ⦃i : Fin (n + 1)⦄ (h0 : 0 < i) (hn : i < Fin.last n) (σ₀ : SSet.horn n i ⟶ S) : ∃ (σ : SSet.standardSimplex.obj (SimplexCategory.mk n) ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion n i) σ

instance SSet.instQuasicategoryOfKanComplex (S : SSet) [S.KanComplex] : S.Quasicategory

Every Kan complex is a quasicategory.

[Kerodon, 003C]

Equations

• ⋯ = ⋯

theorem SSet.quasicategory_of_filler (S : SSet) (filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : SSet.horn (n + 2) i ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ (σ : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))), ∀ (j : Fin (n + 3)) (h : j ≠ i), CategoryTheory.SimplicialObject.δ S j σ = σ₀.app (Opposite.op (SimplexCategory.mk (n + 1))) (SSet.horn.face i j h)) : S.Quasicategory