Edges and "triangles" in simplicial sets

Given a 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.

(This API parallels similar definitions for 2-truncated simplicial sets. The definitions in this file are definitionally equal to their 2-truncated counterparts.)

def SSet.Edge {X : SSet} (x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))) : Type u

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

def SSet.Edge.ofTruncated {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Truncated.Edge x₀ x₁) : Edge x₀ x₁

Constructor for SSet.Edge which takes as an input a term in the definitionally equal type SSet.Truncated.Edge for the 2-truncation of the simplicial set. (This definition is made to contain abuse of defeq in other definitions.)

def SSet.Edge.toTruncated {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : Truncated.Edge x₀ x₁

The edge of the 2-truncation of a simplicial set X that is induced by an edge of X.

def SSet.Edge.edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : X.obj (Opposite.op (SimplexCategory.mk 1))

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

@[simp]

theorem SSet.Edge.ofTruncated_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Truncated.Edge x₀ x₁) : (ofTruncated e).edge = e.edge

@[simp]

theorem SSet.Edge.toTruncated_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : e.toTruncated.edge = e.edge

@[simp]

theorem SSet.Edge.src_eq {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : CategoryTheory.SimplicialObject.δ X 1 e.edge = x₀

@[simp]

theorem SSet.Edge.tgt_eq {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : CategoryTheory.SimplicialObject.δ X 0 e.edge = x₁

theorem SSet.Edge.ext {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e e' : Edge x₀ x₁} (h : e.edge = e'.edge) : e = e'

theorem SSet.Edge.ext_iff {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e e' : Edge x₀ x₁} : e = e' ↔ e.edge = e'.edge

def SSet.Edge.mk {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (edge : X.obj (Opposite.op (SimplexCategory.mk 1))) (src_eq : CategoryTheory.SimplicialObject.δ X 1 edge = x₀ := by cat_disch) (tgt_eq : CategoryTheory.SimplicialObject.δ X 0 edge = x₁ := by cat_disch) : Edge x₀ x₁

Constructor for edges in a simplicial set.

@[simp]

theorem SSet.Edge.mk_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (edge : X.obj (Opposite.op (SimplexCategory.mk 1))) (src_eq : CategoryTheory.SimplicialObject.δ X 1 edge = x₀ := by cat_disch) (tgt_eq : CategoryTheory.SimplicialObject.δ X 0 edge = x₁ := by cat_disch) : (mk edge src_eq tgt_eq).edge = edge

def SSet.Edge.id {X : SSet} (x₀ : X.obj (Opposite.op (SimplexCategory.mk 0))) : Edge x₀ x₀

The constant edge on a 0-simplex.

@[simp]

theorem SSet.Edge.toTruncated_id {X : SSet} (x₀ : X.obj (Opposite.op (SimplexCategory.mk 0))) : (id x₀).toTruncated = Truncated.Edge.id x₀

@[simp]

theorem SSet.Edge.id_edge {X : SSet} (x₀ : X.obj (Opposite.op (SimplexCategory.mk 0))) : (id x₀).edge = CategoryTheory.SimplicialObject.σ X 0 x₀

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

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

@[simp]

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

@[simp]

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

def SSet.Edge.mk' {X : SSet} (s : X.obj (Opposite.op (SimplexCategory.mk 1))) : Edge (CategoryTheory.SimplicialObject.δ X 1 s) (CategoryTheory.SimplicialObject.δ X 0 s)

The edge given by a 1-simplex.

@[simp]

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

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

def SSet.Edge.CompStruct {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) : Type u

Let x₀, x₁, x₂ be 0-simplices of a 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 simplicial sets (and specialized constructions for quasicategories and Kan complexes.).

def SSet.Edge.CompStruct.ofTruncated {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.toTruncated.CompStruct e₁₂.toTruncated e₀₂.toTruncated) : e₀₁.CompStruct e₁₂ e₀₂

Constructor for SSet.Edge.CompStruct which takes as an input a term in the definitionally equal type SSet.Truncated.Edge.CompStruct for the 2-truncation of the simplicial set. (This definition is made to contain abuse of defeq in other definitions.)

def SSet.Edge.CompStruct.toTruncated {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : e₀₁.toTruncated.CompStruct e₁₂.toTruncated e₀₂.toTruncated

Conversion from SSet.Edge.CompStruct to SSet.Truncated.Edge.CompStruct.

def SSet.Edge.CompStruct.simplex {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : X.obj (Opposite.op (SimplexCategory.mk 2))

The underlying 2-simplex in a structure SSet.Edge.CompStruct.

@[simp]

theorem SSet.Edge.CompStruct.d₂ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.SimplicialObject.δ X 2 h.simplex = e₀₁.edge

@[simp]

theorem SSet.Edge.CompStruct.d₀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.SimplicialObject.δ X 0 h.simplex = e₁₂.edge

@[simp]

theorem SSet.Edge.CompStruct.d₁ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.SimplicialObject.δ X 1 h.simplex = e₀₂.edge

def SSet.Edge.CompStruct.mk {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (simplex : X.obj (Opposite.op (SimplexCategory.mk 2))) (d₂ : CategoryTheory.SimplicialObject.δ X 2 simplex = e₀₁.edge := by cat_disch) (d₀ : CategoryTheory.SimplicialObject.δ X 0 simplex = e₁₂.edge := by cat_disch) (d₁ : CategoryTheory.SimplicialObject.δ X 1 simplex = e₀₂.edge := by cat_disch) : e₀₁.CompStruct e₁₂ e₀₂

Constructor for SSet.Edge.CompStruct.

@[simp]

theorem SSet.Edge.CompStruct.mk_simplex {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (simplex : X.obj (Opposite.op (SimplexCategory.mk 2))) (d₂ : CategoryTheory.SimplicialObject.δ X 2 simplex = e₀₁.edge := by cat_disch) (d₀ : CategoryTheory.SimplicialObject.δ X 0 simplex = e₁₂.edge := by cat_disch) (d₁ : CategoryTheory.SimplicialObject.δ X 1 simplex = e₀₂.edge := by cat_disch) : (mk simplex ⋯ ⋯ ⋯).simplex = simplex

theorem SSet.Edge.CompStruct.ext {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} {h h' : e₀₁.CompStruct e₁₂ e₀₂} (eq : h.simplex = h'.simplex) : h = h'

theorem SSet.Edge.CompStruct.ext_iff {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} {h h' : e₀₁.CompStruct e₁₂ e₀₂} : h = h' ↔ h.simplex = h'.simplex

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

def SSet.Edge.CompStruct.idComp {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : (id x₀).CompStruct e e

e : Edge x₀ x₁ is a composition of Edge.id x₀ with e.

@[simp]

theorem SSet.Edge.CompStruct.idComp_simplex {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : (idComp e).simplex = CategoryTheory.SimplicialObject.σ X 0 e.edge

def SSet.Edge.CompStruct.compId {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : e.CompStruct (id x₁) e

e : Edge x₀ x₁ is a composition of e with Edge.id x₁

@[simp]

theorem SSet.Edge.CompStruct.compId_simplex {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (e : Edge x₀ x₁) : (compId e).simplex = CategoryTheory.SimplicialObject.σ X 1 e.edge

def SSet.Edge.CompStruct.map {X Y : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op (SimplexCategory.mk 0))} {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 simplicial sets.

@[simp]

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