Algebraic Topology

Motivation

An integer winding label is discrete, but its exponential readout lies on a continuous circle. This mission makes that relationship exact. For a nonzero real algebraic angle $\alpha$, the map

$$n\longmapsto e^{i n\alpha}$$

is simultaneously a group character, a faithful encoding of $\mathbb Z$, and a countable dense orbit in the unit circle. Its complex values also form a linearly independent family over the algebraic complex numbers $\overline{\mathbb Q}$.

The result welds three previously completed interfaces. Circle covering theory produces canonical integer winding. Irrational-rotation theory classifies when an integer orbit is dense. Lindemann–Weierstrass gives the arithmetic rigidity that excludes resonance and algebraic linear relations. The point is not that topology alone proves transcendence, or that transcendence constructs winding: the theorem records the precise composition of the three layers.

The foundations are the completed private missions Winding Dynamics I, Lindemann–Weierstrass I, and Winding Arithmetic II. The transcendence layer is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.

Setting

Write $S^1\subset\mathbb C$ for the complex unit circle. For a real angle $\alpha$ and integer $n$, define

$$\operatorname{phase}_\alpha(n)=e^{i n\alpha}\in S^1.$$

This is an additive-to-multiplicative character: phase at $0$ is $1$, and phase at $m+n$ is the product of the phases at $m$ and $n$.

A based Circle loop $\gamma$ has a canonical integer $\operatorname{wind}(\gamma)$, obtained from the endpoint of its zero-based lift through the exponential cover. Its real phase readout is $\operatorname{phase}_\alpha(\operatorname{wind}(\gamma))$.

The orbit is dense when every nonempty open subset of $S^1$ contains some $\operatorname{phase}_\alpha(n)$. It is faithful when distinct integers have distinct phases. These properties are compatible: a countable subset may be dense without being all of the circle.

Formalization targets

Irrational rotation criterion

For every real $\alpha$,

$$\operatorname{DenseRange}(n\mapsto e^{i n\alpha}) \quad\Longleftrightarrow\quad \frac{\alpha}{2\pi}\notin\mathbb Q.$$

The proof identifies the phase orbit with integer multiples in $\mathbb R/(2\pi\mathbb Z)$ and transports Mathlib's irrational-rotation theorem through the standard homeomorphism with the complex unit circle.

Algebraic angles are nonresonant

If $\alpha\in\mathbb R$ is nonzero and algebraic over $\mathbb Q$, then $\alpha/(2\pi)$ is irrational. Otherwise $\pi$ would be algebraic, contradicting the proved transcendence of $\pi$. Consequently the real phase character has dense range.

Faithfulness and arithmetic rigidity

For the same nonzero algebraic $\alpha$, the character is injective and

$$\bigl(e^{i n\alpha}\bigr)_{n\in\mathbb Z}$$

is linearly independent over $\overline{\mathbb Q}$. The first conclusion says no two winding integers alias. The second says no nontrivial finite algebraic-coefficient linear relation exists among the phase values.

Actual Circle-loop consumer

For based Circle loops $\gamma$ and $\delta$,

$$e^{i\alpha\operatorname{wind}(\gamma)} =e^{i\alpha\operatorname{wind}(\delta)} \quad\Longleftrightarrow\quad \operatorname{wind}(\gamma)=\operatorname{wind}(\delta).$$

This consumes the canonical covering-space winding rather than an arbitrary externally supplied integer.

Resonance control

At the full-turn angle $\alpha=2\pi$, every integer phase is $1$, so the character is not injective. This negative control is outside the algebraic-angle regime because $\pi$ is transcendental. It records exactly why a nonresonance hypothesis is load-bearing.

Significance

The capstone exhibits one object with three complementary properties:

1. topological discreteness — values are indexed by integer winding;
2. dynamical density — the countable orbit visits every Circle neighborhood;
3. arithmetic rigidity — distinct values are faithful and linearly independent over $\overline{\mathbb Q}$.

This is a precise version of the intuitive claim that winding creates an integer coordinate whose phase representation explores a continuum. The continuum statement is density, not surjectivity: the image remains countable. The arithmetic statement is linear independence, not algebraic independence of the separate phase variables; the character law itself supplies multiplicative relations.

Together with Winding Arithmetic II, continuous homotopy preserves these readouts and a registered reset ledger factorizes their changes. This mission isolates the extra fact that the resulting character is both faithful and dense for every nonzero real algebraic angle.

Difficulty

No single layer implies the capstone by itself. The Circle exponential is periodic, so injectivity requires a genuine nonresonance argument. Density requires the exact normalization by $2\pi$ and transport through the AddCircle–Circle homeomorphism in both directions. Linear independence requires the completed Lindemann–Weierstrass theorem, not merely irrationality or transcendence of $\pi$.

The coercion bridge between the real Circle phase and the complex exponential character is also orientation-sensitive: the formal phase is exactly $\exp(i n\alpha)$. Reversing the sign would still define a dense faithful character, but it would not be the registered convention used by the prior winding arithmetic mission.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Circle density is stated only for real $\alpha$. The arithmetic conclusions require both IsAlgebraic ℚ α and $\alpha\ne0$.

The actual-loop theorem proves equality of phase values if and only if equality of canonical winding integers. It does not claim that the loops themselves are equal, and it does not add a new classification of homotopy classes. That classification remains the responsibility of the Circle covering-space layer.

The theorem proves a faithful representation of winding values, not the existence of winding in an arbitrary physical model. A Kuramoto, XY, or Lohe consumer must still provide a jointly continuous Circle field or a preserved non-simply-connected carrier and readout. No particle–wave or quantum-mechanical interpretation is asserted.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Lean mathematical library, Dense subgroups of the additive circle. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.html
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

Motivation

Winding number is a topological integer: continuous deformation preserves it, while crossing a branch cut or registering a reset can change it by an integer amount. Transcendence theory gives a different kind of rigidity. For a nonzero algebraic coupling $\alpha$, the phases $e^{i\alpha n}$ attached to distinct integers $n$ are linearly independent over the field $\overline{\mathbb Q}$ of algebraic complex numbers. This mission joins those statements at their exact formal interfaces.

The result is useful wherever a model first produces an integer winding label and then represents that label by a complex phase. Topology supplies the discrete coordinate, dynamics determines when it is conserved or reset, and Lindemann–Weierstrass supplies arithmetic distinguishability. None of those layers is asked to manufacture the others.

The foundation comes from three completed private missions: Winding Dynamics I: Homotopy Conservation and Reset Balance, Integer Winding Transcendence I: Exponential Phase Independence, and Lindemann–Weierstrass I: Exponential Independence. The transcendence proof is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.

Setting

Let $S^1$ be the complex unit circle. A based Circle loop is a continuous path in $S^1$ that starts and ends at $1$. Its canonical real lift through the exponential covering starts at $0$; the lift endpoint determines an integer $\operatorname{wind}(\gamma)$.

For $\beta\in\mathbb C$ and $n\in\mathbb Z$, define the integer exponential character

$$\chi_\beta(n)=\exp(n\beta).$$

The arithmetic consumer uses $\beta=i\alpha$, where $\alpha$ is nonzero and algebraic over $\mathbb Q$. Thus a loop $\gamma$ carries the phase $\chi_{i\alpha}(\operatorname{wind}(\gamma))$.

A closed Circle field is a jointly continuous map on the time/spatial square $I\times I$ whose two spatial endpoints agree at every time. Each spatial slice is normalized by its moving basepoint, producing a based loop. A carrier/readout segment generalizes this: an ambient trajectory remains in a registered carrier subspace and is observed through a continuous map from that carrier to $S^1$.

The discontinuous branch is represented separately by a finite reset ledger. It stores successive integer edge-turn cochains. Pairing those cochains with a certified closed edge cycle produces integer winding values and reset periods.

Formalization targets

Circle winding separates algebraic phases

For a family of loops $(\gamma_j)_{j\in J}$ with pairwise-distinct windings,

$$\left(e^{i\alpha\operatorname{wind}(\gamma_j)}\right)_{j\in J} \text{ is linearly independent over }\overline{\mathbb Q}.$$

Continuous evolution preserves the phase basis

If the initial windings of a family of closed Circle fields are distinct, then the initial phase family is linearly independent, every phase is unchanged between endpoint times, and the final phase family remains linearly independent. The same conclusion is exposed through the carrier/readout interface.

Reset balance becomes phase factorization

If a reset ledger has endpoint winding change $W_{\mathrm f}-W_{\mathrm i}$ and registered reset periods $\Delta W_j$, then

$$\chi_\beta(W_{\mathrm f}-W_{\mathrm i}) =\prod_j\chi_\beta(\Delta W_j).$$

This is the multiplicative image of the exact additive ledger balance.

The phase readout is faithful

For nonzero algebraic $\alpha$, the character $\chi_{i\alpha}$ is injective on $\mathbb Z$. Consequently, two actual Circle loops have equal algebraic phase readouts exactly when they have equal canonical winding. On the reset branch,

$$\prod_j\chi_{i\alpha}(\Delta W_j)=1 \quad\Longleftrightarrow\quad W_{\mathrm f}=W_{\mathrm i}.$$

Thus the multiplicative reset record detects zero net winding change without losing integer information.

Significance

The main theorem upgrades conservation of a single integer to conservation of an arithmetic basis. Distinct homotopy classes do not merely retain distinct integer labels: after the algebraic exponential readout, the corresponding phases admit no nontrivial finite linear relation with algebraic coefficients. This lets downstream consumers treat a family of winding sectors as a linearly independent family over $\overline{\mathbb Q}$.

The reset theorem provides the matching event law. Continuous evolution preserves the basis, whereas a registered reset multiplies phases according to the reset periods. The two branches share one character but retain different hypotheses, so a discontinuous ledger event is not misrepresented as a continuous homotopy.

The algebraic readout is also faithful: despite taking values on the complex exponential curve, it neither aliases two winding sectors nor hides a nonzero net reset behind total phase $1$ under the stated algebraic hypothesis.

This does not establish a particle–wave duality or a quantum-mechanical interpretation. It establishes a precise mathematical analogy: an integer topological label has a complex character representation whose distinct values enjoy a strong arithmetic independence theorem under an algebraic nonresonance condition.

Difficulty

The individual deductions are short only because three difficult interfaces have already been proved. Replacing an arbitrary integer map by actual Circle winding requires using the canonical covering lift rather than postulating labels. Preserving the phase basis requires transporting injectivity and linear independence through a jointly continuous moving-basepoint normalization. The reset branch requires respecting the sign convention and mapping a finite sum to a finite product, including the empty ledger.

Several tempting statements would be false. Duplicate winding labels cannot give a linearly independent family. The exponent $\alpha=0$ collapses every phase to $1$. Continuity of finitely many vertex phases does not by itself define a continuous spatial Circle field, and crossing the principal cut can change a discrete principal-turn winding. A global readout from a simply connected carrier such as all of $SU(2)$ cannot support nonzero loop winding without a separately registered non-simply-connected subcarrier or channel.

For a general complex coupling, exponential resonance can destroy injectivity. The nonzero algebraic hypothesis excludes that resonance here through the proved Lindemann--Weierstrass theorem; it is not merely a convenient side condition.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The Circle winding is the floor of the canonical zero-based lift endpoint divided by $2\pi$. Closed fields live on $I\times I$ and are normalized at spatial coordinate zero. The coupling $\alpha$ is an arbitrary complex algebraic number, not necessarily real, and must be nonzero.

The main carrier/readout theorem is conditional on an explicit continuous carrier-valued trajectory, closed spatial slices, and continuous Circle readout. It does not prove existence of a Kuramoto, XY, or Lohe solution, nor preservation of a particular carrier by such an ODE. Those are model-specific successors.

The reset factorization consumes the registered coherent ledger and certified closed cycle. It is an exact algebraic event law, not an energy estimate and not a claim that every physical trajectory realizes such a ledger. Its vertex and edge types retain the universe-zero scope of the existing reset interface.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

Motivation

Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a nontrivial homology class controls one of its distances. Determining how this distance behaves under a tensor product is therefore a basic structural question, not merely a parameter calculation.

Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an arbitrary finite binary chain complex and the other is the one-complex induced by a binary matrix. Their paper was published as “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). Its main distance result is Eq. (13) in the arXiv version: for this particular tensor factor, the usual product upper bound is always exact. The result extends the familiar two-complex setting of quantum hypergraph-product codes to the local structure occurring in complexes of any dimension.

Setting

A based binary chain complex consists of finite-dimensional vector spaces $A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and linear boundary maps

$$\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i \xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots$$

such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is $H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The homological distance is measured in the chosen basis:

$$d_i(\mathcal A)= \min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus \operatorname{im}\partial_{i+1}\}.$$

Following the paper, the minimum of an empty set is $\infty$. Thus $d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.

The endpoint convention is also the one stated explicitly after Eq. (1). For an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and $\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently

$$d_0(\mathcal A)=\min\{\operatorname{wt}(x): x\in A_0\setminus\operatorname{im}\partial_1\}$$

and

$$d_m(\mathcal A)=\min\{\operatorname{wt}(x): 0\ne x\in\ker\partial_m\}.$$

For an $r\times c$ binary matrix $P$, the one-complex $\mathcal K(P)$ has $\mathbb F_2^c$ in degree one, $\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are

$$d_1(\mathcal K(P))= \min\{\operatorname{wt}(x):Px=0,\ x\ne0\}$$

and

$$d_0(\mathcal K(P))= \min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.$$

In particular, $d_0=1$ unless $P$ has full row rank, in which case $d_0=\infty$. The degree-$j$ chain group of $\mathcal A\times\mathcal K(P)$ is

$$(A_j\otimes\mathbb F_2^r)\oplus (A_{j-1}\otimes\mathbb F_2^c),$$

with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign in that boundary has no effect.

Formalization targets

Tensor-product upper bound for arbitrary complexes

The first milestone is Eq. (11) for two arbitrary finite-length based binary chain complexes:

$$d_j(\mathcal A\times\mathcal B)\le \min_i d_i(\mathcal A)d_{j-i}(\mathcal B).$$

Rank-sensitive lower bound

Let $u=\operatorname{rank}P$ and $\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including both of its cases:

$$u<r\Longrightarrow d_j(\mathcal A\times\mathcal K(P))\ge \min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),$$

and

$$u=r\Longrightarrow d_j(\mathcal A\times\mathcal K(P))\ge d_{j-1}(\mathcal A)\delta.$$

Exact distance with a one-complex

The goal is Eq. (13):

$$d_j(\mathcal A\times\mathcal K(P))= \min\!\left( d_{j-1}(\mathcal A)d_1(\mathcal K(P)), d_j(\mathcal A)d_0(\mathcal K(P)) \right).$$

No full-rank hypothesis is imposed on $P$.

Significance

The equality determines the product distance exactly from four component distances. General tensor-product arguments immediately provide the upper bound, but an exact formula requires ruling out lower-weight homology classes that mix the two direct-sum blocks. Once established, the formula can be applied repeatedly to tensor products of one-complexes, which is the step used in the paper to obtain higher-dimensional quantum hypergraph-product code families and to compute their distances.

For formalization, the mission contributes reusable definitions of finite based binary chain data, homological distance valued in $\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant tensor-product boundary maps. Mathlib contains Hamming weight and general homological-algebra infrastructure, while QECLean contains a closely related based length-three homological-code interface. Neither the selected Mathlib environment nor the inspected QECLean development currently supplies this rank-sensitive exact distance theorem.

Difficulty

The central issue is that Hamming weight depends on the chosen bases and is not preserved by arbitrary homological isomorphisms. A Künneth isomorphism describes the product homology and readily produces low-weight representatives, which is enough for the upper bound, but it does not by itself exclude a still lighter representative obtained by cancellation between the two tensor blocks. The lower bound must also remain valid at the endpoints of the complex and in singular cases where one or more homology groups vanish and the relevant distance is $\infty$.

The theorem cannot be reduced to a dimension calculation. It must reason about supports and Hamming weights of based representatives while respecting the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$ and $\operatorname{rank}P=r$.

Formalization scope

The Lean development works over ZMod 2. A finite basis in degree $i$ is represented by Fin (dimension i), and a chain group is the function space from that coordinate type to ZMod 2. BasedBinaryChainComplex stores the dimension and boundary in every nonnegative degree, the chain condition, and a finite length above which all dimensions are zero. Thus the first milestone quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and $\mathcal B$, rather than over a local window or a one-complex specialization. If the stored length is $m$, the zero-dimensional source in degree $m+1$ makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the zero-dimensional target below degree zero makes $\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint cases in Eqs. (1) and (4) are represented directly.

Distances use WithTop ℕ. Their definitions are actual minima of Hamming weights of nontrivial representatives, with ⊤ produced by the empty-set case; infinite distance is not an extra hypothesis or a separately hard-coded branch. Coordinate types may be empty, which covers missing endpoint blocks. The binary matrix $P$ is represented as a linear map between two finite based function spaces. Its row and column coordinate types need not be nonempty, and no injectivity or surjectivity assumption is added.

The degree-$j$ product group is indexed by the disjoint union of all coordinate products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm is the sum of the weights of all tensor-degree blocks. The product boundary is the standard signed tensor boundary; its sign disappears over $\mathbb F_2$. A formal proof verifies that every pair of consecutive product boundaries composes to zero; the cancellation of the two mixed terms uses characteristic two. Thus the product distance is taken from an actual chain complex, rather than from unrelated adjacent linear maps. A basis-free tensor product or an abstract homology group alone is insufficient for the target, because either would discard the weight data on which the statement depends. The mission does not formalize the asymptotic code-family construction later in the paper, the transposed cohomological distance, or the CSS-code parameter translation. Those are natural downstream missions; they should reuse rather than alter the present based-chain definitions.

Selected references

• Weilei Zeng and Leonid P. Pryadko, “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). arXiv:1810.01519.
• Benjamin Audoux and Alain Couvreur, “On Tensor Products of CSS Codes,” arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
• Jean-Pierre Tillich and Gilles Zémor, “Quantum LDPC Codes With Positive Rate and Minimum Distance Proportional to the Square Root of the Blocklength,” IEEE Transactions on Information Theory 60 (2014), 1193--1202.

Motivation

The third mission in the series formalizing Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) turns to the second main topic of Chapter 1, covering spaces (Section 1.3, pp. 56–78). The first mission used the covering $\mathbb{R}\to S^1$ to compute $\pi_1(S^1)$, and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space $X$: the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of $\pi_1(X)$ (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the classification theorem (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of $X$ and subgroups of $\pi_1(X,x_0)$, together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).

All statements live in the Lean namespace Hatcher used by the earlier missions.

Setting

A covering space of $X$ (p. 56) is a space $\tilde X$ with a map $p:\tilde X\to X$ such that every $x\in X$ has an open neighborhood $U$ whose preimage is a disjoint union of open sets each mapped homeomorphically onto $U$; $p^{-1}(U)$ may be empty, so $p$ need not be surjective. This is Mathlib's IsCoveringMap. For a covering space with basepoints $p:(\tilde X,\tilde x_0)\to(X,x_0)$ we write

$$p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0),\qquad H=p_*\big(\pi_1(\tilde X,\tilde x_0)\big)\le\pi_1(X,x_0)$$

for the induced homomorphism (Hatcher.coverHom) and its image (Hatcher.coverSubgroup).

$X$ is semilocally simply-connected (p. 63, Hatcher.IsSemilocallySimplyConnected) if each $x\in X$ has a neighborhood $U$ such that every loop at $x$ contained in $U$ is null-homotopic in $X$. The bundle Hatcher_Covering also fixes: the structure CoveringSpace X (a total space $\tilde X$ and a covering map $p$) and its pointed version PointedCover X x₀ (with $\tilde x_0\in p^{-1}(x_0)$ and associated subgroup PointedCover.subgroup); isomorphism of covering spaces (p. 67), a homeomorphism $f:\tilde X_1\to\tilde X_2$ with $p_1=p_2f$, with or without preservation of basepoints (IsIsomorphic, IsPointedIsomorphic); the deck transformation group $G(\tilde X)$ (p. 70, deckGroup), the self-homeomorphisms of $\tilde X$ commuting with $p$; normal covering spaces (p. 70, IsNormalCover); Hatcher's condition $(\ast)$ for a covering space action of a group $G$ on $Y$ (p. 72, IsCoveringSpaceAction); and the orbit space $Y/G$ with its quotient map (OrbitSpace, orbitProj).

Formalization targets

Goal (Theorem 1.38, p. 67)

Let $X$ be path-connected, locally path-connected and semilocally simply-connected, with basepoint $x_0$. Then:

1. every subgroup $H\le\pi_1(X,x_0)$ is $p_*\pi_1(\tilde X,\tilde x_0)$ for some path-connected covering space with basepoint;
2. two path-connected covering spaces with basepoints are isomorphic by a basepoint-preserving isomorphism iff their subgroups coincide;
3. two path-connected covering spaces are isomorphic (basepoints ignored) iff their subgroups, at some choice of basepoints over $x_0$, are conjugate in $\pi_1(X,x_0)$.

Together these say that $(\tilde X,\tilde x_0)\mapsto p_*\pi_1(\tilde X,\tilde x_0)$ is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.

Milestones

1. Proposition 1.31 (p. 61), first part: $p_*$ is injective.
2. Proposition 1.31, second part: $p_*\pi_1(\tilde X,\tilde x_0)$ consists of the classes of loops at $x_0$ whose lifts starting at $\tilde x_0$ are loops.
3. Proposition 1.32 (p. 61): for $X,\tilde X$ path-connected, the fibre $p^{-1}(x_0)$ is in bijection with the cosets of $H$, so the number of sheets is the index of $H$.
4. Proposition 1.33 (p. 61), the lifting criterion: for $Y$ path-connected and locally path-connected, $f:(Y,y_0)\to(X,x_0)$ lifts to $(\tilde X,\tilde x_0)$ iff $f_*\pi_1(Y,y_0)\subseteq H$.
5. Proposition 1.34 (p. 62), unique lifting: two lifts of $f:Y\to X$ agreeing at one point agree everywhere if $Y$ is connected.
6. Necessity of semilocal simple connectivity (p. 63): if $X$ has a simply-connected covering space (surjective onto $X$), then $X$ is semilocally simply-connected.
7. Existence of a simply-connected covering space (pp. 63–65): if $X$ is path-connected, locally path-connected and semilocally simply-connected, it has a simply-connected covering space (the universal cover).
8. Proposition 1.36 (p. 66): under the same hypotheses, every subgroup $H\le\pi_1(X,x_0)$ is realized as $p_*\pi_1(X_H,\tilde x_0)$ for a path-connected covering space.
9. Proposition 1.37 (p. 67): for $X$ path-connected and locally path-connected, two path-connected covering spaces with basepoints are basepoint-preservingly isomorphic iff their subgroups are equal.
10. Change of basepoint (pp. 67–68, proof of Theorem 1.38): moving $\tilde x_0$ within $p^{-1}(x_0)$ replaces $H$ by a conjugate, and every conjugate arises this way.
11. Proposition 1.39(a) (p. 71): a path-connected covering space of a path-connected, locally path-connected $X$ is normal iff $H$ is a normal subgroup.
12. Proposition 1.39(b): $G(\tilde X)\cong N(H)/H$, given as a surjective homomorphism $N(H)\to G(\tilde X)$ with kernel $H$.
13. Proposition 1.39, final clause: for the universal cover, $G(\tilde X)\cong\pi_1(X,x_0)$.
14. Proposition 1.40(a) (p. 72): for a covering space action of $G$ on $Y$, the quotient map $Y\to Y/G$ is a normal covering space.
15. Proposition 1.40(b): if moreover $Y$ is path-connected, $G$ is the group of deck transformations of $Y\to Y/G$, via $g\mapsto(y\mapsto gy)$.
16. Proposition 1.40(c): if $Y$ is path-connected and locally path-connected, $G\cong\pi_1(Y/G)/p_*\pi_1(Y)$, given as a surjective homomorphism $\pi_1(Y/G)\to G$ with kernel $p_*\pi_1(Y)$.

Significance

The result itself. The classification theorem is the central structural fact about covering spaces: the connected coverings of $X$ are "the same as" the subgroups of $\pi_1(X)$, with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces ($\pi_1(\mathbb{RP}^n)=\mathbb{Z}/2$, $\pi_1(T^n)=\mathbb{Z}^n$, lens spaces) and is used throughout Hatcher's later chapters.

Formalizing it. Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (IsCoveringMap.liftPath, liftHomotopy), the monodromy action (IsCoveringMap.monodromy), the injectivity of $p_*$ (injective_path_homotopic_map, cited there as Proposition 1.31), the unique-lifting statement (IsCoveringMap.eq_of_comp_eq), and the lifting criterion itself (existsUnique_continuousMap_lifts_of_range_le, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has IsQuotientCoveringMap, with the homomorphism $\pi_1(Y/G)\to G^{\mathrm{op}}$ and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings $X_H$, no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.

Difficulty

The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from $x_0$, the topology is generated by the sets $U_{[\gamma]}$ for $U$ in the basis of path-connected open sets on which $\pi_1$ dies, and one must verify that this is a topology basis, that $p$ is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by $H$ and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.

Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in $N(H)$ to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on $Y/G$ and the evenly covered neighborhoods $p(U)$ from condition $(\ast)$; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.

Formalization scope

• Spaces are arbitrary topological spaces; hypotheses (path-connectedness, local path-connectedness, semilocal simple connectivity, connectedness of the domain in Proposition 1.34) are stated per theorem, exactly where Hatcher assumes them.
• CoveringSpace X bundles a total space in the same universe as $X$ with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings $X_H$ are constructed from paths in $X$, they live in that universe, so nothing is lost.
• "Isomorphic" is the existence of a homeomorphism over $X$ (Hatcher, p. 67), a proposition on pairs of covering spaces; Theorem 1.38 is stated as the three-part conjunction above rather than as a bijection between quotient sets, which avoids forming the set of isomorphism classes of types while asserting exactly the same content.
• Conjugacy is expressed with Mathlib's MulAut.conj; "number of sheets equals the index" is stated as a bijection $p^{-1}(x_0)\simeq\pi_1(X,x_0)/H$ with the coset space.
• The isomorphisms of Propositions 1.39(b) and 1.40(c) are stated as surjective homomorphisms with prescribed kernel, which is how Hatcher proves them and avoids requiring a Normal instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on $Y$ prescribed.
• A covering space action includes continuity of each $y\mapsto gy$ (Hatcher's actions are by homeomorphisms). The orbit space is Mathlib's MulAction.orbitRel.Quotient with the quotient topology.
• Trivializing readings are excluded: path-connected spaces are nonempty, and a nonempty covering space of a path-connected base is surjective; milestone 6 assumes surjectivity explicitly because its base need not be connected.

Contributions welcome: a reusable construction of the space of path classes with its topology, the covering $X_H$, and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.3, pp. 56–72. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• E. H. Spanier, Algebraic Topology, Springer, 1966, Chapter 2 (covering spaces and the classification theorem).
• J. R. Munkres, Topology, 2nd ed., Prentice Hall, 2000, Chapter 13 (classification of covering spaces).
• Mathlib, Mathlib/Topology/Covering/Basic.lean (covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.lean
• Mathlib, Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting, monodromy, the lifting criterion). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean
• Mathlib, Mathlib/Topology/Covering/Quotient.lean (quotient covering maps for group actions). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean

Motivation

Once $\pi_1(S^1)\cong\mathbb{Z}$ is known, the next question in Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) is how to compute fundamental groups of spaces built from pieces. Section 1.2 answers this with van Kampen's theorem (Theorem 1.20, p. 43): if a space is covered by open sets with a common basepoint and path-connected intersections, its fundamental group is the free product of the fundamental groups of the pieces, modulo relations coming from the intersections. It is the main computational tool of Chapter 1: it gives the fundamental groups of wedges of circles, graphs, surfaces, and every CW complex from its 2-skeleton (Propositions 1.26–1.28), and it underlies the classification of covering spaces in Section 1.3.

This is the second mission in the series formalizing Hatcher's book. The first mission established the covering-space lifting properties and $\pi_1(S^1,1)\cong\mathbb{Z}$ in the Lean namespace Hatcher; this one covers the subsection "The van Kampen Theorem" of Section 1.2 (pp. 41–47) together with its warm-up Lemma 1.15 and Proposition 1.14 from Section 1.1 (p. 35).

Setting

Let $X$ be a topological space with a basepoint $x_0$. A path is a continuous map $I=[0,1]\to X$, a loop at $x_0$ is a path with both endpoints $x_0$, and $\pi_1(X,x_0)$ is the group of homotopy classes of loops at $x_0$ under concatenation. A continuous map $\varphi:X\to Y$ with $\varphi(x_0)=y_0$ induces a homomorphism $\varphi_*:\pi_1(X,x_0)\to\pi_1(Y,y_0)$, $[f]\mapsto[\varphi\circ f]$.

Let $(A_\alpha)_{\alpha\in\iota}$ be a family of subsets of $X$, each containing $x_0$, with the subspace topology; write $\pi_1(A_\alpha)$ for $\pi_1(A_\alpha,x_0)$. The inclusions $A_\alpha\hookrightarrow X$ induce

$$j_\alpha:\pi_1(A_\alpha)\to\pi_1(X),$$

which are Hatcher.inclHom, and the inclusions $A_\alpha\cap A_\beta\hookrightarrow A_\alpha$ and $A_\alpha\cap A_\beta\hookrightarrow A_\beta$ induce

$$i_{\alpha\beta}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\alpha),\qquad i_{\beta\alpha}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\beta),$$

which are Hatcher.interHomLeft and Hatcher.interHomRight.

The free product $\ast_\alpha G_\alpha$ of a family of groups is the group of reduced words in the $G_\alpha$ (Hatcher, pp. 41–42); in Lean it is Mathlib's Monoid.CoprodI, here Hatcher.FreeProd. Its universal property extends the $j_\alpha$ to a single homomorphism

$$\Phi:\ast_\alpha\pi_1(A_\alpha)\to\pi_1(X),$$

Hatcher.vanKampenHom. Since $j_\alpha i_{\alpha\beta}=j_\beta i_{\beta\alpha}$ (both are induced by $A_\alpha\cap A_\beta\hookrightarrow X$), the elements

$$i_{\alpha\beta}(\omega)\,i_{\beta\alpha}(\omega)^{-1},\qquad \omega\in\pi_1(A_\alpha\cap A_\beta),$$

lie in the kernel of $\Phi$. Let $N$ be the normal subgroup generated by all of them, Hatcher.vanKampenNormal.

Formalization targets

Goal (Theorem 1.20)

If $X$ is the union of path-connected open sets $A_\alpha$ each containing $x_0$, each $A_\alpha\cap A_\beta$ is path-connected, and each $A_\alpha\cap A_\beta\cap A_\gamma$ is path-connected, then

$$\Phi \text{ is surjective}\qquad\text{and}\qquad \ker\Phi=N .$$

Hence $\Phi$ induces an isomorphism $\pi_1(X)\cong\ast_\alpha\pi_1(A_\alpha)/N$.

Milestones

1. Lemma 1.15 (p. 35). If $X$ is the union of path-connected open sets $A_\alpha$ containing $x_0$ with each $A_\alpha\cap A_\beta$ path-connected, then every loop in $X$ at $x_0$ is homotopic to a product of loops each of which is contained in a single $A_\alpha$.
2. Proposition 1.14 (p. 35). $\pi_1(S^n)=0$ for $n\ge 2$.
3. Theorem 1.20, first part (p. 43). Under the hypotheses of Lemma 1.15, $\Phi$ is surjective.
4. The kernel contains the relators (p. 43). $N\le\ker\Phi$, with no hypotheses on the cover.
5. Theorem 1.20, second part (p. 43). If moreover every triple intersection is path-connected, $\ker\Phi\le N$.
6. Induced isomorphism (p. 43). Under the same hypotheses there is an isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ sending the class of a word to its image under $\Phi$.

Significance

The result itself. Van Kampen's theorem is the gluing law for $\pi_1$. With it Hatcher computes $\pi_1$ of wedge sums (free products), of graphs (free groups), of the closed orientable surfaces (Example 1.26), and shows that attaching $2$-cells kills exactly the attaching loops (Proposition 1.26), so that every group is a fundamental group (Corollary 1.28). The surjectivity half alone gives Proposition 1.14, that spheres of dimension at least two are simply connected, and hence that $\mathbb{R}^2$ is not homeomorphic to $\mathbb{R}^n$ for $n\ne 2$ (Corollary 1.16).

Formalizing it. Mathlib has the fundamental groupoid and fundamental group, induced homomorphisms (FundamentalGroup.map), free products of groups (Monoid.CoprodI) with their universal property, normal closures, and quotient groups. It has no version of van Kampen's theorem for topological spaces (its CategoryTheory/Limits/VanKampen concerns colimits in categories, not fundamental groups), and no computation of $\pi_1(S^n)$ for $n\ge 2$; on the platform, however, the theorem SP4Mission.sphere_simplyConnected (already proved in this environment) states that the unit sphere of $\mathbb{R}^n$ is simply connected for $n\ge 3$, which is Proposition 1.14 with shifted indexing, so that milestone can be closed by a one-line reduction. The mission supplies the statements in Hatcher's form, on Mathlib's $\pi_1$, so that later missions (covering spaces, cell complexes) can use them directly.

Difficulty

Surjectivity is a compactness argument: subdivide $I$ so each piece of the loop lies in one $A_\alpha$, then use path-connectedness of the intersections to connect the subdivision points back to $x_0$. The formal difficulty is bookkeeping: producing the subdivision from an open cover of $[0,1]$ (Mathlib's exists_monotone_Icc_subset_open_cover_unitInterval is the tool) and showing the reparametrised concatenation is homotopic to the original loop.

The kernel computation is the hard part. Hatcher's proof takes a homotopy $F:I\times I\to X$ between two factorizations, subdivides the square into rectangles each mapped into a single $A_\alpha$, perturbs the grid so at most three rectangles meet at a corner (this is where triple intersections enter), and then shows that moving the loop across one rectangle at a time changes the factorization only by the two elementary moves that hold in $\ast_\alpha\pi_1(A_\alpha)/N$. Every step is elementary, but the induction over the grid is long, and each elementary move requires an explicit path-homotopy in a subspace. The naive idea of proving $\ker\Phi\le N$ by an induction on word length does not work: the relation between two factorizations of the same loop is only visible through a homotopy in $X$, not through the words.

Proposition 1.14 is easy given Lemma 1.15 but requires exhibiting the cover of $S^n$ by two complements of antipodal points, showing each is simply connected (homeomorphic to $\mathbb{R}^n$ via stereographic projection, which Mathlib has as stereographic), and showing their intersection is path-connected when $n\ge 2$.

Formalization scope

• The index set $\iota$ and the space $X$ are arbitrary; the $A_\alpha$ are Set X with the subspace topology, and $\pi_1(A_\alpha)$ is Mathlib's FundamentalGroup ↥(A α) ⟨x₀, _⟩. Hypotheses are stated explicitly on each theorem: IsOpen, IsPathConnected, ⋃ α, A α = Set.univ, and path-connectedness of pairwise (and, where Hatcher requires it, triple) intersections.
• $i_{\alpha\beta}$ and $i_{\beta\alpha}$ are both defined on $\pi_1(A_\alpha\cap A_\beta)$ (rather than on $\pi_1(A_\beta\cap A_\alpha)$ for the second), so no identification of $A_\alpha\cap A_\beta$ with $A_\beta\cap A_\alpha$ is needed; the set of relators ranges over all ordered pairs $(\alpha,\beta)$.
• "Product of loops" in Lemma 1.15 is a finite List of loops, each tagged with the index $\alpha$ of the piece it lies in, concatenated right-to-left with the constant loop as empty product (Hatcher.loopProd). Any bracketing gives the same homotopy class.
• The goal is stated as the conjunction "surjective and $\ker\Phi=N$"; the isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ is a separate milestone, stated as the existence of a group isomorphism compatible with $\Phi$ on the quotient, which pins it down uniquely.
• $S^n$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1, and "$\pi_1(S^n)=0$" is Mathlib's SimplyConnectedSpace (path-connected with trivial fundamental group), which is what Hatcher means since $S^n$ is path-connected.
• Trivializing readings are excluded: the cover hypotheses do not force $\iota$ nonempty, but then $X=\bigcup A_\alpha=\varnothing$ contradicts the existence of $x_0$, so the statements are not vacuous in any interesting case, and $\Phi$ is the specific homomorphism induced by the inclusions.

Contributions welcome: the subdivision lemma for loops in an open cover, a reusable treatment of factorizations and their elementary moves, and the two-set special case $\pi_1(X)\cong(\pi_1(A)\ast\pi_1(B))/N$ as a corollary.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.2, pp. 40–49; Lemma 1.15 and Proposition 1.14, p. 35. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• E. R. van Kampen, On the connection between the fundamental groups of some related spaces, American Journal of Mathematics 55 (1933), 261–267. https://doi.org/10.2307/2371128
• H. Seifert, Konstruktion dreidimensionaler geschlossener Räume, Berichte Sächs. Akad. Leipzig 83 (1931), 26–66.
• Mathlib, Mathlib/GroupTheory/CoprodI.lean (free products of groups). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.lean
• Mathlib, Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (fundamental group and induced homomorphisms). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean