Edges, "triangles" and isos 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.)

Given 0-simplices x₀ and x₁, and an edge hom : Edge x₀ x₁, InvStruct hom records the data of an edge inv : Edge x₁ x₀ and simplices homInvId : CompStruct hom inv (id x₀) and invHomId : CompStruct inv hom (id x₁), witnessing that inv is an inverse to hom.

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

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

Equations

• SSet.Edge x₀ x₁ = SSet.Truncated.Edge x₀ x₁

def SSet.Edge.ofTruncated {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 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.)

Equations

• SSet.Edge.ofTruncated e = e

def SSet.Edge.toTruncated {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 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.

Equations

• e.toTruncated = e

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

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

Equations

• e.edge = e.toTruncated.edge

@[simp]

theorem SSet.Edge.ofTruncated_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 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 { len := 0 })} (e : Edge x₀ x₁) : e.toTruncated.edge = e.edge

@[simp]

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

@[simp]

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

theorem SSet.Edge.ext {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 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 { len := 0 })} {e e' : Edge x₀ x₁} : e = e' ↔ e.edge = e'.edge

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

Constructor for edges in a simplicial set.

Equations

• SSet.Edge.mk edge src_eq tgt_eq = SSet.Edge.ofTruncated { edge := edge, src_eq := ⋯, tgt_eq := ⋯ }

@[simp]

theorem SSet.Edge.mk_edge {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (edge : X.obj (Opposite.op { len := 1 })) (src_eq : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) edge = x₀ := by cat_disch) (tgt_eq : (CategoryTheory.ConcreteCategory.hom (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 { len := 0 })) : Edge x₀ x₀

The constant edge on a 0-simplex.

Equations

• SSet.Edge.id x₀ = SSet.Edge.ofTruncated (SSet.Truncated.Edge.id x₀)

@[simp]

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

@[simp]

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

def SSet.Edge.map {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : Edge x₀ x₁) (f : X ⟶ Y) : Edge ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₀) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₁)

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

Equations

• e.map f = SSet.Edge.ofTruncated (e.toTruncated.map ((SSet.truncation 2).map f))

@[simp]

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

@[simp]

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

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

The edge given by a 1-simplex.

Equations

• SSet.Edge.mk' s = SSet.Edge.mk s ⋯ ⋯

@[simp]

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

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

def SSet.Edge.ofEq {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} (e : Edge x₀ x₁) (h₀ : x₀ = y₀) (h₁ : x₁ = y₁) : Edge y₀ y₁

Transports an edge between x₀ and x₁ to an edge between y₀ and y₁, given x₀ = y₀ and x₁ = y₁.

Equations

• e.ofEq h₀ h₁ = { edge := e.edge, src_eq := ⋯, tgt_eq := ⋯ }

@[simp]

theorem SSet.Edge.ofEq_edge {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} (e : Edge x₀ x₁) (h₀ : x₀ = y₀) (h₁ : x₁ = y₁) : (e.ofEq h₀ h₁).edge = e.edge

def SSet.Edge.CompStruct {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 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.).

Equations

• e₀₁.CompStruct e₁₂ e₀₂ = e₀₁.toTruncated.CompStruct e₁₂.toTruncated e₀₂.toTruncated

def SSet.Edge.CompStruct.ofTruncated {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 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.)

Equations

• SSet.Edge.CompStruct.ofTruncated h = h

def SSet.Edge.CompStruct.toTruncated {X : SSet} {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₀₁.toTruncated.CompStruct e₁₂.toTruncated e₀₂.toTruncated

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

Equations

• h.toTruncated = h

def SSet.Edge.CompStruct.simplex {X : SSet} {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₀₂) : X.obj (Opposite.op { len := 2 })

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

Equations

• h.simplex = h.toTruncated.simplex

@[simp]

theorem SSet.Edge.CompStruct.d₂ {X : SSet} {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₀₂) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 2)) h.simplex = e₀₁.edge

@[simp]

theorem SSet.Edge.CompStruct.d₀ {X : SSet} {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₀₂) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) h.simplex = e₁₂.edge

@[simp]

theorem SSet.Edge.CompStruct.d₁ {X : SSet} {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₀₂) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) h.simplex = e₀₂.edge

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

Constructor for SSet.Edge.CompStruct.

Equations

• SSet.Edge.CompStruct.mk simplex d₂ d₀ d₁ = { simplex := simplex, d₂ := ⋯, d₀ := ⋯, d₁ := ⋯ }

@[simp]

theorem SSet.Edge.CompStruct.mk_simplex {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (simplex : X.obj (Opposite.op { len := 2 })) (d₂ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 2)) simplex = e₀₁.edge := by cat_disch) (d₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) simplex = e₁₂.edge := by cat_disch) (d₁ : (CategoryTheory.ConcreteCategory.hom (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 { len := 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 { len := 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 { len := 2 })) : ∃ (x₀ : X.obj (Opposite.op { len := 0 })) (x₁ : X.obj (Opposite.op { len := 0 })) (x₂ : X.obj (Opposite.op { len := 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 { len := 0 })} (e : Edge x₀ x₁) : (id x₀).CompStruct e e

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

Equations

• SSet.Edge.CompStruct.idComp e = SSet.Edge.CompStruct.ofTruncated (SSet.Truncated.Edge.CompStruct.idComp e.toTruncated)

@[simp]

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

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

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

Equations

• SSet.Edge.CompStruct.compId e = SSet.Edge.CompStruct.ofTruncated (SSet.Truncated.Edge.CompStruct.compId e.toTruncated)

@[simp]

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

def SSet.Edge.CompStruct.idCompId {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (id x).CompStruct (id x) (id x)

The identity edge on a point, composed with itself, gives the identity.

Equations

• SSet.Edge.CompStruct.idCompId x = SSet.Edge.CompStruct.ofTruncated (SSet.Truncated.Edge.CompStruct.idCompId x)

@[simp]

theorem SSet.Edge.CompStruct.idCompId_simplex {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (idCompId x).simplex = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 0)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 0)) x)

def SSet.Edge.CompStruct.map {X Y : SSet} {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₀₂) (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.

Equations

• h.map f = SSet.Edge.CompStruct.ofTruncated (h.toTruncated.map ((SSet.truncation 2).map f))

@[simp]

theorem SSet.Edge.CompStruct.map_simplex {X Y : SSet} {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₀₂) (f : X ⟶ Y) : (h.map f).simplex = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 2 }))) h.simplex

def SSet.Edge.CompStruct.ofEq {X : SSet} {x₀ x₁ x₂ y₀ y₁ y₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {f₀₁ : Edge y₀ y₁} {e₁₂ : Edge x₁ x₂} {f₁₂ : Edge y₁ y₂} {e₀₂ : Edge x₀ x₂} {f₀₂ : Edge y₀ y₂} (c : e₀₁.CompStruct e₁₂ e₀₂) (h₀₁ : e₀₁.edge = f₀₁.edge) (h₁₂ : e₁₂.edge = f₁₂.edge) (h₀₂ : e₀₂.edge = f₀₂.edge) : f₀₁.CompStruct f₁₂ f₀₂

Transports a CompStruct between edges e₀₁, e₁₂ and e₀₂ to a CompStruct between edges f₀₁, f₁₂ and f₀₂ along equalities of 1-simplices eᵢⱼ.edge = fᵢⱼ.edge.

Equations

• c.ofEq h₀₁ h₁₂ h₀₂ = { simplex := c.simplex, d₂ := ⋯, d₀ := ⋯, d₁ := ⋯ }

@[simp]

theorem SSet.Edge.CompStruct.ofEq_simplex {X : SSet} {x₀ x₁ x₂ y₀ y₁ y₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : Edge x₀ x₁} {f₀₁ : Edge y₀ y₁} {e₁₂ : Edge x₁ x₂} {f₁₂ : Edge y₁ y₂} {e₀₂ : Edge x₀ x₂} {f₀₂ : Edge y₀ y₂} (c : e₀₁.CompStruct e₁₂ e₀₂) (h₀₁ : e₀₁.edge = f₀₁.edge) (h₁₂ : e₁₂.edge = f₁₂.edge) (h₀₂ : e₀₂.edge = f₀₂.edge) : (c.ofEq h₀₁ h₁₂ h₀₂).simplex = c.simplex

structure SSet.Edge.InvStruct {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (hom : Edge x₀ x₁) : Type u

For an edge hom, InvStruct hom encodes the data of a backward edge inv, and 2-simplices witnessing that hom and inv compose to the identity on their endpoints. This implies that hom becomes an isomorphism in the homotopy category.

• inv : Edge x₁ x₀

  The backwards edge

• homInvId : hom.CompStruct self.inv (id x₀)

  The simplex witnessing that hom and inv compose to the identity

• invHomId : self.inv.CompStruct hom (id x₁)

  The simplex witnessing that inv and hom compose to the identity

theorem SSet.Edge.InvStruct.ext {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} {x y : hom.InvStruct} (inv : x.inv = y.inv) (homInvId : x.homInvId ≍ y.homInvId) (invHomId : x.invHomId ≍ y.invHomId) : x = y

theorem SSet.Edge.InvStruct.ext_iff {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} {x y : hom.InvStruct} : x = y ↔ x.inv = y.inv ∧ x.homInvId ≍ y.homInvId ∧ x.invHomId ≍ y.invHomId

def SSet.Edge.InvStruct.invStructId {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (id x).InvStruct

The identity edge has an inverse.

Equations

• SSet.Edge.InvStruct.invStructId x = { inv := SSet.Edge.id x, homInvId := SSet.Edge.CompStruct.idCompId x, invHomId := SSet.Edge.CompStruct.idCompId x }

@[simp]

theorem SSet.Edge.InvStruct.invStructId_inv {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (invStructId x).inv = id x

@[simp]

theorem SSet.Edge.InvStruct.invStructId_homInvId {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (invStructId x).homInvId = CompStruct.idCompId x

@[simp]

theorem SSet.Edge.InvStruct.invStructId_invHomId {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (invStructId x).invHomId = CompStruct.idCompId x

def SSet.Edge.InvStruct.invStructInv {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) : I.inv.InvStruct

The inverse has an inverse.

Equations

• I.invStructInv = { inv := hom, homInvId := I.invHomId, invHomId := I.homInvId }

@[simp]

theorem SSet.Edge.InvStruct.invStructInv_homInvId {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) : I.invStructInv.homInvId = I.invHomId

@[simp]

theorem SSet.Edge.InvStruct.invStructInv_inv {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) : I.invStructInv.inv = hom

@[simp]

theorem SSet.Edge.InvStruct.invStructInv_invHomId {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) : I.invStructInv.invHomId = I.homInvId

def SSet.Edge.InvStruct.map {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y) : (hom.map f).InvStruct

Maps an inverse along an morphism of simplicial sets.

Equations

• I.map f = { inv := I.inv.map f, homInvId := (I.homInvId.map f).ofEq ⋯ ⋯ ⋯, invHomId := (I.invHomId.map f).ofEq ⋯ ⋯ ⋯ }

@[simp]

theorem SSet.Edge.InvStruct.map_inv {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y) : (I.map f).inv = I.inv.map f

@[simp]

theorem SSet.Edge.InvStruct.map_homInvId {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y) : (I.map f).homInvId = (I.homInvId.map f).ofEq ⋯ ⋯ ⋯

@[simp]

theorem SSet.Edge.InvStruct.map_invHomId {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y) : (I.map f).invHomId = (I.invHomId.map f).ofEq ⋯ ⋯ ⋯

def SSet.Edge.InvStruct.ofEq {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} {hom' : Edge y₀ y₁} (I : hom.InvStruct) (hhom : hom.edge = hom'.edge) : hom'.InvStruct

Transports an inverse for hom along an equality of 1-simplices hom = hom'. I.e. constructs an inverse for hom' from an inverse for hom.

Equations

• I.ofEq hhom = { inv := I.inv.ofEq ⋯ ⋯, homInvId := I.homInvId.ofEq hhom ⋯ ⋯, invHomId := I.invHomId.ofEq ⋯ hhom ⋯ }

@[simp]

theorem SSet.Edge.InvStruct.ofEq_invHomId {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} {hom' : Edge y₀ y₁} (I : hom.InvStruct) (hhom : hom.edge = hom'.edge) : (I.ofEq hhom).invHomId = I.invHomId.ofEq ⋯ hhom ⋯

@[simp]

theorem SSet.Edge.InvStruct.ofEq_homInvId {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} {hom' : Edge y₀ y₁} (I : hom.InvStruct) (hhom : hom.edge = hom'.edge) : (I.ofEq hhom).homInvId = I.homInvId.ofEq hhom ⋯ ⋯

@[simp]

theorem SSet.Edge.InvStruct.ofEq_inv {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : Edge x₀ x₁} {hom' : Edge y₀ y₁} (I : hom.InvStruct) (hhom : hom.edge = hom'.edge) : (I.ofEq hhom).inv = I.inv.ofEq ⋯ ⋯