Joyal's theorem on special outer horns

In a quasicategory C, the outer horns Λ[n + 2, 0] cannot be filled in general, but they can when their initial edge, from 0 to 1, is an equivalence. Conversely, an edge all of whose outer horns Λ[n + 2, 0] can be filled is an equivalence (HTT Proposition 1.2.4.3). Together with its dual for the horns Λ[n + 2, n + 2], which is not proved here, this is the input for showing that the core of a quasicategory and its right mapping spaces are Kan complexes.

The proof follows Kerodon: under the isomorphism Δ[1] ⋆ Δ[n] ≅ Δ[n + 2], the horn Λ[n + 2, 0] is the pushout-join (Λ[1, 0] ⋆ Δ[n]) ∪ (Δ[1] ⋆ ∂Δ[n]), so filling it amounts to lifting an edge, with prescribed source, along the restriction of cones C_{/σ} ⟶ C_{/∂σ} for the face σ : Δ[n] ⟶ C opposite to the vertices 0 and 1. This restriction is a right fibration, and right fibrations lift equivalences with prescribed source. The edge to be lifted is an equivalence because its image in C is, and the projection C_{/∂σ} ⟶ C is a right fibration, which reflects equivalences. These facts about right fibrations are in TauCeti.AlgebraicTopology.Quasicategory.RightFibration, and the lifting property of the restriction of cones is SSet.slice.hasLift_of_isEquivalence.

Conversely, filling the horns Λ[2, 0] and Λ[3, 0] with initial edge e produces a right inverse of e and shows that it is also a left inverse.

Main results

• SSet.Quasicategory.hornFilling_zero: Joyal's theorem, a horn Λ[n + 2, 0] in a quasicategory whose initial edge is an equivalence can be filled.
• SSet.Edge.isEquivalence_iff_hornFilling_zero: an edge of a quasicategory is an equivalence exactly when every horn Λ[n + 2, 0] with that initial edge can be filled.

References

• A. Joyal, Quasi-categories and Kan complexes, J. Pure Appl. Algebra 175 (2002), Theorem 1.3.
• J. Lurie, Higher Topos Theory, Proposition 1.2.4.3.
• J. Lurie, Kerodon, Theorem 4.4.2.6, Proposition 4.4.2.11, Proposition 4.4.2.13 and Example 4.4.1.11.

theorem SSet.Quasicategory.hornFilling_zero {C : SSet} [C.Quasicategory] {n : ℕ} (σ₀ : (horn (n + 2) 0).toSSet ⟶ C) (h : (Edge.mk' ((CategoryTheory.ConcreteCategory.hom (σ₀.app (Opposite.op { len := 1 }))) (horn.edge (n + 2) 0 0 1 ⋯ ⋯))).IsEquivalence) : ∃ (σ : stdSimplex.obj { len := n + 2 } ⟶ C), σ₀ = CategoryTheory.CategoryStruct.comp (horn (n + 2) 0).ι σ

Joyal's theorem on special outer horns (HTT Proposition 1.2.4.3): in a quasicategory, a horn Λ[n + 2, 0] whose initial edge, from 0 to 1, is an equivalence can be filled.

theorem SSet.Edge.isEquivalence_iff_hornFilling_zero {C : SSet} {x y : C.obj (Opposite.op { len := 0 })} [C.Quasicategory] (e : Edge x y) : e.IsEquivalence ↔ ∀ (n : ℕ) (σ₀ : (horn (n + 2) 0).toSSet ⟶ C), (CategoryTheory.ConcreteCategory.hom (σ₀.app (Opposite.op { len := 1 }))) (horn.edge (n + 2) 0 0 1 ⋯ ⋯) = e.edge → ∃ (σ : stdSimplex.obj { len := n + 2 } ⟶ C), σ₀ = CategoryTheory.CategoryStruct.comp (horn (n + 2) 0).ι σ

Joyal's characterization of equivalences by special outer horns (HTT Proposition 1.2.4.3): an edge e of a quasicategory is an equivalence exactly when every horn Λ[n + 2, 0] whose initial edge is e can be filled.