Equivalences and the core of a quasicategory #
An edge e : x₀ ⟶ x₁ of a simplicial set X is an equivalence when it admits an inverse up to
2-simplices, i.e. a structure SSet.Edge.InvStruct e. When X is a quasicategory this says
exactly that e becomes an isomorphism in the homotopy category of X.
The core X.core of X is the subcomplex of the simplices all of whose edges are equivalences.
When X is a quasicategory, its core is again a quasicategory: an inner horn determines all edges
of its filler except, for Λ[2, 1], the long edge, which is a composite of two equivalences. Every
Kan complex contained in X lies in the core. That the core of a quasicategory is itself a Kan
complex, hence the largest Kan complex in X, is Joyal's theorem on special outer horns, which is
not proved here. For the nerve of a category C, the core is the nerve of the groupoid Core C.
Main definitions #
SSet.Edge.IsEquivalence: an edge admitting an inverse up to2-simplices.SSet.core: the subcomplex of simplices all of whose edges are equivalences.CategoryTheory.Core.nerveIso: the nerve ofCore Cis the core of the nerve ofC.
Main results #
SSet.Edge.isEquivalence_iff_isIso: in a quasicategory, an edge is an equivalence exactly when its class in the homotopy category is an isomorphism.SSet.Edge.CompStruct.isEquivalence₀₂,isEquivalence₀₁,isEquivalence₁₂: equivalences in a quasicategory satisfy two-out-of-three.SSet.Edge.isEquivalence_of_kanComplex: every edge of a Kan complex is an equivalence. Hence every Kan complex contained inXlies in its core (SSet.le_core_of_kanComplex), and two vertices of a Kan complex lie in the same connected component exactly when an edge joins them (SSet.π₀.mk_eq_mk_iff_nonempty_edge).SSet.le_core_iff: the core is the largest subcomplex all of whose edges are equivalences.SSet.Edge.isEquivalence_tensor_iff,SSet.core_tensor: an edge of a product is an equivalence exactly when both of its projections are, so the core of a product is the product of the cores. This makes the cores of function complexes closed under composition.SSet.range_le_core_of_unit: maps from𝟙_ SSetfactor through the core, so the cores of function complexes contain the identities.SSet.hasLiftingProperty_horn_ι_core_ι: the inclusion of the core of a quasicategory is an inner fibration, soSSet.core.quasicategory: the core of a quasicategory is a quasicategory.CategoryTheory.nerve.mem_core_iff: a simplex of the nerve of a category lies in the core exactly when all its morphisms are isomorphisms.
References #
- J. Lurie, Higher Topos Theory, §1.2.4 and §1.2.5 (Proposition 1.2.5.3).
- J. Lurie, Kerodon, Tag 01D7 (the core of an
∞-category).
An edge e of a simplicial set is an equivalence when it admits an inverse up to
2-simplices, that is, a structure e.InvStruct. In a quasicategory these are the edges that
become isomorphisms in the homotopy category (SSet.Edge.isEquivalence_iff_isIso).
Instances For
A choice of inverse structure for an equivalence.
Instances For
Transporting an edge along equalities of its endpoints does not change whether it is an equivalence.
In a quasicategory, an edge is an equivalence exactly when its class in the homotopy category is an isomorphism.
In a quasicategory, a composite of equivalences is an equivalence.
In a quasicategory, if e₀₁ and a composite e₀₂ of e₀₁ and e₁₂ are equivalences, then
so is e₁₂.
In a quasicategory, if e₁₂ and a composite e₀₂ of e₀₁ and e₁₂ are equivalences, then
so is e₀₁.
Every edge of a Kan complex is an equivalence: filling the outer horns Λ[2, 0] and
Λ[2, 2] provides a right and a left inverse in the homotopy category.
In a quasicategory, if two faces δ 2 s and δ 0 s of a 2-simplex s are equivalences,
then so is the third face δ 1 s.
The edge of a simplex s along a map f : ⦋1⦌ ⟶ n selecting the same vertex index twice is
degenerate, hence an equivalence.
In a Kan complex, two vertices lie in the same connected component exactly when there is an edge between them: edges compose, and they can be reversed since they are equivalences.
The core of a simplicial set X: the subcomplex of the simplices all of whose edges are
equivalences. When X is a quasicategory, it is the ∞-groupoid of objects of X and
equivalences between them.
Instances For
Every vertex of X lies in its core.
An edge lies in the core exactly when it is an equivalence.
A subcomplex of X lies in the core exactly when all its edges are equivalences.
A map of simplicial sets factors through the core exactly when it sends edges to equivalences.
The core of X is all of X exactly when every edge of X is an equivalence.
The core of a Kan complex is everything.
Every Kan complex contained in X lies in the core of X.
Every map from the unit 𝟙_ SSet factors through the core.
Maps from the unit 𝟙_ SSet into the core of X are the same as maps into X.
Instances For
An edge of a product X ⊗ Y is an equivalence exactly when both of its projections are.
The inclusion of the core of a quasicategory has the right lifting property against inner horn
inclusions. A filler in X of an inner horn in the core has all its edges in the horn, except for
the long edge of a filler of Λ[2, 1], which is a composite of two equivalences.
The inclusion of the core of a quasicategory is an inner fibration.
The core of a quasicategory is a quasicategory.
An edge of the nerve of a category is an equivalence exactly when the corresponding morphism is an isomorphism.
A 1-simplex of the nerve of a category is an equivalence exactly when the morphism it
represents is an isomorphism.
A simplex of the nerve of a category lies in the core exactly when all the morphisms it contains are isomorphisms.
The nerve of the core of a category is the core of its nerve.
Instances For
Under nerveIso, the inclusion of the core of the nerve corresponds to the nerve of the
inclusion of the core.
Under nerveIso, the inclusion of the core of the nerve corresponds to the nerve of the
inclusion of the core.