Asphericity from a three-manifold hierarchy (source code)

= Asphericity from a three-manifold hierarchy

In an <orientable> <irreducible three-manifold>, an incompressible cut is <fundamental group>-injective by the <Loop theorem>. Lift a <three-manifold hierarchy> to the <universal cover>. The terminal ball pieces are <contractible> and their gluing <surfaces> have <contractible> universal covers. The incidence graph is a tree, by the <van Kampen theorem> normal form for successive cuts. Finite subtrees are <contractible> by successively attaching a terminal piece along a <contractible> intersection. Every <sphere> map has <compact> image contained in a finite subtree, so all higher <homotopy groups> of the <universal cover> vanish.