Presentation-complex support
These nodes turn Hatcher's proof of Corollary 1.28 into explicit interfaces for the project's pointed wedge, indexed cone attachment, and Mathlib's abstract CW-complex sequence.
Formalized foundations
Package the universal property of Hatcher.PointedWedge: a continuous map
from the wedge is equivalent to a target point together with continuous maps
from every summand that send its chosen basepoint to that target point.
Intended main artifact:
def Hatcher.PointedWedge.continuousMapEquiv
{ι : Type u} {X : ι → Type v} [∀ i, TopologicalSpace (X i)]
(x₀ : ∀ i, X i) {Y : Type w} [TopologicalSpace Y] :
C(Hatcher.PointedWedge X x₀, Y) ≃
Σ y₀ : Y, {f : ∀ i, C(X i, Y) // ∀ i, f i (x₀ i) = y₀}
Also expose a constructor desc, simp lemmas for the wedge point and each
inclusion, an extensionality theorem, and a homeomorphism constructor
Hatcher.PointedWedge.homeomorphCongr for basepoint-preserving families of
summand homeomorphisms. The construction must include the empty-index case.
Sources
For a family of path-connected spaces, equip Hatcher.PointedWedge with a
PathConnectedSpace instance. Map a path from each summand point to its
chosen basepoint through the canonical inclusion, then join arbitrary wedge
points through the common wedge point. The proof must also cover an empty
index type, for which this project's pointed wedge is a one-point space.
Intended main artifact:
instance Hatcher.PointedWedge.instPathConnectedSpace
{ι : Type u} {X : ι → Type v} [∀ i, TopologicalSpace (X i)]
(x₀ : ∀ i, X i) [∀ i, PathConnectedSpace (X i)] :
PathConnectedSpace (Hatcher.PointedWedge X x₀)
Dependencies
For a pointed topological space (X, x₀) and
g : FundamentalGroup X x₀, construct a continuous map from the boundary of
the standard two-disk to X, preserving the chosen basepoints and sending the
standard positively oriented boundary loop to g.
Intended main artifact:
noncomputable def Hatcher.diskBoundaryMapOfFundamentalGroup
{X : Type u} [TopologicalSpace X] {x₀ : X}
(g : FundamentalGroup X x₀) :
C(((TopCat.diskBoundary.{u} 2 : TopCat.{u}) : Type u), X)
The public API must include the basepoint simp lemma and:
theorem Hatcher.diskBoundaryMapOfFundamentalGroup_generator
(g : FundamentalGroup X x₀) :
FundamentalGroup.mapOfEq (diskBoundaryMapOfFundamentalGroup g)
(diskBoundaryMapOfFundamentalGroup_basepoint g)
(FundamentalGroup.fromPath (.mk diskBoundaryTwoLoop)) = g
A valid construction chooses a representative with Quotient.out, extends
its path to the unit interval, descends through AddCircle, and transports
along diskBoundaryTwoHomeomorphCircle.
Sources
Dependencies
Equip the unique map from the initial topological space to a point with one standard zero-cell attachment.
Intended artifact:
noncomputable def Hatcher.VanKampen.pointAttachCells :
HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell.{u} 0)
(CategoryTheory.Limits.initial.to (TopCat.of PUnit.{u + 1}))
The cell index must be definitionally PUnit, or accompanied by a specified
equivalence with PUnit. Identify TopCat.diskBoundary 0 with the empty
space and TopCat.disk 0 with a point, then transport the one-index cone
attachment through the resulting source and target isomorphisms.
Attach the cone on TopCat.diskBoundary 1 to a point by the unique map and
identify the resulting quotient with the circle, with the image of the point
corresponding to 1.
Intended artifact:
noncomputable def Hatcher.VanKampen.circleOneCellHomeomorph :
Hatcher.VanKampen.ConeAttachment
(fun _ : ((TopCat.diskBoundary.{u} 1 : TopCat.{u}) : Type u) =>
PUnit.unit) ≃ₜ ULift.{u} _root_.Circle
Also prove the simp lemma sending the cone-attachment basepoint to
ULift.up (1 : Circle). Use the standard homeomorphisms from the one-disk to
a closed interval, from the interval quotient to AddCircle, and from
AddCircle to Circle. The ULift is required by the standard-cell
universe.
For every dimension and topological space, equip the identity map with a
standard cell-attachment structure whose cell index is PEmpty.
Intended artifact:
noncomputable def Hatcher.VanKampen.CellAttachment.attachCellsId
(n : ℕ) (X : TopCat.{u}) :
HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell.{u} n) (𝟙 X)
Construct both indexed coproducts as initial objects and use the identity pushout square. The empty index must remain visible to the later dimension bound.
Package a natural-number sequence of standard cell attachments as a
TopCat.CWComplex whenever its initial stage is initial and its tail is
eventually constant.
Intended main artifact:
noncomputable def Hatcher.VanKampen.CellAttachment.cwComplexOfEventuallyConstantSequence
(X : ℕ → TopCat.{u}) (step : ∀ n, X n ⟶ X (n + 1))
(hX₀ : CategoryTheory.Limits.IsInitial (X 0)) (N : ℕ)
(hconst : (CategoryTheory.Functor.ofSequence step).IsEventuallyConstantFrom N)
(cells : ∀ n, HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell.{u} n) (step n)) :
TopCat.CWComplex (X N)
Also expose a helper deriving eventual constancy from isomorphism instances
on all steps after N, and a theorem saying that if each tail attachment has
empty cell index then every cell in the resulting CW structure has dimension
strictly less than N. The construction uses the eventual-constant cocone and
its colimit proof; it does not postulate a finite-sequence CW constructor.
Assembly chain
Equip the map from a point to the common basepoint of a wedge of circles with one standard one-cell for each circle.
Intended artifacts:
def Hatcher.wedgeCirclesBaseHom {ι : Type u} :
TopCat.of PUnit.{u + 1} ⟶
TopCat.of (Hatcher.PointedWedge
(fun _ : ι => _root_.Circle) (fun _ => (1 : _root_.Circle)))
noncomputable def Hatcher.wedgeCirclesAttachCells {ι : Type u} :
HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell.{u} 1)
(Hatcher.wedgeCirclesBaseHom (ι := ι))
The attachment's cell index must be definitionally ι, or accompanied by a
specified equivalence with ι; the construction must include the empty-index
case. Build the indexed cone attachment for constant maps to PUnit, identify
each quotient summand with the circle, use the pointed-wedge universal
property to assemble the homeomorphism, and transport the existing
AttachCells structure through the resulting arrow isomorphism.
For rels : Set (FreeGroup S), realize each relator as a based map from the
boundary of a two-disk into the pointed wedge of S circles, and package the
family as an indexed attachment by standard two-cells.
The public API must include a based continuous map
Hatcher.wedgeCircleRelatorAttachingMap r, an indexed family
Hatcher.presentationRelatorAttachingMap rels, the resulting space
Hatcher.presentationComplex rels and its basepoint, and:
noncomputable def Hatcher.presentationRelatorAttachCells
{S : Type u} (rels : Set (FreeGroup S)) :
HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell.{u} 2)
(Hatcher.presentationComplexBaseHom rels)
For every r : rels, prove that the corresponding attaching loop, transported
through Hatcher.fundamentalGroupEquivWedgeCircles, is exactly r.1. This
correctness theorem is the only representation detail the quotient
calculation may use.
Sources
Dependencies
Compute the fundamental group of the concrete presentation complex by the two-cell attachment theorem and transport the attaching normal closure through the free-group equivalence for the wedge of circles.
Intended main artifact:
noncomputable def Hatcher.presentationComplexFundamentalGroupEquiv
{S : Type u} (rels : Set (FreeGroup S)) :
PresentedGroup rels ≃*
FundamentalGroup (Hatcher.presentationComplex rels)
(Hatcher.presentationComplexBasepoint rels)
Prove explicitly that mapping the normal closure of the attaching loops along
Hatcher.fundamentalGroupEquivWedgeCircles gives
Subgroup.normalClosure rels, then use QuotientGroup.congr. The result must
include empty and infinite presentations and must not assume a finitely
generated or finitely presented group.
Sources
Equip the concrete presentation complex with Mathlib's abstract CW-complex structure by assembling its zero-, one-, and two-cell attachments and an empty constant tail.
Intended main artifact:
noncomputable def Hatcher.presentationComplexCWComplex
{S : Type u} (rels : Set (FreeGroup S)) :
TopCat.CWComplex (TopCat.of (Hatcher.presentationComplex rels))
Also expose the source-facing dimension bound:
theorem Hatcher.presentationComplexCWComplex_cells_dim_le_two
{S : Type u} (rels : Set (FreeGroup S))
(γ : HomotopicalAlgebra.RelativeCellComplex.Cells
(Hatcher.presentationComplexCWComplex rels)) :
γ.j ≤ 2
Use the sequence initial → point → wedge → presentationComplex, constant
from stage three onward. Its cell indices are one point in dimension zero,
S in dimension one, rels in dimension two, and empty in every higher
dimension. The empty tail, not an informal dimension convention, must prove
the bound.
Sources
Dependencies
The two final interfaces feed the completed source-facing presentation-complex realization. The formalized cyclic presentation complex is the concrete one-generator, one-relator example of the same attachment pattern. The exact implementation conventions are recorded in the project specification.
Additional formalization targets
For a generator type S and relators rels : Set (FreeGroup S), construct
the presentation complex with one vertex, one oriented 1-cell for each
generator, and one 2-cell for each relator. Prove that it is an abstract
two-dimensional CW complex and that its fundamental group is the corresponding
PresentedGroup.
Intended artifact:
Hatcher.exists_presentationComplex_fundamentalGroupEquiv.
The source-facing Lean statement should be equivalent to:
theorem exists_presentationComplex_fundamentalGroupEquiv
(S : Type u) (rels : Set (FreeGroup S)) :
∃ (X : TopCat.{u}) (x₀ : X) (c : TopCat.CWComplex X),
(∀ γ : HomotopicalAlgebra.RelativeCellComplex.Cells c, γ.j ≤ 2) ∧
Nonempty (PresentedGroup rels ≃* FundamentalGroup X x₀)
The construction uses the wedge of S circles as the 1-skeleton and attaches
one 2-cell along a loop representing each relator. The proof checks that these
are the only positive-dimensional cells; merely producing a space with the
required fundamental group would not establish Hatcher's two-dimensional
conclusion.
The supporting formalizations in presentation-complex support supply the wedge's one-cell attachment, based representatives for relators, the concrete two-cell attachment and group calculation, and the eventually constant CW sequence with its dimension bound. These interfaces avoid the unrelated unresolved bridge between Mathlib's classical and categorical CW APIs.
The arbitrary-group corollary composes this theorem's equivalence with
Hatcher.exists_presentedGroup_equiv.
Sources
Hatcher, Example 1.29 (page 52), group calculation only. For a positive
natural number n, attach a 2-cell to S¹ along the degree-n map. The
resulting presentation complex has fundamental group isomorphic to ℤ/nℤ.
Intended artifact: Hatcher.fundamentalGroupEquiv_cyclicPresentationComplex.
Define cyclicPresentationComplex n as the singleton indexed cone attachment
to Circle, using the boundary-of-the-two-disk homeomorphism followed by
Circle.degreeMap n as attaching map, and use the image of 1 as basepoint.
IndexedConeAttachment.attachCells_basicCell supplies the required abstract
2-cell attachment, so the generic attachment theorem and the cyclic quotient
calculation now complete the group computation.
The Lean artifact is defined for every n : ℕ. Its positive cases are exactly
Hatcher's example; at n = 0 the same construction yields the valid extension
with fundamental group ZMod 0 ≃+ ℤ.
The quotient calculation after the geometric step is already formalized in The degree-n circle relation gives the cyclic group.
This node does not claim the example's later geometric assertions identifying
the n = 2 case with ℝP² or excluding embeddings and surface structures for
higher n.