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/Quasicategory/Nerve.lean, we show that the nerve of a category is a quasicategory.

TODO

• Generalize the definition to higher universes. See the corresponding TODO in Mathlib/AlgebraicTopology/SimplicialSet/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.

• hornFilling' ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (horn (n + 2) i).toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)) : ∃ (σ : stdSimplex.obj { len := n + 2 } ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (horn (n + 2) i).ι σ

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

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

Every Kan complex is a quasicategory.

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

theorem SSet.quasicategory_of_hasLiftingProperty (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) (h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (horn n i).ι (t.from S)) : S.Quasicategory

theorem SSet.Quasicategory.hasLiftingProperty (S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) (hn : i < Fin.last n) : CategoryTheory.HasLiftingProperty (horn n i).ι (t.from S)

theorem SSet.quasicategory_iff_hasLiftingProperty (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) : S.Quasicategory ↔ ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (horn n i).ι (t.from S)