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 along equalities on vertices.

Equations

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

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 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 { len := 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 : { len := n } ⟶ { len := m }} {g : { len := m } ⟶ { len := l }} {h : { len := n } ⟶ { len := l }} (x : X.obj (Opposite.op { len := l })) (e : CategoryTheory.CategoryStruct.comp f g = h) : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) ((CategoryTheory.ConcreteCategory.hom (X.map g.op)) x) = (CategoryTheory.ConcreteCategory.hom (X.map h.op)) x

def SSet.Edge.IsIso.idCompId {X : SSet} (x : X.obj (Opposite.op { len := 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 { len := 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 { len := 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 { len := 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 { len := 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 ⋯ }