Edge-loop group (source code)

= Edge-loop group
{title2=$E(K,b)$}

Two based <edge loops> are equivalent under insertion or deletion of stationary steps, cancellation or insertion of a backtracking spur, and replacement of two sides of a triangle by its third side. The <edge-loop group> consists of the resulting classes, with concatenation as product and reversal as inverse. Each elementary move can be performed inside a longer concatenation, so multiplication is well defined. Associativity follows from concatenation, the stationary loop is the identity, and a loop followed by its reversal cancels by spurs.

Realization induces a homomorphism to the <fundamental group> of the geometric realization, because each move is a homotopy in an edge or a triangle. The relative <Simplicial approximation theorem> applied to based circles makes this map surjective. The full edge-path theorem additionally proves injectivity by approximating homotopies; that stronger assertion is not needed for the group construction or the surjectivity argument.