\(\newcommand{\textesh}{∫}\) \(\newcommand{\ensuremath}{}\)

Abstract

Homotopy type theory captures all the major concepts of differential geometry including forms, connections, curvature, and gauge theory. We show this by focusing on combinatorial manifolds, which are discrete in the sense of real cohesion (Shulman, 2017), and drawing inspiration from the similarly young field of discrete differential geometry.

“It is always ourselves we work on, whether we realize it or not. There is no other work to be done in the world.” — Stephen Talbott, The Future Does Not Compute (Talbott, 1995)

1 Introduction: Discrete differential geometry

The observation that sparks the following discussion is this: if we can manage to reformulate differential geometry in discrete terms (i.e. finite, without infinitesimals) then we may also be able to construct it synthetically in homotopy type theory. Furthermore, if we do capture geometry in HoTT then there’s a chance that it can become clearer and smaller. We would then have new tools, a new audience, and a new program to (re)explore geometry, gauge theory, low dimensional topology, and mathematical physics.

Applied mathematicians and computer scientists have been developing discrete differential geometry (DDG) for many years. The 2003 Ph.D. thesis of Anil Hirani (Hirani, 2003) (see also the multi-author follow-up (Desbrun et al., 2005)) defines finite versions of vector fields, differential forms, the wedge product, the Hodge star, and several differential operators (exterior derivative, div, grad, curl, Laplace-Beltrami, Lie derivative). Hirani and others cite Whitney’s 1957 book Geometric Integration Theory (Whitney, 1957) which develops a theory of cochains by integrating smooth forms over chains. In 2004 Melvil Leok, Jerrold Marsden, and Alan Weinstein (Leok et al., 2005) defined discrete connections on principal bundles. This is probably the work most spiritually similar to this paper. The motivation for the above constructions was applied mathematics: modeling the differential equations of mechanics and fluid mechanics with the so-called “finite element” methods. The theory has been adopted and extended by the computer graphics community as well (see Keenan Crane’s course notes (Crane et al., 2013) for a gentle survey).

The applied category theory community has begun to develop category theoretic foundations and software libraries to increase the reusability and compositionality of finite element methods in science and engineering problems. See for example recent work to bring discrete exterior calculus into the AlgebraicJulia library (Morris et al., 2024) (Patterson et al., 2022).

For these classically-minded applied mathematicians DDG is defined on combinatorial manifolds such as simplicial complexes, of any finite dimension. The 0-cells play the role of points, the 1-cells are path segments, and so on. They define \(n\)-forms as functions on the \(n\)-dimensional faces of the manifold into the real numbers, which is then extended by linearity to arbitrary \(n\)-chains. Exterior differentiation is defined by Stokes theorem (which is no longer a theorem in this setting), by which we mean the following.

We will take the following path. We will use DDG as a stepping stone between smooth geometry and HoTT. We will learn how to see the finite analogues of infinitesimal constructions, and then use the syntax of type theory to re-present them. It won’t always be a two-step process! Sometimes even the smooth arguments are made with finite combinatorial methods, and then a limit is taken. This is especially true where the Gauss-Bonnet and Poincaré-Hopf theorems are concerned. \[\mathrm{Differential\ geometry}\longrightarrow\mathrm{Discrete\ differential\ geometry}\longrightarrow \mathrm{Homotopy\ type\ theory}\]

2 Examples

TODO:

1. Color-code each continuous cycle on the flat torus and the 3d torus, and use that to demonstrate how the curvature acts (begun).

2. There’s a missing argument here. I motivate some particular permutation of hexagons with geometric analogy, but what is actually being said? Why is this making contact with anything? Does it have to wait for the proof of Poincaré-Hopf and Gauss-Bonnet?

2.1 The octahedron

We will define some higher inductive types to serve as domain and codomain of these motivating examples.

2.1.1 The higher inductive type \(\ensuremath{\mathbb{O}}\)

First we need a square, which will be a stand-in for a circle that can support a notion of a quarter-rotation.

We may also think of \(C_4\) as the join of the two-element sets \(\{c_1, c_3\}* \{c_2, c_4\}\).

We have obvious maps \(\ensuremath{\mathbb{O}}_0\xrightarrow[]{i_0} \ensuremath{\mathbb{O}}_1\xrightarrow[]{i_1} \ensuremath{\mathbb{O}}\) that include each skeleton into the next-higher-dimensional skeleton.

2.1.2 \(\mathsf{link}\), \(\mathsf{xbox}\), and \(\mathsf{xdisk}\)

Here we’ll define combinatorial versions of tangent spaces and tangent circles, in the special case where every vertex has four neighbors.

Combinatorial spaces have a concept called the link of a vertex, which will be the main tool by which we connect with manifold theory. The vertices in the link are the vertices that are one edge away from the given point (its immediate neighbors), and the edges in the link are the edges connecting the neighbors to each other. If the link of an \(n\)-dimensional combinatorial space is always a combinatorial \(n-1\)-sphere, then we say the space is a combinatorial triangulation. We will look only at HITs that have a link that is merely equivalent to \(C_4\). So first we need notation for a connected component of the universe:

Denote by \(abcd:\mathrm{BAut}C_4\) the HIT with vertices \(a, b, c, d\) and edges \(ab, bc, cd, da\) which clearly has various isomorphisms with \(C_4\).

We can now define a map \(\mathsf{link}:\ensuremath{\mathbb{O}}_0\to\mathrm{BAut}C_4\). Extending this later on to the 1-skeleton and 2-skeleton will take us into differential geometry!

Besides the link we also want to consider the 5-pointed object that includes the vertex itself and the edges connecting it to the vertices in the link. We will call such a shape an xbox since it is a square with both diagonals. We will denote xboxes by extending the square notation with a fifth letter to indicate the center of the xbox. For example, we can define an xbox \(C_{4c}\) as follows:

And we get a map \(\mathsf{xbox}:\ensuremath{\mathbb{O}}_0\to\mathsf{Type}\) similarly to \(\mathsf{link}\).

Finally we want to consider the 2-type that fills in the faces of the xbox. This is a contractible type we will call an xdisk.

We can define \(\mathsf{xdisk}:\ensuremath{\mathbb{O}}_0\to\mathrm{BAut}C_{4c\mathsf{xdisk}}\) by filling in the triangles in \(\mathsf{xbox}\).

2.1.3 Extending \(\mathsf{link}\)

Note that \(\mathrm{BAut}C_4\) is of homotopy dimension at least 2, just as \(\ensuremath{\mathbb{O}}\) is. The paths are isomorphisms between types that are merely equivalent to squares, and the 2-paths are homotopies between these. We can make further use of Figure 1 by imagining how \(\mathsf{link}\) changes as we slide from point to point. Sliding from \(w\) to \(b\) and tipping the link as we go, we see \(r\mapsto r\) and \(o\mapsto o\) because those lie on the axis of rotation. Then \(g\mapsto w\) and \(b\mapsto y\).

The full map on the 1-skeleton is:

It’s very important to be able to visualize what \(T_1\) does to triangular paths such as \(wb\cdot br\cdot rw\) (which circulates around the boundary of face \(wbr\)). You can see it if you imagine Figure 1 as the frames of a short movie. Or you can place your palm over the top of a cube and note where your fingers are pointing, then slide your hand to an equatorial face, then along the equator, then back to the top. The answer is: you come back rotated clockwise by a quarter-turn.

Now let’s extend \(T_1\) to all of \(\ensuremath{\mathbb{O}}\) by providing values for the eight faces. The face \(wbr\) is a path from \(\ensuremath{\mathsf{refl}}_w\) to the concatenation \(wb\cdot br\cdot rw\), and so the image of \(wbr\) under the extended version of \(T_1\) must be a homotopy from \(\ensuremath{\mathsf{refl}}_{T_1(w)}\) to \(T_1(wb\cdot br\cdot rw)\).

All the faces do the same thing: they map to a homotopy between the identity and clockwise rotation by a quarter turn. Concatenating the eight faces in the 2-groupoid \(\ensuremath{\mathbb{O}}\) would then map to a homotopy between the identity and two full rotations. This makes visible in HoTT the link between curvature and the euler characteristic (which is 2 for the octahedron).

2.2 The torus

We can define a combinatorial torus as a similar HIT. This time each vertex will have six neighbors. So all the links will be merely equal to \(C_6\) which is a hexagonal version of \(C_4\). See Figure 2.

To help parse this figure, imagine instead Figure 3. We take this simple alternating-triangle pattern, then glue the left and right edges, then bend into Figure 2. The fact that each column in Figure 3 has four dots corresponds to the torus in Figure 2 having a square in front, diamonds in the middle, and a square in back.

It’s a bit of a challenge to visualize how the connection should twist these “xhexes” as we move around. Part of the issue is that we have actually constrained ourselves quite a bit by requiring the tangent space to be the link of a point, which only has six points. We could be more precise about angles if the tangent spaces had many subdivisions of the circle. The way to achieve better approximations, which we will not pursue in this paper, is to refine a given triangulation, and then choose a contractible neighborhood for each point which is not the link but goes “farther out” and consists of many edges and encloses many triangles. We could then transport along a single edge, and map between two circles that each have many segments, approximating to arbitrary precision any real-world application. The theory and practice of refinements is extensive and includes computer graphics research.

But given an arbitrary edge on our impoverished 3d-embedded torus, how should we decide how to map the hexagons at the endpoints? The goal is of course to approximate the actual geometry of transport on a curved torus, so we should learn a little about that. Which is comforting – we’re trying to capture geometry, so it’s good that we need to use some!

Of all the edges on our shape, the ones that are not very similar to geodesics are the squares in front and back. The two diamonds clearly correspond to highly symmetric geodesics, and less clearly there are four other cycles that are close enough to geodesics that if we drew the edges curved, they’d be actual geodesics on the torus they were hugging (Figure 5).

Transport along geodesics is minimal in a technical sense, meaning the least twisty. If we use the flat torus diagram to help us, then we can identify the outer and inner diamond, which are three of the vertical black lines, as geodesics, as well as all of the diagonal lines, which are the ones in Figure 5. That leaves only the black vertical lines that go around the front and back squares. Those are not geodesics, and some twisting will take place there.

I am talking about twisting on individual edges, but that’s not a concept with standalone meaning since the hexagons are torsors. I’m impicitly using the flat torus to makes the hexagons all pointed, by pointing them at the top as they appear in Figure 3. But let’s not use that extra information, and instead let’s start talking about loops around faces.

2.3 Combinatorial manifolds

(This section is not quite off the ground.)

The combinatorial structure we have in mind is a nerve of a good open cover. What do we know about which smooth manifolds have such covers? While we’re at it, let’s survey all the combinatorial-flavored spaces and survey what smooth manifolds are homotopy equivalent to which structures.

What topological manifolds are equivalent to a CW complex? The answer is the composition of a few results summarized by Allen Hatcher¹ (citing (Kirby & Siebenmann, 1977) and (Freedman & Quinn, 1990)):

Every topological manifold has a handlebody structure except in dimension 4, where a 4-manifold has a handlebody structure if and only if it is smoothable. This is a theorem on page 136 of Freedman and Quinn’s book “Topology of 4-Manifolds”, with a reference given to the Kirby-Siebenmann book for the higher-dimensional case. It is then an elementary fact that an \(n\)-manifold with a handlebody structure is homotopy equivalent to a CW complex with one \(k\)-cell for each \(k\)-handle, so in particular there are no cells of dimension greater than \(n\). At least in the compact case a manifold with a handlebody structure is in fact homeomorphic to a CW complex with \(k\)-cells corresponding to \(k\)-handles; see page 107 of Kirby-Siebenmann. This probably holds in the noncompact case as well, though I don’t know a reference.

3 Central H-spaces

• introduce torsors

• show subtlety how \(BG\) doesn’t classify stuff since it has extra properties

• draw

  

• H-spaces paper result equating this to a universal cover of a component of the universe. (It should feel significant that \(BS^1\simeq \mathrm{BAut}_1(S^1)\).)

To create a tangent bundle of a surface we need to map loops on the surface to isomorphisms of the plane. For us this means we need to map loops on the surface to circles. That in turn means we are looking for a codomain that is a delooping of the circle.

Let \(G\) be a group consisting of a set (0-type) \(S\), an identity \(e:S\), a multiplication \(\mu:S\times S \to S\), an inverse function \(i:S\to S\) satisfying the group laws (associativity of \(\mu\), unit laws).

Let a \(G\)-type be a type \(X:\mathcal{U}\) equipped with an action \(m:G\to X\simeq X\). To form a classifying type \(\mathsf{GType}\) of \(G\)-types we can let \(G\) act on the universe:

where \(m\) preserves fibers of the universal fibration. We can form type families of \(G\)-types by pulling back this diagram:

If we add to this the requirement that the action be free and transitive, we obtain the type \(\mathsf{GTor}\) of \(G\)-torsors.

Central H-spaces are the classifying spaces for principal bundles on abelian groups. We won’t be able to access the full theory for nonabelian groups just yet, but we hope that the theory of maximal tori and weights might bring even those within reach of the central H-space paradigm.

We will rely on the lovely paper by Buchholtz, Christensen, Flaten and Rijke (Buchholtz et al., 2023).

This result will inform our study of the Leibniz rule: the analogue of the algebra of functions to \(\ensuremath{\mathbb{R}}\) is:

We will also be looking in detail at maps into the classifying space of \(S^1\) bundles. The Buchholtz et al paper (Buchholtz et al., 2023) describes this type in several helpful ways, summarized by:

This means that we can form a sequence of deloopings \(\ensuremath{\mathbb{Z}}, S^1, \mathrm{BAut}_1(S^1), \ldots\).

4 Why this is geometry

How can we double check that we are describing the intended theory of geometry? In this section we will enumerate a wishlist of facts that we believe characterize the subject, and then provide evidence for some of them.

Here are the translations that are covered in the current paper: \[\begin{aligned} & \text{\small Connections are infinitesimal splittings of a} & \quad &\text{\small Paths in a sigma type are equivalent to a} \\ & \text{\small principal bundle.} & \quad&\text{\small pair of paths.} \\ \hline & \text{\small Differentials satisfy the Leibniz (product) rule.} &\quad &\text{\small Horizontal composition in an H-space is} \\ & & \quad&\text{\small performed in two steps.} \\ \hline & \text{\small Connections with 0-truncated groups are covering} &\quad &\text{\small Transport around contractible loops is } \ensuremath{\mathsf{refl}}\\ & \text{\small spaces with unique flat connection.} & \quad&\text{\small when fibers are sets.} \\ \hline & \text{\small The group of gauge transformations (bundle} &\quad &\text{\small Homotopies of classifying maps respect } \\ & \text{\small automorphisms) acts on the space of connections.} & \quad&\text{\small the splitting of paths in sigma types.} \\ \end{aligned}\]

And here are questions to explore in the future:

1. There’s a notion of tensorial that holds for forms but not for connections.

2. Where is the Grassmannian structure of wedge product?

3. The Gauss-Bonnet theorem holds, relating the curvature of a 2-manifold to the Euler characteristic.

4. More generally, characteristic classes of bundles can be computed using a connection (Chern-Weil theory).

4.1 Higher maps contain connections

To hew close to the intended context of the term “connection” we will examine manifold-like types mapping into bundle-classifying-like types. The novelty here, compared to other HoTT investigations, is the focus on combinatorial types to stand in for manifolds.

In recent times it has been believed in the HoTT community that maps from a discrete type to a discrete classifying space can encode only the connections that a classical mathematician would call flat (zero curvature). In this context the word discrete means having the discrete topology, in the sense of cohesion (Shulman, 2017). This is not the case! We will show that if the codomain is a classifying space of \(S^1\) or other group of homotopy dimension at least 1, then non-flat connections appear despite the type \(S^1\) being topologically discrete. Another common meaning of the shorthand “discrete” is to indicate a 0-truncated type, i.e. a set, as opposed to a type with higher homotopical structures. We will show that indeed if the codomain classifies sets, which is the case for example with the classifying space \(B\ensuremath{\mathbb{Z}}\), the delooping of \(\ensuremath{\mathbb{Z}}\), then connections are flat. (The type we denote by \(\mathbb{S}^1\stackrel{\mathrm{def}}{=}\{(x, y)|x^2+y^2=1\}\) is a set and is not topologically discrete. We will not be discussing it at all in this paper.)

The DDG philosophy tells us to look at HITs that are polytope-like. A polytope \(M\) will have finitely many 0-dimesional (point) constructors \(\{m_0^i\}\), finitely many 1-dimesnional constructors \(\{m_1^{ij}:m_0^i=m_0^j\}\), and so on. Type families \(f:M\to \mathcal{U}\) on this type specify where each of these constructors is sent. In DDG parlance, \(f\) restricted to the 0-dimensional constructors of \(M\) is a 0-form and \(f\) restricted to the 1-dimensional constructors (not the 1-skeleton but just the 1-dimensional parts, whatever that means in HoTT) is a 1-form, and so on.

A principal \(S^1\) bundle is a family of \(S^1\) torsors and so we will often be focusing on the function type \(M\to \mathrm{BAut}_1(S^1)\). The novel claim here is that \(M\to \mathrm{BAut}_1(S^1)\) contains more than just all the principal \(S^1\)-bundles: it also contains all the connections on all the bundles. Every connection is present, both curved and flat, because we have complete freedom to specify the images of the paths.

Classically, curvature is a property of the connection. It is computed either on infinitesimal loops, or on the infinitesimal surface bounded by the loop. In fact it is “the derivative of the connection” morally speaking. Getting into the details would wreck the simplicity we’re going for². We will look for curvature by examining \(f\) on 1-dimensional loops. If \(M\) is at least a 2-type and if we want to claim that \(f\) classifies a bundle with connection, then we will be required to map the 2-faces of \(M\) (the 2-dimesional constructors) to a path from \(\ensuremath{\mathsf{refl}}\) to the image of a bounding loop. So at dimension 2 we will impose that constraint. Since \(\mathrm{BAut}_1(S^1)\) is 2-truncated, \(f\) factors through the truncation map \(M\to||M||_2\) and so that’s the top dimension.

There is an example at the end of this paper. For those who are best served by examples, do look at it and return to this point.

4.2 Connections as splittings

The classical story goes like this.

\(VP\) can be visualized as the collection of tangent vectors that point along the fibers. It should be clear that the group \(\mathrm{Aut}P\) acts on \(VP\): an automorphism \(\phi:P\to P\) sends \(V_pP\) to \(V_{\phi(p)}P\), where of course \(\pi(p)=\pi(\phi(p))\).

Being preserved by the action of \(\mathrm{Aut}P\) means that the complementary horizontal subspaces in a given fiber of \(\pi:P\to M\) are determined by the splitting at any single point in the fiber. The action of \(G\) on this fiber can then push the splitting around to all the other points.

The motivation for this definition is that we now have an isomorphism \(T_p\pi:H_pP\to T_{\pi(p)}M\) between each horizontal space and the tangent space below it in \(M\). This means that given a tangent vector at \(x:M\) and a point \(p\) in \(\pi^{-1}(x)\) we can uniquely lift the tangent vector to a horizontal vector at \(p\). We can also lift vector fields and paths in this way. To lift a path \(\gamma:[0,1]\to M\) you must specify a lift for \(\gamma(0)\) and then lift the tangent vectors of \(\gamma\) and prove that you can integrate the lift of that vector field upstairs in \(HP\).

Then, armed with the lifting of paths one immediately obtains isomorphisms between the fibers of \(P\). So the Ehresmann connection, the lifting of paths, and transport isomorphisms between fibers are all recapitulations of the structure that the connection adds to the bundle.

Moving now to HoTT, fix a type \(M:\mathcal{U}\) and a type family \(f:M\to\mathcal{U}\). Path induction gives us the transport isomorphism \(\prod_{p:x=_M y}\mathrm{tr}(p):f(x)=f(y)\). We can use this to define a type of dependent paths, also called pathovers or paths over a given path.

See (Bezem et al., 2023) for more discussion of dependent paths (where they use the term “path over”), including composition, and associativity thereof.

We recall now the identity type of sigma types:

In particular, given \(p:x=_M y\) and \(w:f(x)\) we have \(w\xrightarrow[{p}]{=}tr(p)(w)\simeq tr(p)(w)=_{f(y)}tr(p)(w)\) which has the term \(\ensuremath{\mathsf{refl}}\) which we can call “the horizontal lift of \(p\) starting at \(w\).” We can imitate the classical definition of a connection by defining \(\omega\stackrel{\mathrm{def}}{=}\ensuremath{\mathrm{pr}}_2\circ\mathsf{split}\), the projection onto the vertical component. And thus in HoTT we can see the equivalence of transport and lifting of paths into horizontal and vertical components.

4.3 The Leibniz (product) rule

The Leibniz rule for exterior differentiation states that if \(f, g:M\to \ensuremath{\mathbb{R}}\) are two smooth functions to the real numbers then \(d(fg) = fdg + gdf\). Here \(fg\) is the function formed by taking the pointwise product of \(f\) and \(g\). This is an interaction between multiplication in \(\ensuremath{\mathbb{R}}\) and the action on vectors of smooth functions (the 1-forms \(df\) and \(dg\)).

To examine this situation in HoTT we need type-theoretic functions \(f, g:M\to B\) from some type \(M\) to a central H-space \(B\). Let \(\mu:B\to B\to B\) be the H-space multiplication. How does \(\mu\) act on paths? Suppose we have \(a, a', b, b':B\) and \(p:a=_B a', q:b=_B b'\). Then we also have homotopies \(\mu(p, -):\mu(a, -)=_{B\to B}\mu(a', -)\) and \(\mu(-,q):\mu(-,b)=_{B\to B}\mu(-,b').\) Since \(\mu(a, -):B=B\) is an (unpointed) equivalence of \(B\), and similarly for \(\mu(b, -)\) and so on, this data assembles into the following diagram of higher groupoid morphisms:

And so the two homotopies can be horizontally composed to give a path \[\mu(p,-)\star\mu(-,q): \mu(a, b)=\mu(a',b').\] Horizontal composition is given by \[\mu(p,-)\star\mu(-,q)\stackrel{\mathrm{def}}{=}(\mu(p,-)\cdot_r \mu(-,b))\cdot(\mu(a', -)\cdot_l\mu(-, q))\] where \[\mu(p,-)\cdot_r\mu(-,b):\mu(a,b)=\mu(a',b)\] and \[\mu(a',-)\cdot_l\mu(-,q):\mu(a',b)=\mu(a',b')\] are defined by path induction. See the HoTT book Theorem 2.1.6 on the Eckmann-Hilton argument (Univalent Foundations Program, 2013).

We can recognize the process of using whiskering to form horizontal composition in the Leibniz rule.

Quick aside: moving from infinitesimal calculus to finite groupoid algebra actually involves two changes. The first is the change from vectors to paths, forms to functions and so on. But it’s also the case that tangent vectors have just the one basepoint, whereas paths have two endpoints. You can see this play out in this example, where \(a\) and \(a'\) were distinct points (and \(b\) and \(b'\)).

The horizontal composition we build lives entirely in \(B\) and we didn’t make use of \(M\) yet. The Leibniz rule will be a pointwise version of what’s going on in \(B\). Denote by \(\mu\circ(f,g):M\to B\) the map which sends \(x\mapsto \mu(f(x),g(x))\).

4.4 Covering spaces

If \(G\) is a 0-truncated group such as \(\ensuremath{\mathbb{Z}}\) then the type of torsors (delooping) \(BG\) is 1-truncated. If \(f:M\to BG\) is a type family then \(\sum_{x:M}f(x)\) has fibers that are sets (\(G\)-torsors). So transport functions are set isomorphisms, and the transport of any contractible loop in \(M\) will be \(\ensuremath{\mathsf{refl}}\) (the identity) of the fiber, which is what we mean by flat.

4.5 Gauge transformations

A gauge transformation is a term inherited from physics. It’s an automorphism of a principal bundle \(P\to M\), meaning a homeomorphism of \(P\) that commutes with the projection to \(M\) and so acts on each fiber. It is further required to be equivariant under the action of the group \(G\), and so it’s very similar to the act of multiplying each fiber by a continuously varying element of \(G\).

In HoTT if the bundle is classified by \(f:M\to \mathcal{U}\) then an automorphism is a homotopy \(f\sim f\) and the group of gauge transformations is the loop space \(\Omega_f(M\to \mathcal{U})\).

Recall that torsors have a physical interpretation as a quantity without a specified unit, such as mass, length, or time. When we choose a base point in a torsor it becomes the standard torsor \(G\) acting on itself (for example, the additive real numbers). A physicist is looking for properties or laws that are independent of such a choice. In the 20th century physicists further wondered about choices of units that vary from point to point, and began searching for laws that are invariant under this much larger space of transformations. And so they and we are led to explore quotienting by the action of the group of gauge transformations, and in particular the space of connections “mod gauge.” In this scenario the base manifold \(M\) is spacetime, and a gauge transformation is a smoothly varying choice of gauge (units) at each point.

Gauge transformations act on connections. When we view connections as infinitesimal splittings of \(TP\) into vertical and horizontal sub-bundles, a gauge transformation that is constant in the neighborhood of a point will not change the splitting, it will just shift the fiber rigidly along itself, but one that is changing rapidly near a point will tilt the horizontal subspaces. So there are two effects: the effect of sliding along the fiber, and the effect of the rate of change of the gauge transformation. In classical geometry you’ll see formulas like this:

This theorem is a combination of Theorems 5.2.2 and 5.4.4 in the excellent recent book on gauge theory for mathematicians interested in physics by Mark Hamilton (Hamilton, 2017).

It’s not so important to fully understand this formula because we will re-explain it in HoTT terms in a moment. But notice that \(H^*A\) (the action of the gauge transformation on the connection 1-form) has contributions from two terms (both of which are vertical — connections always map onto the vertical bundle). The first is the adjoint action at the specific point \(x\). This is always what we expect when we shift the base point in a torsor and look at the resulting group (or in this case, the Lie algebra). The second term involves the Maurer-Cartan form, which is the derivative of subtraction in the group. It takes tangent vectors at \(g:G\) to a tangent vector at the identity (the Lie algebra, denoted \(\mathfrak{g}\)) by differentiating the action of multiplication by \(g^{-1}\). If we think in terms of finite-length paths, then imagine a path \(p:g=g'\) and the function \((g^{-1}\cdot -)\). The function will act on the path to give a path \(g^{-1}\cdot p:e=(g'\cdot g^{-1})\) that starts at the identity. So the Maurer-Cartan form shifts paths to start at the identity by subtracting off the start point. Our Maurer-Cartan term is the pullback of the Maurer-Cartan form by \(H\) which records how \(H\) acts infinitesimally, i.e. the contribution from the gauge transformation \(H\) that comes from the rapidity of change from point to point. This term will be large when \(H_U\) has a large derivative.

In HoTT the connection’s parallel transport is visible as the transport function, and the horizontal-vertical splitting is visible in the decomposition of paths in the sigma type (total space) into pairs of paths. What is the effect of applying a homotopy \(H:f\sim f\) on transport, and on splitting?

\(H\) is a family of fiber automorphisms: \(H:\prod_{a:M}f(a)=f(a)\) which we can assemble into an equivalence \(H':\sum_{a:M}f(a)=\sum_{a:M}f(a)\) that acts fiberwise. We want to compute the action of \(\ensuremath{\mathsf{ap}}(H')\) on the horizontal-vertical decomposition of paths from Theorem 2 by computing \(\omega\circ\ensuremath{\mathsf{ap}}(H')=\ensuremath{\mathrm{pr}}_2\circ\mathsf{split}\circ\ensuremath{\mathsf{ap}}(H')\).

Denote \(\sum_{a:M}f(a)\) by \(P\). We’ll adopt a convention of roman letters for structures in \(M\) and Greek for those upstairs in \(P\). Let \(p:a=_M b\) be a path in the base and let \(\pi:(a,\alpha)=_P (b,\beta)\) be a path in \(P\) over \(p\). Then \(\omega(\pi):\mathrm{tr}_p(\alpha)=\beta\).

Now let’s apply \(H\). We have \(\ensuremath{\mathsf{ap}}(H')(\pi):(a,H(a)(\alpha))=_P(b,H(b)(\beta))\) which is still a path over \(p\). Applying \(\omega\) we get \[\omega(\ensuremath{\mathsf{ap}}(H')(\pi)):\mathrm{tr}_p(H(a)(\alpha))=(H(b)(\beta))\]. Using the lemma below we can if we wish rewrite this as \[\omega(\ensuremath{\mathsf{ap}}(H')(\pi)):H(b)\left[\mathrm{tr}_p(\alpha)=\beta\right]\] which uses only \(H(b)\).

5 Gauss-Bonnet, Vector Fields, and the Poincaré-Hopf Theorem

1. Given Chern-Weil, we can hypothesize that Pfaffians and determinants can be made from the path groupoid structure.

2. Theorem 1: Gauss-Bonnet: curvature vs euler characteristic (2-d)

3. Theorem 2: Gauss-Bonnet-Chern (2n-d, Pfaffian/Euler class, 1944)

4. Theorem 3: Poincaré-Hopf: v.f. index is indep of v.f., and is euler characteristic via a specific v.f.

5. Non-theorem: v.f. on torus is the gradient of a Morse function. Bringing in Morse theory is future work.

6. use

   

5.1 Discrete vector fields

If \(M\) is a combinatorial manifold and we form a type family over \(M\) using \(\mathsf{link}\), \(\mathsf{xbox}\), or \(\mathsf{xdisk}\) then what we want to examine next is the dependent function type of this family, which are equivalent to sections of the sigma type. These sections will play the role of vector fields.

Introduce the notation \(P_f\stackrel{\mathrm{def}}{=}\sum_{x:M}f(x)\) and \(V_f\stackrel{\mathrm{def}}{=}\prod_{x:M}f(x)\). We will also refer to the 0-skeleton of \(M\) as \(M_0\) and the 1-skeleton as \(M_1\). We’ll be interested in \(P_\mathsf{xbox}\) (the xbox bundle over \(M\)) and \(V_\mathsf{xbox}\) (the type of sections thereof). Since \(M\) is a HIT, then to specify a map \(X:V_\mathsf{xbox}\) we need to supply a point in each fiber, and for each path \(p:x=_M y\) in \(M\) a path \(X(p):p_* X(x)=_{\mathsf{xbox}(y)} X(y)\).

Since \(\mathsf{xbox}\) is defined using the neighboring points and paths of \(M\), we can exponentiate \(P_\mathsf{xbox}\), forming a map \(\exp:P_\mathsf{xbox}\to M\): just map the xboxes back onto where they came from in \(M\). This is the finite version of exponentiating a tangent space. It’s very different from the projection map \(\ensuremath{\mathrm{pr}}_1\) since it spreads the fibers out along \(M\).

Hence we also have a map \(\exp\circ X:M\to M\) which is in general not an equivalence but can be. We can think of it as the flow given by \(X\), the analogue of integrating a vector field for some finite time.

5.2 The index of a fixed point

Suppose that \(x\) satisfies \(X(x)=\ensuremath{\mathsf{refl}}_x\), and so \(\exp\circ X(x)=x\) and \(x\) is a fixed point of the flow. Combinatorial manifolds are finite and decidable so this equation makes sense. In such a situation we can form a map \(\mathrm{tr}\circ X\circ\exp:\mathsf{link}(x)\to\mathsf{link}(x).\) Starting with a point in \(\mathsf{link}(x)\) we exponentiate to the actual neighboring point in \(M\), take the value of \(X\) on this other point (some neighbor of this neighbor, possibly \(x\)), and transport that back to \(\mathsf{link}(x)\). Such a map has a degree, and that degree is a discrete version of what is called the index of the vector field at a fixed point.

To prove the Gauss-Bonnet theorem one needs a notion of Euler characteristic and a notion of curvature. To prove the Poincaré-Hopf theorem, one needs a notion of the index of a vector field, and again, a notion of curvature. To prove both and relate them it helps to equate the Euler characteristic to the index of a special vector field.

The following proofs follow the explanations given in (Needham, 2021). But as we might hope, the proofs can be brought into HoTT in a much abbreviated form!

Note that \(X\) is a pointing of all the fibers. So a second vector field can be lifted to the classifying map to pointed types, which is contractible. That’s really all that’s going on in these classical proofs!

---

1. https://mathoverflow.net/questions/201944/topological-n-manifolds-have-the-homotopy-type-of-n-dimensional-cw-complexes↩︎

2. I’m picking and choosing where to tell the story fully twice (see the next section) and where to simply look for motivation.↩︎