Slices of quasicategories

For a quasicategory C and a diagram p : K ⟶ C, the slice C_{/p} is again a quasicategory, and its projection C_{/p} ⟶ C has the right lifting property with respect to the horn inclusions Λ[m, i] ⟶ Δ[m] with 0 < i, including the final horns Λ[m, m]; that is, it is a right fibration in the sense of Higher Topos Theory, §2.1.2. The slice is the quasicategory of cones over p, and a limit of p is a final object of it.

A lifting problem of Λ[m, i] ⟶ Δ[m] against C_{/p} ⟶ C is an extension problem for maps into C along (Λ[m, i] ⋆ K) ∪ Δ[m] ⟶ Δ[m] ⋆ K. Through the universal property of the coslice, such extension problems along (Λ[m, i] ⋆ Y) ∪ (Δ[m] ⋆ X) ⟶ Δ[m] ⋆ Y, for a monomorphism X ⟶ Y, are lifting problems of X ⟶ Y against the restriction of cocones C_{σ/} ⟶ C_{(Λ[m, i] ⟶ Δ[m] ⟶ C)/} for a simplex σ : Δ[m] ⟶ C. This restriction is a trivial fibration: by Mathlib's description of the trivial fibrations as the maps lifting against boundary inclusions (SSet.rlp_monomorphisms), it suffices to treat ∂Δ[n] ⟶ Δ[n], where the pushout-join (Λ[m, i] ⋆ Δ[n]) ∪ (Δ[m] ⋆ ∂Δ[n]) is the inner horn Λ[m + n + 1, i].

More generally, for a monomorphism j : L ⟶ K and 0 < i, a lifting problem of Λ[m, i] ⟶ Δ[m] against the restriction of cones C_{/p} ⟶ C_{/j ≫ p} is a lifting problem of j against the restriction of cocones C_{σ/} ⟶ C_{(Λ[m, i] ⟶ Δ[m] ⟶ C)/} along Λ[m, i] ⟶ Δ[m], a trivial fibration, so the restriction of cones is a right fibration. As a right fibration over a quasicategory, it lifts with prescribed source every edge whose image in C is an equivalence.

Main results

• SSet.coslice.hasLiftingProperty_map_horn_ι: for a quasicategory C, a simplex σ : Δ[m] ⟶ C and 0 < i, restriction of cocones C_{σ/} ⟶ C_{(Λ[m, i] ⟶ Δ[m] ⟶ C)/} has the right lifting property with respect to every monomorphism.
• SSet.slice.hasLiftingProperty_horn_ι_π: for a quasicategory C and 0 < i, the projection C_{/p} ⟶ C has the right lifting property with respect to Λ[m, i] ⟶ Δ[m].
• SSet.slice.rightFibration_π, SSet.slice.quasicategory: the projection of the slice of a quasicategory is a right fibration, and the slice is a quasicategory.
• SSet.slice.hasLiftingProperty_horn_ι_map, SSet.slice.rightFibration_map: for a monomorphism j : L ⟶ K, the restriction of cones C_{/p} ⟶ C_{/j ≫ p} is a right fibration.
• SSet.slice.hasLift_of_isEquivalence: this restriction lifts, with prescribed source, every edge whose image in C is an equivalence.

Implementation notes

The reduction of SSet.coslice.hasLiftingProperty_map_horn_ι to boundary inclusions and an inner anodyne pushout-join follows the shape of the proof of Mathlib's SSet.innerFibration_pullbackObjObjπ by Jack McKoen and Joël Riou, with coslices playing the role of the internal hom.

References

• J. Lurie, Higher Topos Theory, Lemma 2.1.2.3, Proposition 2.1.2.1 and Corollary 2.1.2.2.
• A. Joyal, Quasi-categories and Kan complexes, J. Pure Appl. Algebra 175 (2002).

theorem SSet.coslice.hasLiftingProperty_map_horn_ι {C : SSet} {m : ℕ} {i : Fin (m + 1)} [C.Quasicategory] (hi : 0 < i) (σ : stdSimplex.obj { len := m } ⟶ C) {X Y : SSet} (j : X ⟶ Y) [CategoryTheory.Mono j] : CategoryTheory.HasLiftingProperty j (map (horn m i).ι (CategoryTheory.CategoryStruct.id C) ⋯)

For a quasicategory C, a simplex σ : Δ[m] ⟶ C and 0 < i, the restriction of cocones C_{σ/} ⟶ C_{(Λ[m, i] ⟶ Δ[m] ⟶ C)/} is a trivial fibration: it has the right lifting property with respect to every monomorphism j : X ⟶ Y. Through the universal property of the coslice, this says that maps (Λ[m, i] ⋆ Y) ∪ (Δ[m] ⋆ X) ⟶ C extending σ extend to Δ[m] ⋆ Y.

theorem SSet.slice.hasLiftingProperty_horn_ι_π {K C : SSet} {m : ℕ} {i : Fin (m + 1)} [C.Quasicategory] (p : K ⟶ C) (hi : 0 < i) : CategoryTheory.HasLiftingProperty (horn m i).ι (π p)

For a quasicategory C and 0 < i, the projection C_{/p} ⟶ C of a slice has the right lifting property with respect to the horn inclusion Λ[m, i] ⟶ Δ[m]. This includes the final horns Λ[m, m], so the projection is a right fibration.

instance SSet.slice.rightFibration_π {K C : SSet} [C.Quasicategory] (p : K ⟶ C) : RightFibration (π p)

The projection of the slice of a quasicategory is a right fibration, hence an inner fibration.

instance SSet.slice.quasicategory {K C : SSet} [C.Quasicategory] (p : K ⟶ C) : (slice p).Quasicategory

The slice of a quasicategory is a quasicategory (Joyal).

theorem SSet.slice.hasLiftingProperty_horn_ι_map {K C : SSet} {m : ℕ} {i : Fin (m + 1)} {L : SSet} [C.Quasicategory] (p : K ⟶ C) (j : L ⟶ K) [CategoryTheory.Mono j] (hi : 0 < i) : CategoryTheory.HasLiftingProperty (horn m i).ι (map j (CategoryTheory.CategoryStruct.id C) ⋯)

For a quasicategory C, a diagram p : K ⟶ C, a monomorphism j : L ⟶ K and 0 < i, the restriction of cones C_{/p} ⟶ C_{/j ≫ p} has the right lifting property with respect to the horn inclusion Λ[m, i] ⟶ Δ[m]. Through the universal property of the slice, this says that maps (Λ[m, i] ⋆ K) ∪ (Δ[m] ⋆ L) ⟶ C extend to Δ[m] ⋆ K.

instance SSet.slice.rightFibration_map {K C L : SSet} [C.Quasicategory] (p : K ⟶ C) (j : L ⟶ K) [CategoryTheory.Mono j] : RightFibration (map j (CategoryTheory.CategoryStruct.id C) ⋯)

For a quasicategory C and a monomorphism j : L ⟶ K, the restriction of cones C_{/p} ⟶ C_{/j ≫ p} is a right fibration.

theorem SSet.slice.hasLift_of_isEquivalence {K C L : SSet} [C.Quasicategory] (p : K ⟶ C) (j : L ⟶ K) [CategoryTheory.Mono j] {t : (horn 1 0).toSSet ⟶ slice p} {b : stdSimplex.obj { len := 1 } ⟶ slice (CategoryTheory.CategoryStruct.comp j p)} (sq : CategoryTheory.CommSq t (horn 1 0).ι (map j (CategoryTheory.CategoryStruct.id C) ⋯) b) (hb : (Edge.mk' (yonedaEquiv (CategoryTheory.CategoryStruct.comp b (π (CategoryTheory.CategoryStruct.comp j p))))).IsEquivalence) : sq.HasLift

For a quasicategory C, a diagram p : K ⟶ C and a monomorphism j : L ⟶ K, the restriction of cones C_{/p} ⟶ C_{/j ≫ p} lifts, with prescribed source, every edge whose image in C is an equivalence: a commutative square from Λ[1, 0] ⟶ Δ[1] to it has a lift when the edge of C underlying its bottom edge is an equivalence. Through the universal property of the slice, maps (Λ[1, 0] ⋆ K) ∪ (Δ[1] ⋆ L) ⟶ C extend to Δ[1] ⋆ K when their edge Δ[1] ⟶ C is an equivalence.