Full subcategories of quasicategories

Given a predicate P on the vertices of a simplicial set X, the full enhanced subcategory X.fullEnhancedSubcategory P is the subcomplex of X consisting of the simplices all of whose vertices satisfy P. When X is a quasicategory, this is the full subcategory of the ∞-category X spanned by the objects satisfying P.

Main declarations

• SSet.fullEnhancedSubcategory: the full enhanced subcategory of X on P.
• SSet.mem_fullEnhancedSubcategory_obj_iff_forall_fin: an n-simplex lies in it exactly when each of its n + 1 vertices satisfies P.
• SSet.le_fullEnhancedSubcategory_iff: it is the largest subcomplex whose vertices satisfy P; SSet.range_le_fullEnhancedSubcategory_iff is the corresponding factorization criterion for maps into X.
• SSet.fullEnhancedSubcategory.verticesEquiv: its vertices are the vertices of X satisfying P.
• SSet.hasLiftingProperty_fullEnhancedSubcategory_ι: the inclusion has the right lifting property against every map that is surjective on vertices. In particular it is an inner fibration, so the full enhanced subcategory of a quasicategory is a quasicategory.
• CategoryTheory.ObjectProperty.nerveFullSubcategoryIso: for the nerve of an ordinary category, the full enhanced subcategory is the nerve of the full subcategory.

References

• J. Lurie, Higher Topos Theory, §1.2.11.

def SSet.fullEnhancedSubcategory (X : SSet) (P : X.obj (Opposite.op { len := 0 }) → Prop) : X.Subcomplex

The full enhanced subcategory of a simplicial set X on a predicate P on its vertices: the subcomplex of the simplices all of whose vertices satisfy P.

theorem SSet.mem_fullEnhancedSubcategory_obj_iff {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) {n : SimplexCategoryᵒᵖ} (x : X.obj n) : x ∈ (X.fullEnhancedSubcategory P).obj n ↔ ∀ (v : { len := 0 } ⟶ Opposite.unop n), P ((CategoryTheory.ConcreteCategory.hom (X.map v.op)) x)

A simplex lies in the full enhanced subcategory on P exactly when each of its vertices satisfies P.

theorem SSet.mem_fullEnhancedSubcategory_obj_iff_forall_fin {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : x ∈ (X.fullEnhancedSubcategory P).obj (Opposite.op { len := n }) ↔ ∀ (i : Fin (n + 1)), P ((CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } i).op)) x)

An n-simplex lies in the full enhanced subcategory on P exactly when each of its n + 1 vertices satisfies P.

@[simp]

theorem SSet.mem_fullEnhancedSubcategory_obj_zero_iff {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) (x : X.obj (Opposite.op { len := 0 })) : x ∈ (X.fullEnhancedSubcategory P).obj (Opposite.op { len := 0 }) ↔ P x

A vertex lies in the full enhanced subcategory on P exactly when it satisfies P.

theorem SSet.le_fullEnhancedSubcategory_iff {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) (A : X.Subcomplex) : A ≤ X.fullEnhancedSubcategory P ↔ ∀ x ∈ A.obj (Opposite.op { len := 0 }), P x

The full enhanced subcategory on P is the largest subcomplex all of whose vertices satisfy P.

theorem SSet.range_le_fullEnhancedSubcategory_iff {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) {Y : SSet} (f : Y ⟶ X) : Subcomplex.range f ≤ X.fullEnhancedSubcategory P ↔ ∀ (y : Y.obj (Opposite.op { len := 0 })), P ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) y)

A map of simplicial sets factors through the full enhanced subcategory on P exactly when it sends every vertex to a vertex satisfying P.

theorem SSet.fullEnhancedSubcategory_mono {X : SSet} {P Q : X.obj (Opposite.op { len := 0 }) → Prop} (h : P ≤ Q) : X.fullEnhancedSubcategory P ≤ X.fullEnhancedSubcategory Q

@[simp]

theorem SSet.fullEnhancedSubcategory_top (X : SSet) : X.fullEnhancedSubcategory ⊤ = ⊤

The full enhanced subcategory on the predicate that always holds is everything.

@[simp]

theorem SSet.fullEnhancedSubcategory_bot (X : SSet) : X.fullEnhancedSubcategory ⊥ = ⊥

The full enhanced subcategory on the predicate that never holds is empty.

def SSet.fullEnhancedSubcategory.verticesEquiv {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) : ↑((X.fullEnhancedSubcategory P).obj (Opposite.op { len := 0 })) ≃ { x : X.obj (Opposite.op { len := 0 }) // P x }

The vertices of the full enhanced subcategory on P are the vertices satisfying P.

@[simp]

theorem SSet.fullEnhancedSubcategory.verticesEquiv_apply_coe {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) (x : ↑((X.fullEnhancedSubcategory P).obj (Opposite.op { len := 0 }))) : ↑((verticesEquiv P) x) = ↑x

@[simp]

theorem SSet.fullEnhancedSubcategory.verticesEquiv_symm_apply_coe {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) (x : { x : X.obj (Opposite.op { len := 0 }) // P x }) : ↑((verticesEquiv P).symm x) = ↑x

theorem SSet.hasLiftingProperty_fullEnhancedSubcategory_ι {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) {A B : SSet} (i : A ⟶ B) (hi : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := 0 })))) : CategoryTheory.HasLiftingProperty i (X.fullEnhancedSubcategory P).ι

The inclusion of a full enhanced subcategory has the right lifting property against every map of simplicial sets that is surjective on vertices.

instance SSet.instInnerFibrationιFullEnhancedSubcategory {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) : InnerFibration (X.fullEnhancedSubcategory P).ι

The inclusion of a full enhanced subcategory is an inner fibration: inner horn inclusions are surjective on vertices.

instance SSet.instQuasicategoryToSSetFullEnhancedSubcategory {X : SSet} (P : X.obj (Opposite.op { len := 0 }) → Prop) [X.Quasicategory] : (X.fullEnhancedSubcategory P).toSSet.Quasicategory

The full enhanced subcategory of a quasicategory is a quasicategory.

def CategoryTheory.ObjectProperty.nerveFullSubcategoryIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : nerve P.FullSubcategory ≅ ((nerve C).fullEnhancedSubcategory fun (x : (nerve C).obj (Opposite.op { len := 0 })) => P (nerveEquiv x)).toSSet

The nerve of the full subcategory of C on P is isomorphic to the full enhanced subcategory of the nerve of C on the vertices whose object satisfies P.

@[simp]

theorem CategoryTheory.ObjectProperty.nerveFullSubcategoryIso_hom_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : CategoryStruct.comp P.nerveFullSubcategoryIso.hom ((nerve C).fullEnhancedSubcategory fun (x : (nerve C).obj (Opposite.op { len := 0 })) => P (nerveEquiv x)).ι = nerveMap P.ι

Under nerveFullSubcategoryIso, the inclusion of the full enhanced subcategory corresponds to the nerve of the inclusion of the full subcategory.

@[simp]

theorem CategoryTheory.ObjectProperty.nerveFullSubcategoryIso_hom_ι_assoc {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {Z : SSet} (h : nerve C ⟶ Z) : CategoryStruct.comp P.nerveFullSubcategoryIso.hom (CategoryStruct.comp ((nerve C).fullEnhancedSubcategory fun (x : (nerve C).obj (Opposite.op { len := 0 })) => P (nerveEquiv x)).ι h) = CategoryStruct.comp (nerveMap P.ι) h

Under nerveFullSubcategoryIso, the inclusion of the full enhanced subcategory corresponds to the nerve of the inclusion of the full subcategory.