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 := ⋯ })) : 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 := ⋯ })

  A 1-simplex

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

  The source of the edge is x₀.

• tgt_eq : X.map (SimplexCategory.Truncated.δ₂ 0 ⋯ ⋯).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 := ⋯ })} {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 := ⋯ })} {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 := ⋯ })) : Edge (X.map (SimplexCategory.Truncated.δ₂ 1 ⋯ ⋯).op s) (X.map (SimplexCategory.Truncated.δ₂ 0 ⋯ ⋯).op s)

The edge given by a 1-simplex.

Equations

• SSet.Truncated.Edge.mk' s = { edge := s, src_eq := ⋯, tgt_eq := ⋯ }

@[simp]

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

theorem SSet.Truncated.Edge.exists_of_simplex {X : Truncated 2} (s : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })) : ∃ (x₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) (x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) (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 := ⋯ })) : Edge x x

The constant edge on a 0-simplex.

Equations

• SSet.Truncated.Edge.id x = { edge := X.map (SimplexCategory.Truncated.σ₂ 0 SSet.Truncated.Edge.mk'._proof_2 SSet.Truncated.Edge.mk'._proof_3).op x, src_eq := ⋯, tgt_eq := ⋯ }

@[simp]

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

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

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

Equations

• e.map f = { edge := f.app (Opposite.op { obj := SimplexCategory.mk 1, property := SSet.Truncated.Edge.mk'._proof_1 }) e.edge, src_eq := ⋯, tgt_eq := ⋯ }

@[simp]

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

@[simp]

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

structure SSet.Truncated.Edge.CompStruct {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (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 := ⋯ })

  A 2-simplex with prescribed 1-dimensional faces

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

theorem SSet.Truncated.Edge.CompStruct.ext {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {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.ext_iff {X : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {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.exists_of_simplex {X : Truncated 2} (s : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) : ∃ (x₀ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) (x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) (x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) (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 := ⋯ })} (e : Edge x y) : (id x).CompStruct e e

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def SSet.Truncated.Edge.CompStruct.map {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {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.

Equations

• h.map f = { simplex := f.app (Opposite.op { obj := SimplexCategory.mk 2, property := SSet.Truncated.Edge.CompStruct.map._proof_1 }) h.simplex, d₂ := ⋯, d₀ := ⋯, d₁ := ⋯ }

@[simp]

theorem SSet.Truncated.Edge.CompStruct.map_simplex {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {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 := map._proof_1 }) h.simplex