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, for f a simplicial set morphism, is equal to f applied to that 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 between x₀ and x₁ along equalities xᵢ = yᵢ. I.e. constructs an edge between the yᵢ from an edge between the xᵢ.

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 between edges e₀₁, e₁₂ and e₀₂ along equalities on 1-simplices eᵢⱼ.edge = fᵢⱼ.edge. I.e. constructs a CompStruct between the fᵢⱼ from a CompStruct between the eᵢⱼ.

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

For hom an edge, IsIso hom encodes that there is a backward edge inv, and there are 2-simplices witnessing that hom and inv compose to the identity on their endpoints. This means that hom becomes 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 on a point, composed with itself, gives the identity.

Equations

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

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 a proof of isomorphism for hom along an equality of 1-simplices hom = hom'. I.e. shows that hom' is an isomorphism from an isomorphism proof of hom.

Equations

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