Edges and "triangles" in truncated simplicial sets

Given a 2-truncated simplicial set X, we introduce two types:

• Given 0-simplices x₀ and x₁, we define Edge x₀ x₁ which is the type of 1-simplices with faces x₁ and x₀ respectively;
• Given 0-simplices x₀, x₁, x₂, edges e₀₁ : Edge x₀ x₁, e₁₂ : Edge x₁ x₂, e₀₂ : Edge x₀ x₂, a structure CompStruct e₀₁ e₁₂ e₀₂ which records the data of a 2-simplex with faces e₁₂, e₀₂ and e₀₁ respectively. This data will allow to obtain relations in the homotopy category of X.

structure SSet.Truncated.Edge {X : Truncated 2} (x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })) : Type u

In a 2-truncated simplicial set, an edge from a vertex x₀ to x₁ is a 1-simplex with prescribed 0-dimensional faces.

• edge : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_2 })

  A 1-simplex

• src_eq : X.map (SimplexCategory.Truncated.δ₂ 1 _proof_1 _proof_3).op self.edge = x₀

  The source of the edge is x₀.

• tgt_eq : X.map (SimplexCategory.Truncated.δ₂ 0 _proof_1 _proof_3).op self.edge = x₁

  The target of the edge is x₁.

theorem SSet.Truncated.Edge.ext_iff {X : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} {x y : Edge x₀ x₁} : x = y ↔ x.edge = y.edge

theorem SSet.Truncated.Edge.ext {X : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} {x y : Edge x₀ x₁} (edge : x.edge = y.edge) : x = y

def SSet.Truncated.Edge.mk' {X : Truncated 2} (s : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_2 })) : Edge (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_1 _proof_3).op s) (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_1 _proof_3).op s)

The edge given by a 1-simplex.

@[simp]

theorem SSet.Truncated.Edge.mk'_edge {X : Truncated 2} (s : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_2 })) : (mk' s).edge = s

theorem SSet.Truncated.Edge.exists_of_simplex {X : Truncated 2} (s : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_2 })) : ∃ (x₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })) (x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })) (e : Edge x₀ x₁), e.edge = s

def SSet.Truncated.Edge.id {X : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })) : Edge x x

The constant edge on a 0-simplex.

@[simp]

theorem SSet.Truncated.Edge.id_edge {X : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })) : (id x).edge = X.map (SimplexCategory.Truncated.σ₂ 0 _proof_3 _proof_1).op x

def SSet.Truncated.Edge.map {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} (e : Edge x₀ x₁) (f : X ⟶ Y) : Edge (f.app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 }) x₀) (f.app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 }) x₁)

The image of an edge by a morphism of truncated simplicial sets.

@[simp]

theorem SSet.Truncated.Edge.map_edge {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} (e : Edge x₀ x₁) (f : X ⟶ Y) : (e.map f).edge = f.app (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_2 }) e.edge

@[simp]

theorem SSet.Truncated.Edge.map_id {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })) (f : X ⟶ Y) : (id x).map f = id (f.app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 }) x)

instance SSet.Truncated.Edge.instSubsingleton {X : Truncated 2} [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_2 }))] {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} : Subsingleton (Edge x y)

structure SSet.Truncated.Edge.CompStruct {X : Truncated 2} {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₂) : Type u

Let x₀, x₁, x₂ be 0-simplices of a 2-truncated simplicial set X, e₀₁ an edge from x₀ to x₁, e₁₂ an edge from x₁ to x₂, e₀₂ an edge from x₀ to x₂. This is the data of a 2-simplex whose faces are respectively e₀₂, e₁₂ and e₀₁. Such structures shall provide relations in the homotopy category of arbitrary (truncated) simplicial sets (and specialized constructions for quasicategories and Kan complexes.).

• simplex : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_1 })

  A 2-simplex with prescribed 1-dimensional faces

• d₂ : X.map (SimplexCategory.Truncated.δ₂ 2 Edge._proof_2 _proof_2).op self.simplex = e₀₁.edge
• d₀ : X.map (SimplexCategory.Truncated.δ₂ 0 Edge._proof_2 _proof_2).op self.simplex = e₁₂.edge
• d₁ : X.map (SimplexCategory.Truncated.δ₂ 1 Edge._proof_2 _proof_2).op self.simplex = e₀₂.edge

theorem SSet.Truncated.Edge.CompStruct.ext_iff {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} {x y : e₀₁.CompStruct e₁₂ e₀₂} : x = y ↔ x.simplex = y.simplex

theorem SSet.Truncated.Edge.CompStruct.ext {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} {x y : e₀₁.CompStruct e₁₂ e₀₂} (simplex : x.simplex = y.simplex) : x = y

theorem SSet.Truncated.Edge.CompStruct.exists_of_simplex {X : Truncated 2} (s : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_1 })) : ∃ (x₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })) (x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })) (x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })) (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) (h : e₀₁.CompStruct e₁₂ e₀₂), h.simplex = s

def SSet.Truncated.Edge.CompStruct.idComp {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })} (e : Edge x y) : (id x).CompStruct e e

e : Edge x y is a composition of Edge.id x with e.

def SSet.Truncated.Edge.CompStruct.compId {X : Truncated 2} {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })} (e : Edge x y) : e.CompStruct (id y) e

e : Edge x y is a composition of e with Edge.id y.

def SSet.Truncated.Edge.CompStruct.idCompId {X : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })) : (id x).CompStruct (id x) (id x)

Edge.id x is a composition of Edge.id x with Edge.id x.

@[simp]

theorem SSet.Truncated.Edge.CompStruct.idCompId_simplex {X : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })) : (idCompId x).simplex = X.map (SimplexCategory.Truncated.σ₂ 0 _proof_2 Edge._proof_2).op (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_3 Edge._proof_1).op x)

def SSet.Truncated.Edge.CompStruct.map {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) (f : X ⟶ Y) : (e₀₁.map f).CompStruct (e₁₂.map f) (e₀₂.map f)

The image of a Edge.CompStruct by a morphism of 2-truncated simplicial sets.

@[simp]

theorem SSet.Truncated.Edge.CompStruct.map_simplex {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) (f : X ⟶ Y) : (h.map f).simplex = f.app (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_1 }) h.simplex