Documentation

Mathlib.AlgebraicTopology.Quasicategory

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 #

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]

Instances
    theorem SSet.Quasicategory.hornFilling' {S : SSet} [self : S.Quasicategory] ⦃n : ⦃i : Fin (n + 3) (σ₀ : SSet.horn (n + 2) i S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)) :
    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) :
    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 < ii < 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