2-truncated quasicategories and homotopy relations

We define 2-truncated quasicategories Quasicategory₂ by three horn-filling properties, and the left and right homotopy relations HomotopicL and HomotopicR on the edges in a 2-truncated simplicial set.

We prove that for 2-truncated quasicategories, both homotopy relations are equivalence relations, and that the left and right homotopy relations coincide.

For a 2-truncated quasicategory A, we define a category HomotopyCategory₂ A whose morphisms are given by (left) homotopy classes of edges. The construction of this category is different from HomotopyCategory A in AlgebraicTopology.SimplicialSet.HomotopyCat:

• HomotopyCategory₂ A has morphisms given by homotopy classes of edges
• HomotopyCategory A has morphisms given by equivalence classes of paths in the underlying reflexive quiver of A.

The two constructions agree for 2-truncated quasicategories (TODO: handled by future PR).

Implementation notes

Throughout this file, we make use of Edge and CompStruct to conveniently deal with edges and triangles in a 2-truncated simplicial set.

class SSet.Truncated.Quasicategory₂ (X : Truncated 2) : Prop

A 2-truncated quasicategory is a 2-truncated simplicial set with the properties:

• (2, 1)-filling: given two consecutive Edges e₀₁ and e₁₂, there exists a CompStruct with (0, 1)-edge e₀₁ and (0, 2)-edge e₁₂.
• (3, 1)-filling: given three CompStructs f₃, f₀ and f₂ which form a (3, 1)-horn, there exists a fourth CompStruct such that the four faces form the boundary ∂Δ[3] of a 3-simplex.
• (3, 2)-filling: given three CompStructs f₃, f₀ and f₁ which form a (3, 2)-horn, there exists a fourth CompStruct such that the four faces form the boundary ∂Δ[3] of a 3-simplex.

• fill21 {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) : Nonempty ((e₀₂ : Edge x₀ x₂) × e₀₁.CompStruct e₁₂ e₀₂)
• fill31 {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) : Nonempty (e₀₂.CompStruct e₂₃ e₀₃)
• fill32 {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) : Nonempty (e₀₁.CompStruct e₁₃ e₀₃)

@[reducible, inline]

abbrev SSet.Truncated.HomotopicL {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} (f g : Edge x y) : Prop

Two edges f and g are left homotopic if there is a CompStruct with (0, 1)-edge f, (1, 2)-edge Edge.id and (0, 2)-edge g. We use Nonempty to have a Prop valued HomotopicL.

@[reducible, inline]

abbrev SSet.Truncated.HomotopicR {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} (f g : Edge x y) : Prop

Two edges f and g are right homotopic if there is a CompStruct with (0, 1)-edge Edge.id, (1, 2)-edge f, and (0, 2)-edge g. We use Nonempty to have a Prop valued HomotopicR.

theorem SSet.Truncated.HomotopicL.refl {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f : Edge x y} : HomotopicL f f

The left homotopy relation is reflexive.

theorem SSet.Truncated.HomotopicL.symm {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} (hfg : HomotopicL f g) : HomotopicL g f

The left homotopy relation is symmetric.

theorem SSet.Truncated.HomotopicL.trans {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g h : Edge x y} (hfg : HomotopicL f g) (hgh : HomotopicL g h) : HomotopicL f h

The left homotopy relation is transitive.

theorem SSet.Truncated.HomotopicR.refl {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f : Edge x y} : HomotopicR f f

The right homotopy relation is reflexive.

theorem SSet.Truncated.HomotopicR.symm {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} (hfg : HomotopicR f g) : HomotopicR g f

The right homotopy relation is symmetric.

theorem SSet.Truncated.HomotopicR.trans {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g h : Edge x y} (hfg : HomotopicR f g) (hgh : HomotopicR g h) : HomotopicR f h

The right homotopy relation is transitive.

theorem SSet.Truncated.HomotopicL.homotopicR {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} (h : HomotopicL f g) : HomotopicR f g

In a 2-truncated quasicategory, left homotopy implies right homotopy.

theorem SSet.Truncated.HomotopicR.homotopicL {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} (h : HomotopicR f g) : HomotopicL f g

In a 2-truncated quasicategory, right homotopy implies left homotopy.

theorem SSet.Truncated.homotopicL_iff_homotopicR {X : Truncated 2} [X.Quasicategory₂] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} : HomotopicL f g ↔ HomotopicR f g

In a 2-truncated quasicategory, the right and left homotopy relations coincide.

theorem SSet.Truncated.Edge.CompStruct.comp_unique {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f f' : Edge x y} {g g' : Edge y z} {h h' : Edge x z} (s : f.CompStruct g h) (s' : f'.CompStruct g' h') (hf : HomotopicL f f') (hg : HomotopicL g g') : HomotopicL h h'

Given CompStruct f g h and CompStruct f' g' h' with the same vertices and edges such that f ≃ f' and g ≃ g', then the long diagonal edges h and h' are also homotopic.

noncomputable def SSet.Truncated.Edge.comp {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} (f : Edge x y) (g : Edge y z) : Edge x z

Given two consecutive edges f, g in a 2-truncated quasicategory, nonconstructively choose an edge that is the diagonal of a 2-simplex with spine given by f and g. The CompStruct witnessing this property is given by Edge.composeStruct.

noncomputable def SSet.Truncated.Edge.compStruct {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} (f : Edge x y) (g : Edge y z) : f.CompStruct g (f.comp g)

See Edge.comp

structure SSet.Truncated.HomotopyCategory₂ (A : Truncated 2) : Type u_1

The homotopy category of a 2-truncated quasicategory A has as objects the vertices of A

• pt : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })

  An object of the homotopy category is a vertex of A.

instance SSet.Truncated.instSetoidEdge {A : Truncated 2} [A.Quasicategory₂] (x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })) : Setoid (Edge x y)

Left homotopy is an equivalence relation on the edges of A. Remark: We could have equivalently chosen right homotopy, as shown by homotopicL_iff_homotopicR.

def SSet.Truncated.HomotopyCategory₂.Hom {A : Truncated 2} [A.Quasicategory₂] (x y : A.HomotopyCategory₂) : Type u_1

The morphisms between two vertices x, y in HomotopyCategory₂ A are homotopy classes of edges between x and y.

noncomputable instance SSet.Truncated.HomotopyCategory₂.instCategoryStruct {A : Truncated 2} [A.Quasicategory₂] : CategoryTheory.CategoryStruct.{u_1, u_1} A.HomotopyCategory₂

Composition of morphisms in HomotopyCategory₂ A is given by lifting the edge chosen by composeEdges.

theorem SSet.Truncated.HomotopyCategory₂.mk_surjective {A : Truncated 2} : Function.Surjective mk

The function HomotopyCategory₂.mk taking a vertex of A and sending it to the corresponding object of HomotopyCategory₂ A is surjective.

def SSet.Truncated.HomotopyCategory₂.homMk {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} (f : Edge x y) : { pt := x } ⟶ { pt := y }

Any edge in the 2-truncated simplicial set A defines a morphism in the homotopy category by taking its equivalence class.

theorem SSet.Truncated.HomotopyCategory₂.homMk_surjective {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} : Function.Surjective homMk

Every morphism in the homotopy category HomotopyCategory₂ A is the equivalence class of an edge of A.

@[simp]

theorem SSet.Truncated.HomotopyCategory₂.homMk_id {A : Truncated 2} [A.Quasicategory₂] (x : A.HomotopyCategory₂) : homMk (Edge.id x.pt) = CategoryTheory.CategoryStruct.id x

The trivial (degenerate) edge at a vertex x is a representative for the identity morphism x ⟶ x.

theorem SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} (h : HomotopicL f g) : HomotopyCategory₂.homMk f = HomotopyCategory₂.homMk g

Left homotopic edges represent the same morphism in the homotopy category.

theorem SSet.Truncated.HomotopicR.congr_homotopyCategory₂HomMk {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f g : Edge x y} (h : HomotopicR f g) : HomotopyCategory₂.homMk f = HomotopyCategory₂.homMk g

Right homotopic edges represent the same morphism in the homotopy category.

theorem SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f : Edge x y} {g : Edge y z} {h : Edge x z} (s : f.CompStruct g h) : CategoryTheory.CategoryStruct.comp (HomotopyCategory₂.homMk f) (HomotopyCategory₂.homMk g) = HomotopyCategory₂.homMk h

A CompStruct f g h is a witness for the fact that the morphisms represented by f and g compose to the morphism represented by h.

noncomputable def SSet.Truncated.Edge.CompStruct.ofHomotopyCategory₂Fac {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f : Edge x y} {g : Edge y z} {h : Edge x z} (fac : CategoryTheory.CategoryStruct.comp (HomotopyCategory₂.homMk f) (HomotopyCategory₂.homMk g) = HomotopyCategory₂.homMk h) : f.CompStruct g h

If we have a factorization homMk f ≫ homMk g = homMk h, this is the choice of a structure CompStruct f g h.

theorem SSet.Truncated.Edge.CompStruct.nonempty_iff {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Quasicategory₂._proof_1 })} {f : Edge x y} {g : Edge y z} {h : Edge x z} : Nonempty (f.CompStruct g h) ↔ CategoryTheory.CategoryStruct.comp (HomotopyCategory₂.homMk f) (HomotopyCategory₂.homMk g) = HomotopyCategory₂.homMk h

Given edges f, g and h of a 2-truncated quasicategory, there exists a structure CompStruct f g h iff homMk f ≫ homMk g = homMk h holds in the homotopy category.

noncomputable instance SSet.Truncated.instCategoryHomotopyCategory₂ {A : Truncated 2} [A.Quasicategory₂] : CategoryTheory.Category.{u_1, u_1} A.HomotopyCategory₂