Right fibrations and equivalences

A right fibration q : X ⟶ Y lifts the horns Λ[2, 2] and Λ[1, 1]; in terms of edges and 2-simplices, it lifts composition triangles with two prescribed faces, and edges with prescribed target. Lifting inverses this way shows that, when X is a quasicategory, q reflects equivalences (Kerodon Proposition 4.4.2.11), and that q lifts equivalences of Y with prescribed source (compare Kerodon Example 4.4.1.11).

Main results

• SSet.Edge.exists_compStruct_of_hasLiftingProperty_horn₂₂, SSet.Edge.exists_edge_of_hasLiftingProperty_horn₁₁: lifting against Λ[2, 2] ⟶ Δ[2] and Λ[1, 1] ⟶ Δ[1], in terms of edges and 2-simplices.
• SSet.Edge.isEquivalence_map_iff_of_rightFibration: a right fibration from a quasicategory reflects equivalences.
• SSet.RightFibration.hasLift_of_isEquivalence: a right fibration lifts equivalences with prescribed source.

References

• J. Lurie, Kerodon, Proposition 4.4.2.11 and Example 4.4.1.11.

theorem SSet.Edge.exists_compStruct_of_hasLiftingProperty_horn₂₂ {X Y : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} (q : X ⟶ Y) [CategoryTheory.HasLiftingProperty (horn 2 2).ι q] (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) (s : Y.obj (Opposite.op { len := 2 })) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y 0)) s = (CategoryTheory.ConcreteCategory.hom (q.app (Opposite.op { len := 1 }))) e₁₂.edge) (h₁ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y 1)) s = (CategoryTheory.ConcreteCategory.hom (q.app (Opposite.op { len := 1 }))) e₀₂.edge) : ∃ (e₀₁ : Edge x₀ x₁), Nonempty (e₀₁.CompStruct e₁₂ e₀₂) ∧ (CategoryTheory.ConcreteCategory.hom (q.app (Opposite.op { len := 1 }))) e₀₁.edge = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y 2)) s

If q : X ⟶ Y has the right lifting property with respect to Λ[2, 2] ⟶ Δ[2], edges e₁₂ : x₁ ⟶ x₂ and e₀₂ : x₀ ⟶ x₂ of X lying over the faces δ 0 s and δ 1 s of a 2-simplex s of Y are two faces of a 2-simplex of X, a composition structure e₀₁ ≫ e₁₂ = e₀₂, whose third face e₀₁ : x₀ ⟶ x₁ lies over δ 2 s.

theorem SSet.Edge.exists_edge_of_hasLiftingProperty_horn₁₁ {X Y : SSet} (q : X ⟶ Y) [CategoryTheory.HasLiftingProperty (horn 1 1).ι q] (x : X.obj (Opposite.op { len := 0 })) (f : Y.obj (Opposite.op { len := 1 })) (hf : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ Y 0)) f = (CategoryTheory.ConcreteCategory.hom (q.app (Opposite.op { len := 0 }))) x) : ∃ (g : X.obj (Opposite.op { len := 1 })), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) g = x ∧ (CategoryTheory.ConcreteCategory.hom (q.app (Opposite.op { len := 1 }))) g = f

If q : X ⟶ Y has the right lifting property with respect to Λ[1, 1] ⟶ Δ[1], every edge of Y ending at the image of a vertex x of X is the image of an edge of X ending at x.

theorem SSet.Edge.isEquivalence_map_iff_of_rightFibration {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} [X.Quasicategory] (q : X ⟶ Y) [RightFibration q] (e : Edge x₀ x₁) : (e.map q).IsEquivalence ↔ e.IsEquivalence

Right fibrations reflect equivalences (Kerodon Proposition 4.4.2.11): for a right fibration q : X ⟶ Y whose source is a quasicategory, an edge of X is an equivalence exactly when its image in Y is.

theorem SSet.RightFibration.hasLift_of_isEquivalence {X Y : SSet} (q : X ⟶ Y) [RightFibration q] {t : (horn 1 0).toSSet ⟶ X} {b : stdSimplex.obj { len := 1 } ⟶ Y} (sq : CategoryTheory.CommSq t (horn 1 0).ι q b) (hb : (Edge.mk' (yonedaEquiv b)).IsEquivalence) : sq.HasLift

Right fibrations lift equivalences with prescribed source (compare Kerodon Example 4.4.1.11): for a right fibration q : X ⟶ Y, a commutative square from the inclusion Λ[1, 0] ⟶ Δ[1] of the vertex 0 to q has a lift when its bottom edge is an equivalence.