Composition of edges in quasicategories

In this file, we define the notions of left and right homotopies on edges of simplicial sets, and we show that if X is a quasicategory, then edges can be composed (see SSet.Edge.comp and SSet.Edge.compStruct) and that this composition satisfies some form of associativity. The results are deduced from similar results for 2-truncated quasicategories.

@[reducible, inline]

abbrev SSet.Edge.HomotopyL {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e e' : Edge x₀ x₁) : Type u

A left homotopy between two edges e and e' is a CompStruct e (id _) e'.

Equations

• e.HomotopyL e' = e.CompStruct (SSet.Edge.id x₁) e'

@[reducible, inline]

abbrev SSet.Edge.HomotopyR {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e e' : Edge x₀ x₁) : Type u

A right homotopy between two edges e and e' is a CompStruct (id _) e e'.

Equations

• e.HomotopyR e' = (SSet.Edge.id x₀).CompStruct e e'

noncomputable def SSet.Edge.comp {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} [X.Quasicategory] (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) : Edge x₀ x₂

The composition of two edges in a quasicategory.

Equations

• e₀₁.comp e₁₂ = SSet.Truncated.Edge.comp e₀₁ e₁₂

noncomputable def SSet.Edge.compStruct {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} [X.Quasicategory] (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) : e₀₁.CompStruct e₁₂ (e₀₁.comp e₁₂)

If e₀₁ : Edge x₀ x₁ and e₁₂ : Edge x₁ x₂ are edges in a quasicategory, this is a structure exhibiting the fact that e₀₁.comp e₁₂ is a composition of e₀₁ and e₁₂.

Equations

• e₀₁.compStruct e₁₂ = SSet.Truncated.Edge.compStruct e₀₁ e₁₂

noncomputable def SSet.Edge.assoc {X : SSet} [X.Quasicategory] {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (h₀₂ : e₀₁.CompStruct e₁₂ e₀₂) (h₁₃ : e₁₂.CompStruct e₂₃ e₁₃) (h : e₀₁.CompStruct e₁₃ e₀₃) : e₀₂.CompStruct e₂₃ e₀₃

The associativity of the composition of edges in a quasicategory.

Equations

• SSet.Edge.assoc h₀₂ h₁₃ h = SSet.Truncated.Edge.assoc h₀₂ h₁₃ h

noncomputable def SSet.Edge.assoc' {X : SSet} [X.Quasicategory] {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (h₀₂ : e₀₁.CompStruct e₁₂ e₀₂) (h₁₃ : e₁₂.CompStruct e₂₃ e₁₃) (h : e₀₂.CompStruct e₂₃ e₀₃) : e₀₁.CompStruct e₁₃ e₀₃

The associativity of the composition of edges in a quasicategory.

Equations

• SSet.Edge.assoc' h₀₂ h₁₃ h = SSet.Truncated.Edge.assoc' h₀₂ h₁₃ h

noncomputable def SSet.Edge.HomotopyL.homotopyR {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} [X.Quasicategory] {e e' : Edge x₀ x₁} (h : e.HomotopyL e') : e.HomotopyR e'

In a quasicategory, two left homotopic edges are also right homotopic.

Equations

• h.homotopyR = SSet.Edge.assoc' (SSet.Edge.CompStruct.idComp e) (SSet.Edge.CompStruct.compId e) h

noncomputable def SSet.Edge.HomotopyR.homotopyL {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} [X.Quasicategory] {e e' : Edge x₀ x₁} (h : e.HomotopyR e') : e.HomotopyL e'

In a quasicategory, two right homotopic edges are also left homotopic.

Equations

• h.homotopyL = SSet.Edge.assoc (SSet.Edge.CompStruct.idComp e) (SSet.Edge.CompStruct.compId e) h

noncomputable def SSet.Edge.CompStruct.unique {X : SSet} [X.Quasicategory] {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) {e₀₁' : Edge x₀ x₁} {e₁₂' : Edge x₁ x₂} {e₀₂' : Edge x₀ x₂} (h' : e₀₁'.CompStruct e₁₂' e₀₂') (h₀₁ : e₀₁.HomotopyL e₀₁') (h₁₂ : e₁₂.HomotopyL e₁₂') : e₀₂.HomotopyL e₀₂'

If we have structures CompStruct e₀₁ e₁₂ e₀₂ and CompStruct e₀₁' e₁₂' e₀₂' involving edges in a quasicategory, e₀₁ and e₀₁' are left homotopic and e₁₂ and e₁₂' are left homotopic, then e₀₂ and e₀₂' are left homotopic.

Equations

• h.unique h' h₀₁ h₁₂ = SSet.Truncated.Edge.CompStruct.unique h h' h₀₁ h₁₂

noncomputable def SSet.Edge.CompStruct.unique' {X : SSet} [X.Quasicategory] {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) {e₀₂' : Edge x₀ x₂} (h' : e₀₂.HomotopyL e₀₂') : e₀₁.CompStruct e₁₂ e₀₂'

If we have a structure CompStruct e₀₁ e₁₂ e₀₂ and e₀₂ is left homotopic to e₀₂', then there is a CompStruct e₀₁ e₁₂ e₀₂' structure.

Equations

• h.unique' h' = SSet.Edge.assoc' h (SSet.Edge.CompStruct.compId e₁₂) h'