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.
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) σ
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))
:
∃ (σ : 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) σ
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