Classifying covering types in homotopy type theory

This paper formalizes the Galois correspondence between covering spaces and subgroups of fundamental groups within homotopy type theory, extends the concept to n-dimensional generalizations, and applies the framework to classify lens space coverings and construct the Poincaré homology sphere.

The Gist

Imagine you are trying to understand the shape of a mysterious, complex object—let's call it a "Space." In mathematics, specifically in a field called algebraic topology, one of the best ways to understand a Space is to look at its "holes" and loops.

This paper by Samuel Mimram and Émile Oleon is about a powerful tool called Covering Spaces. Think of a covering space as a "super-detailed map" or a "zoomed-in version" of your original Space.

Here is the breakdown of their work using simple analogies:

1. The Core Idea: The "Unrolled" Map

Imagine your original Space is a Möbius strip (a loop with a twist). If you walk along it, you eventually return to where you started, but you are upside down. It's confusing!

A Covering Space is like unrolling that Möbius strip into a long, flat ribbon.

• On the ribbon, you can walk forever without ever getting confused or returning to the start.
• However, if you look at the ribbon from above, it still looks exactly like the Möbius strip.
• Every point on the Möbius strip has a whole stack of points on the ribbon directly above it.

In math, this "unrolling" helps us study the "loops" (fundamental groups) of the original shape. The most famous version of this is the Universal Covering, which unrolls the shape completely until it has no loops left at all.

2. The New Language: Homotopy Type Theory (HoTT)

Usually, mathematicians study these shapes using geometry and calculus. But this paper uses a different language called Homotopy Type Theory (HoTT).

• The Analogy: Imagine HoTT as a "Lego language" for shapes. Instead of drawing curves and calculating angles, you build shapes out of logical blocks (types).
• The Benefit: In this Lego world, if two shapes can be stretched or squished into each other without tearing (homotopy), they are considered the same. This makes proving things about shapes much more logical and computer-friendly. The authors are essentially writing a "user manual" for how to build and classify these unrolled maps using Lego blocks.

3. The "Galois Correspondence": The Master Key

The paper proves a famous relationship called the Galois Correspondence.

• The Analogy: Imagine the original Space is a locked room. The "Fundamental Group" is the set of all possible keys (loops) that fit in the lock.
• The Discovery: The authors show that there is a perfect one-to-one match between:
  1. The different ways you can "unroll" the room (Covering Spaces).
  2. The different groups of keys you can pick from the master set (Subgroups).

If you pick a specific group of keys, you get a specific unrolled map. If you pick a different group, you get a different map. It's like a master keyring where every combination of keys opens a specific version of the room.

4. Generalizing to "n-Coverings"

The authors didn't just stop at the standard "unrolling." They invented a new concept called n-coverings.

• The Analogy: Think of a standard covering as unrolling a shape until it has no 1-dimensional loops (like a circle).
• The Innovation: They created a system to unroll shapes until they have no 2-dimensional holes (like the surface of a ball), no 3-dimensional holes, and so on.
• They call the "fully unrolled" version the Universal n-covering. It's a shape that is so smooth and simple that it has no "knots" or "holes" up to a certain dimension.

5. Real-World Applications: Lens Spaces and Poincaré's Sphere

To prove their theory works, they applied it to some tricky shapes:

• Lens Spaces: Imagine taking a sphere and twisting it in a specific way before gluing the ends together. These are called Lens Spaces. The authors used their "Lego logic" to list every possible way to unroll these twisted spheres. It's like cataloging every possible way to untangle a specific type of knot.
• The Poincaré Homology Sphere: This is a famous, weird shape invented by the mathematician Poincaré. It looks like a sphere from the inside (it has the same "homology" or fluid flow properties as a sphere), but it has a different "loop structure."
  • The authors showed how to build this strange shape by taking a perfect 3D sphere and gluing its points together according to a specific set of rules (a group action).
  • They proved that this shape is essentially a "quotient" of the sphere, created by the same "unrolling" logic they developed.

Why Does This Matter?

• For Mathematicians: It provides a rigorous, computer-checkable way to understand the relationship between shapes and their loops. It bridges the gap between geometry and logic.
• For the Future: By formalizing this in a language computers understand (Type Theory), they are paving the way for software that can automatically verify complex geometric proofs. It's like teaching a computer to "see" the shape of the universe and understand how to unroll it.

In a nutshell: The authors built a new, logical toolkit to "unroll" complex shapes into simpler ones. They proved that every way you can unroll a shape corresponds perfectly to a specific set of rules (keys) governing that shape. They then used this toolkit to solve puzzles involving twisted spheres and other exotic geometric objects.

Technical Summary

Here is a detailed technical summary of the paper "Classifying covering types in homotopy type theory" by Samuel Mimram and Émile Oleon.

1. Problem Statement

The paper addresses the formalization of covering spaces and the Galois correspondence (the bijection between coverings of a space and subgroups of its fundamental group) within Homotopy Type Theory (HoTT).

While the correspondence is a cornerstone of classical algebraic topology, its translation into HoTT presents specific challenges:

• Synthetic Geometry: HoTT treats types as spaces up to homotopy. Defining "local triviality" (the standard topological definition of a covering) is difficult because HoTT lacks an intrinsic notion of open sets or local neighborhoods.
• Generalization: The authors aim to move beyond the classical case ($n=0$) to define and classify $n$-coverings, which generalize the concept of covering spaces to higher homotopical dimensions.
• Constructive Proofs: The goal is to provide proofs that are shorter, more conceptual, and amenable to generalization compared to traditional topological proofs, leveraging the univalence axiom and higher inductive types.

2. Methodology

The authors utilize the synthetic approach of HoTT, relying on the following core concepts:

• Grothendieck Duality: They exploit the equivalence between fibrations over a type $A$ and type families indexed by $A$ ($U/A \simeq (A \to U)$). This allows them to define coverings as families of types with specific truncation properties rather than geometric maps.
• Truncation and Connectivity: They use $n$-truncation ($\|A\|_n$) to define $n$-types and $n$-connectedness. An $n$-covering is defined as a map whose fibers are $n$-types.
• Factorization Systems: They utilize the $(n+1)$-connected / $n$-truncated factorization system. Any map can be factored uniquely into an $(n+1)$-connected map followed by an $n$-truncated map. This factorization is central to constructing universal coverings.
• Delooping: The construction of classifying spaces ($BG$) for groups is used to relate group actions to fibrations.
• Formalization: The work is grounded in constructive mathematics and has been partially formalized in Cubical Agda.

3. Key Contributions

A. Definition of $n$-Covering Types

The authors generalize the notion of a covering space.

• Definition: An $n$-covering of a type $A$ is a map $p: B \to A$ such that all fibers are $n$-types (i.e., the map is $n$-truncated).
• Universal $n$-Covering: They define the universal $n$-covering ($\tilde{A}_n$) as the unique pointed $n$-covering that is initial in the category of pointed $n$-coverings.
• Construction: The universal $n$-covering is constructed via the $n$-image of the pointing map $1 \to A$. Specifically,$\tilde{A}_n$is the total space of the map$p_n: \text{im}_n(1 \to A) \to A$.
• Properties:
  • The total space $\tilde{A}_n$ is $(n+1)$-connected.
  • It "kills" homotopy groups $\pi_i$ for $i \leq n+1$ while preserving $\pi_i$ for $i > n+1$.
  • For $n=0$, this recovers the standard universal covering (where $\tilde{A}$ is 1-connected).

B. The Galois Correspondence in HoTT

The paper provides a rigorous proof of the Galois correspondence for $n=0$ (standard coverings).

• The Galois Fibration: They define a canonical map $g_A: A \to \|\!A\!\|_1$ (where $\|\!A\!\|_1 \simeq B\pi_1(A)$). The fiber of this map is the universal covering $\tilde{A}$.
• Classification Theorem (Theorem 36): There is an equivalence between:
  1. The type of subgroups of the fundamental group $\pi_1(A)$.
  2. The type of pointed, connected coverings of $A$.
• Mechanism:
  • From Subgroup to Covering: Given a subgroup inclusion $i: H \hookrightarrow \pi_1(A)$, the corresponding covering is the pullback of the Galois fibration $g_A$ along the delooping $Bi: BH \to B\pi_1(A)$.
  • From Covering to Subgroup: Given a connected covering $f: X \to A$, the corresponding subgroup is the image of the induced map on fundamental groups $\pi_1(f): \pi_1(X) \to \pi_1(A)$.
• Proof Strategy: The proof relies on the fact that the fiber of the map $Bi$ is the set of cosets $G/H$, and uses the universal property of the pullback to establish the bijection.

C. Applications to Specific Spaces

The authors demonstrate the utility of their framework by classifying coverings for specific, non-trivial spaces:

1. Lens Spaces ($L^k_n$):
   • Defined as the source of a map $\phi: L \to B\mathbb{Z}_n$.
   • The fundamental group is $\mathbb{Z}_n$.
   • The paper classifies all connected coverings of Lens spaces as $L^k_m$ where $m$ divides $n$. The projection maps are constructed via joins of maps $S^1 \to B\mathbb{Z}_m$.
2. Poincaré Homology Sphere and Hypercubical Manifold:
   • These spaces are constructed as quotients of the 3-sphere ($S^3$) by finite groups (Binary Icosahedral group and Quaternion group, respectively).
   • The authors show how to construct the Galois fibration $\phi: D \to B\pi_1(D)$ for these spaces.
   • By proving the fiber of this map is $S^3$, they formally establish that these spaces are quotients of $S^3$ under coherent group actions, validating their construction as higher inductive types.

4. Results

• Formal Equivalence: Established a constructive equivalence between subgroups of $\pi_1(A)$ and connected coverings of $A$ within HoTT.
• Generalization: Successfully defined $n$-coverings and characterized their universal forms, showing that the universal $n$-covering is the $(n+1)$-connected cover.
• Computational Verification: The classification of Lens space coverings and the construction of the Poincaré homology sphere serve as concrete, non-trivial validations of the theory.
• Conjecture: The authors conjecture that the connected component of the universal $n$-covering in the type of all $n$-coverings corresponds to the delooping of the fundamental $n$-group of $A$.

5. Significance

• Synthetic Topology: The paper demonstrates that complex topological concepts like covering spaces and the Galois correspondence can be developed purely synthetically in type theory, without relying on point-set topology (open sets, local triviality).
• Proof Efficiency: The HoTT proofs are described as "shorter and more conceptual" than traditional topological proofs, relying on the structural properties of types (univalence, truncation) rather than geometric constructions.
• Foundation for Higher Structures: By introducing $n$-coverings, the paper lays the groundwork for a higher-dimensional Galois theory, potentially linking higher homotopy groups to higher categorical structures (higher groupoids).
• Formalization: The work contributes to the library of formalized mathematics (specifically in Agda), providing verified definitions and theorems for algebraic topology within a constructive logic framework.

In summary, Mimram and Oleon successfully bridge the gap between classical algebraic topology and Homotopy Type Theory, providing a robust, generalized framework for understanding covering spaces and their classification via fundamental groups.