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

The 1-simplex of e.map f is f applied to the edge.

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

Transports an edge along equalities on vertices.

Equations

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

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₂} (c : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.SimplicialObject.δ X 2 c.simplex = e₀₁.edge

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₂} (c : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.SimplicialObject.δ X 0 c.simplex = e₁₂.edge

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₂} (c : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.SimplicialObject.δ X 1 c.simplex = e₀₂.edge

def SSet.Edge.CompStruct.ofEq {X : SSet} {x₀ x₁ x₂ y₀ y₁ y₂ : X.obj (Opposite.op (SimplexCategory.mk 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 along equalities on 1-simplices.

Equations

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

structure SSet.Edge.IsIso {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} (hom : Edge x₀ x₁) : Type u_1

IsIso hom encodes that hom has an inverse edge with 2-simplices witnessing composition to identity edges, making hom an isomorphism in the homotopy category.

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

theorem SSet.Edge.IsIso.id_comp_id_aux {X : SSet} {l m n : ℕ} {f : SimplexCategory.mk n ⟶ SimplexCategory.mk m} {g : SimplexCategory.mk m ⟶ SimplexCategory.mk l} {h : SimplexCategory.mk n ⟶ SimplexCategory.mk l} (x : X.obj (Opposite.op (SimplexCategory.mk l))) (e : CategoryTheory.CategoryStruct.comp f g = h) : X.map f.op (X.map g.op x) = X.map h.op x

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

The identity edge composed with itself gives the identity.

Equations

• SSet.Edge.IsIso.idCompId x = SSet.Edge.CompStruct.idComp (SSet.Edge.id x)

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

The identity edge is an isomorphism.

Equations

• SSet.Edge.IsIso.isIsoId x = { inv := SSet.Edge.id x, homInvId := SSet.Edge.IsIso.idCompId x, invHomId := SSet.Edge.IsIso.idCompId x }

def SSet.Edge.IsIso.isIsoInv {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} {hom : Edge x₀ x₁} (I : hom.IsIso) : I.inv.IsIso

The inverse of an isomorphism is an isomorphism.

Equations

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

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

The image of an isomorphism under an SSet morphism is an isomorphism.

Equations

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

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

Transports an isomorphism proof along an equality of 1-simplices.

Equations

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