Theorems · Inductive type · algebraic topology

SSet.Edge.InvStruct

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

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Cited by

14 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound