\(\newcommand{\textesh}{∫}\) \(\newcommand{\ensuremath}{}\) \(\newcommand{\raisebox}[2]{}\)

Abstract

Type families on higher inductive types such as pushouts can capture homotopical properties of differential geometric constructions including connections, curvature, and vector fields. We define a class of pushouts based on simplicial complexes, then define principal bundles, connections, and curvature on these. We provide an example of a tangent bundle but do not prove when these must exist. We define vector fields, and the index of a vector field. Our main result is a theorem relating total curvature and total index, a key step to proving the Gauss-Bonnet theorem and the Poincaré-Hopf theorem, but without an existing definition of Euler characteristic to compare them to. We draw inspiration in part from the young field of discrete differential geometry, and in part from the original classical proofs, which often make use of triangulations and other discrete arguments.

This thesis is dedicated to John Baez, Sean M. Carroll, Sabine Hossenfelder, and other communicators who are carrying the torch of science forward in the spirit of my hero Carl Sagan. I have followed you all for many years, and you have inspired me to continue my studies alongside my career. Thank you.

1 Overview

“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[1]

We will define

• principal bundles in Section 2,

• simplicial complexes, and homotopical realizations of these in Section 3,

• tangent bundles and vector fields in Section 5,

and observe emerging from those definitions the presence of

• connections and curvature in Section 4,

• the index of a vector field in Section 6,

and then define in Section 6, for a 2-dimensional simplicial complex

• the total curvature, as in the Gauss-Bonnet theorem

• the total index of a vector field, as in the Poincaré-Hopf theorem,

• and prove the equality of these to each other when the complex is oriented (Theorem 52).

We will build up an example of all of these structures on an octahedron model of the sphere. We will not, however, be supplying a separate definition of Euler characteristic so as to truly reproduce the Gauss-Bonnet and Poincaré-Hopf theorems.

Once we have defined homotopical realizations of simplicial complexes in Section 3, we will focus on dimensions 1 and 2. In dimension 1 we define polygons, which we prove are equivalent to \(S^1\), and so give terms in the type \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\stackrel{\mathrm{def}}{=}\sum_{A:\mathcal{U}}||A\simeq S^1||_1\). We can call this component of the universe “mere circles.” In dimension 2 we will focus on a subset of complexes where the neighboring vertices and edges of each vertex (the vertex’s “link”) form a polygon. The homotopical realization \(\ensuremath{\mathbb{M}}\) of such a complex then has a map \(\mathop{\mathrm{\mathsf{link}}}\) from each vertex to a homotopical polygon, i.e. a map to \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\). We do not know under what conditions this map necessarily extends to the higher cells of the realization.

Given a map \(\ensuremath{\mathbb{M}}\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) we can form the pullback

to obtain a bundle of mere circles. We will discuss when such a map factors through a map \(\ensuremath{\mathbb{M}}\to \mathrm{K}(\ensuremath{\mathbb{Z}},2)\), and hence when it is in fact a principal fibration.

Then in Section 4 we will name various elements of the above construction, indicating their relationship to classical definitions.

In Section 5 we will define vector fields, which require a tangent bundle. We will introduce a method for decomposing a vector field along a concatenation of paths.

Finally, in Section 6 we will define a method for visiting all the faces of a manifold in order to form “totals” of local objects. We will examine the total curvature and the total index and prove that they are equal. Our proof tracks very closely with the classical proof of Hopf[2], presented in detail in Needham[3]. In their case they can go on to prove that these values are both equal to the Euler characteristic, but we would need an independent definition to prove agreement with, which we do not currently have.

2 Torsors and principal bundles

2.1 Torsors

We will review some definitions and facts, drawing on the excellent resource [4].

A \(G\)-equivariant map from \((X,\phi)\) to \((Y,\psi)\) is a function \(f:X\to Y\) such that \(f(\phi(g,x))=\psi(g,f(x))\). Denote the type of \(G\)-equivariant maps by \(X\to_G Y\).

These lemmas lead to

We call types \(X\) such that \(\Omega X\simeq_* G\) a delooping of \(G\). So the type of \(G\)-torsors \(BG\) is a delooping of \(G\).

Suppose we have a basepoint \(b:BG\). Following [4] Section 4.3, another term \(X:BG\) is a torsor for the higher group \(\Omega_b(BG)\stackrel{\mathrm{def}}{=}(b=_{BG} b)\). In particular there is an action \(\alpha:(b=_{BG}b)\times X\to X\), and an equivalence \((\alpha, \ensuremath{\mathrm{pr}}_2) : (b=_{BG}b)\times X\stackrel{\sim}{\to}(X\times X)\).

If \(G\) is abelian then \(\mathrm{K}(G,1)\) can be delooped, and in fact can be delooped in a unique way, any number of times. In the next section we will learn how to proceed from a construction of \(\mathrm{K}(G, 1)\) to obtain \(\mathrm{K}(G, n)\).

2.2 Bundles of Eilenberg-Mac Lane spaces

To construct maps into \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) we will follow Scoccola[5]. When can a map into a connected component of the universe be factored through an Eilenberg-Mac Lane space?

Scoccola constructs a map by composing

• suspension \(\Sigma:\mathrm{EM}(G,n)\to\mathrm{EM}_{\bullet\bullet}(G,n)\) (see [6] §6.5), which maps into types with two points (denoted by the bullets),

• \((n+1)\)-truncation (see [6] §7.3),

• forgetting a point \(F_\bullet:\mathrm{EM}_{\bullet\bullet}(G,n)\to \mathrm{EM}_{\bullet}(G,n)\),

to form the composition \[\mathrm{EM}(G,n)\xrightarrow[]{||\Sigma||_{n+1}} \mathrm{EM}_{\bullet\bullet}(G,n+1)\xrightarrow[]{F_\bullet}\mathrm{EM_{\bullet}}(G,n+1)\] to types with two points (north and south), then to pointed types (by forgetting the south point).

The above theory of classifying spaces should be relevant to any future project to bring the study of gauge theory into homotopy type theory. In this note we will be focused on the special case \(G=\ensuremath{\mathbb{Z}}\) and \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) and \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\).

2.3 Pathovers

Here we will recall basic facts from homotopy type theory. See for example [6] or [9]. Suppose we have \(T:M\to\mathcal{U}\) and \(P\stackrel{\mathrm{def}}{=}\sum_{x:M}Tx\). Recall that if \(p:a=_M b\) then \(T\) acts on \(p\) with what’s called the action on paths, denoted \(\ensuremath{\mathsf{ap}}(T)(p):Ta=Tb\) ([6] §2.2). This is a path in the codomain \(\mathcal{U}\) of \(T\). Type theory also provides a function called transport, denoted \(\mathsf{tr}(p):Ta\to Tb\) ([6] §2.3) which acts on the fibers of \(P\). \(\mathsf{tr}(p)\) is a function, acting on the terms of the types \(Ta\) and \(Tb\), and univalence tells us this is the isomorphism corresponding to \(\ensuremath{\mathsf{ap}}(T)(p)\).

Type theory also tells us that paths in \(P\) are given by pairs of paths: a path \(p:a=_M b\) in the base, and a pathover \(\pi:\mathsf{tr}(p)(\alpha)=_{Tb}\beta\) between \(\alpha:Ta\) and \(\beta:Tb\) in the fibers ([6] §2.7). We can’t directly compare \(\alpha\) and \(\beta\) since they are of different types, so we apply transport to one of them. We say \(\pi\) lies over \(p\). See Figure 1.

Given functions \(\phi,\psi:A\to B\) between two arbitrary types we can form a type family of paths \(\alpha:A\to\mathcal{U}\) by \(\alpha(a)\stackrel{\mathrm{def}}{=}(\phi(a)=_B\psi(a))\). Transport in this family is given by concatenation as follows (see Figure 2), where \(p:a=_A a'\) and \(q:\phi(a)=\psi(a)\) ([6] Theorem 2.11.3): \[\mathsf{tr}(p)(q) = \phi(p)^{-1}\cdot q\cdot \psi(p)\] which gives a path in \(\phi(a')=\psi(a')\) by connecting dots between the terms \(\phi(a'), \phi(a), \psi(a), \psi(a')\). This relates a would-be homotopy \(\phi\sim\psi\) specified at a single point, to a point at the end of a path. We will use this to help construct such homotopies.

Finally, recall that in the presence of a section \(X:M\to P\) there is a dependent generalization of \(\ensuremath{\mathsf{ap}}\) called \(\mathsf{apd}\): \(\mathsf{apd}(X)(p):\mathsf{tr}(p)(X(a))=X(b)\) which is a pathover between the two values of the section over the basepoints of the path \(p\) ([6] Lemma 2.3.4).

3 Discrete manifolds

We will remind ourselves of the definition of a classical simplicial complex, in sets. Then we will create a type that realizes the data of a complex, using pushouts.

3.1 Abstract simplicial complexes

We can imagine constructing a simplicial complex dimension by dimension.

Note that \(P(n)_{(n-1)}\) has \(n+1\) elements. For example, \(P(2)_1\) consists of the three 2-element subsets of \(\{0, 1, 2\}\).

Given \(M=[M_0,\ldots,M_n]\) and \(k\leq n\), a face \(f_k:M_k\) is the union of \((k+1)\) faces in \(M_{k-1}\), and so the \(k\)-skeleton is obtained from the \((k-1)\)-skeleton by forming the following pushout of sets:
where the vertical “attach” map \(a_k(f_k, -)\) picks out the \(k+1\) subsets of \(f_k\).

The link is easier to understand as all the neighboring vertices of \(v\) and the subcomplex containing these. See for example Figure 3.

3.2 Higher inductive realizations

We will realize a simplicial complex as a higher inductive type by forming a sequence of pushouts. We will work upward by dimension so as to define a standard sphere that we need in the next dimension.

where \(a_k\) is the attachment data of the edges in \(M_1\), as in diagram [eq:attach]. The right vertical map \(*_{\ensuremath{\mathbb{M}}_1}\) provides a hub point for each edge, and the homotopy \(h_1\) provides the spokes that connect the hub to the vertices.

where \(\mathbb{A}_1\) is such that this additional diagram commutes

In this diagram \(a_1\) is the simplicial attaching map from [eq:attach], and \(*_{\mathbb{M}_{\leq 1}}\) simply gathers the hub maps from \(M_0\) and \(M_1\) into \(\ensuremath{\mathbb{M}}_1\). The commutativity then says that \(\mathbb{A}_1\) reflects the attachment data.

where \(\mathbb{A}_n\) is such that the following commutes

Gathering some of the inductive process into one definition, we have

3.3 Polygons

The 1-type \(\partial\Delta^{2}\) has three vertices. In order to define the link of an arbitrary realization, we will need to have \(n\)-gons for \(n\geq 3\). For example in Figure 3 the link is a 6-gon. And since \(S^1\) could be called a 1-gon, we will also define a 1-gon, and for completeness a 2-gon.

We also have two special polygons:

The homotopical realization \([\![{R}]\!]\) has a path to the identity:

We wrote the homotopy \(H_R(x)\) as starting at \(x\) because it feels like a record of a time-based process of applying \(R\). We will rely on this convention when we define flatness.

3.4 Surfaces

We will eventually focus on 2-dimensional simplicial complexes in this note, and our running example which begins in the next section is 2-dimensional. We have a simple way to define an orientation in this dimension, which we provide here. We will touch on the relationship between this classical definition and the definition of our HoTT classifying space when we discuss vector fields in Section 5.1.

3.5 The octahedron model of the sphere

We will create our first combinatorial surface, an octahedron. We will not prove that this type is equivalent to the sphere. In \(\mathsf{SimCom_n}\) the combinatorial data of the faces can be represented with a Hasse diagram, which shows the poset of inclusions in a graded manner, with a special top and bottom element. We give an octahedron in Figure 5. The names of the vertices are short for white, yellow, blue, red, green, and orange, the colors of the faces of a Rubik’s cube. The octahedron is the dual of the cube, with each vertex corresponding to a face.

We can realize \(O_0\to O_1\to O\) as a cellular type denoted \(\ensuremath{\mathbb{O}}_0\to \ensuremath{\mathbb{O}}_1\to \ensuremath{\mathbb{O}}\).

4 Bundles, connections, and curvature

Bundles are simply maps into the universe. By using the extra cellular structure and the even more detailed combinatorial structure of realizations, we can identify inside of HoTT some additional classical definitions.

4.1 Definitions

Having the cellular structure allows us to define bundles and connections.

then we say

• The map \(f_k\) is a \(k\)-bundle on \(\ensuremath{\mathbb{M}}\).

• The pair given by the map \(f_k\) and the proof \(f_k\circ \imath_{k-1}=f_{k-1}\) that \(f_k\) extends \(f_{k-1}\) is called a \(k\)-connection on the \((k-1)\)-bundle \(f_{k-1}\).

Having the additional structure of a simplicial complex allows us to define curvature, which is a local concept.

the outer square of which restricts on each face to the diagram

then we say the filler \(\flat_k\) is called a flatness structure for the face \(m_k\), and its ending path is called curvature at the face \(m_k\).

Although all the pushout diagrams are introducing hub points for each edge and face, in practice we will ignore those. But in the case of flatness, which we will use extensively, we should clarify what its type is when we are ignoring hubs. If we have a face \(F\) with vertices \(v_1, v_2, v_3\) and paths \(e_{ij}:v_i=v_j\) that are realizations of edges, and the loop \(\ell_F\stackrel{\mathrm{def}}{=}e_{12}\cdot e_{23}\cdot e_{31}\) then we will write \(\flat(\ell_F):\ensuremath{\text{id}}_{f_0(v_1)}=f_1(\ell_F)\) for a 2-path filling this loop.

The definitions can be digested to give

On a 2-dimensional cellular type \(\ensuremath{\mathbb{M}}\stackrel{\mathrm{def}}{=}\ensuremath{\mathbb{M}}_0\to\ensuremath{\mathbb{M}}_1\to\ensuremath{\mathbb{M}}_2\) the terminology works out as follows: a 0-bundle on \(\ensuremath{\mathbb{M}}\) is a map \(T_0:\ensuremath{\mathbb{M}}_0\to\mathcal{U}\). A 1-connection on \(T_0\) is an extension \(T_1:\ensuremath{\mathbb{M}}_1\to\mathcal{U}\). A 2-connection on \(T_1\) is an extension \(T_2:\ensuremath{\mathbb{M}}_2\to\mathcal{U}\). Classically, a 1-extension that extends to a 2-connection is called flat.

4.2 Flat connections as local trivializations

This section can be viewed as an extended remark. The observation we want to make is that the data of a 2-bundle on a realization of a 2-dimensional simplicial complex is related to the construction of local trivializations: the fiber at one vertex can be extended throughout a single face coherently, using the connection (the extension of the classifying map to the edges) to specify isomorphisms with the fibers at the other points, and the higher connections to establish commutativity between these.

We introduce a notation more suitable for the algebra of charts and overlaps: denote the fiber at \(v_i\) by \(T_i\) and denote transport along \(e_{ij}:v_i=v_j\) by \(T_{ji}:T_i\to T_j\). The indices are ordered from right to left, which is compatible with function composition notation. Denote the inverse function by swapping indices: \(T_{ij}\stackrel{\mathrm{def}}{=}T_{ji}^{-1}\). Assume we have some fixed isomorphism \(T_i=S^1\), and to avoid composing everything with this function we will assume it is \(\ensuremath{\text{id}}\). In the diagram below we see the data arranged so that our bundles fibers are on the left, and the fiber of a trivial bundle is on the right.

The two middle squares commute definitionally. Call these two squares together the back face. The left triangle is filled by the flatness structure on the face, and the right triangular filler is trivial. There is also a filler needed for the front, i.e. the outer square. This requires proving that \(T_{ki}T_{ij}T_{jk}=\ensuremath{\text{id}}\), which is supplied by the flatness structure. There is also a 3-cell filling the interior of this prism, mapping the back face plus the left triangle filler to the front face plus the right triangle filler. These two faces both consist of one or two identities concatenated with the flatness structure, and so the 3-cell is definitional.

This relationship between flatness structure and local triviality of a chart can be compared to the classical result that on a paracompact, simply connected manifold (such as a single chart), a connection on a principal bundle is flat if and only if the bundle is trivial. See for example [12] Corollary 9.2.

4.3 The tangent bundle of the sphere

We will build up a map \(T\) out of \(\ensuremath{\mathbb{O}}_0\to\ensuremath{\mathbb{O}}_1\to\ensuremath{\mathbb{O}}\) which is meant to be a model of the tangent bundle of the sphere. The link function will serve as our approximation to the tangent space. Taking the link of a vertex gives us a map from vertices to polygons, so the codomain is \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\).

If \(\{b, r, g, o\}\) are four vertices in \(\ensuremath{\mathbb{O}}\), the notation \([\![{brgo}]\!]\) refers to the 4-gon spanned by these four vertices and the edges of \(\ensuremath{\mathbb{O}}\) that connect them to each other.

To extend \(T_0\) to a function \(T_1\) on the 1-skeleton we have some freedom. We will do something motivated by the figures we have been drawing of an octahedron embedded in 3-dimensional space. We will imagine how \(T_1\) changes as we slide from point to point in the embedding shown in the figures. 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\).

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 6 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, which we saw in Definition 25 where it is called \([\![{R}]\!]\).

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)\). Here there is no additional freedom.

4.4 Existence of connections

How confident can we be that we can always define a connection on the realization of an arbitrary simplicial complex? Two things make the octahedron example special: the link is a 4-gon at every vertex (as opposed to having a variable number of vertices), and every transport map extends to a rotation of the entire octahedron in 3-dimensional space. This imposed a coherence on the interactions of all the choices we made for the connection, which we can worry may not exist for more complex combinatorial data.

We know as a fact outside of HoTT that any combinatorial surface that has been realized as a triangulated surface embedded in 3-dimensional euclidean space can inherit the parallel transport entailed in the embedding. We could then approximate that data to arbitrary precision with enough subdivision of the fibers of \(T\).

What would a proof inside of HoTT look like? We will leave this as an open question.

5 Vector fields

5.1 Definition

Vector fields are sections of the tangent bundle of a manifold. We do not have a general theory of tangent bundles, even for 2-dimensional cellular types, since we cannot yet prove that connections always exist on the 1-skeleton (see Section 4.4). But if \(\ensuremath{\mathbb{M}}\stackrel{\mathrm{def}}{=}\ensuremath{\mathbb{M}}_0\to\ensuremath{\mathbb{M}}_1\to\ensuremath{\mathbb{M}}_2\) is a cellular type, and given an extension \(T:\ensuremath{\mathbb{M}}\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) of the \(\mathop{\mathrm{\mathsf{link}}}\) function, we can consider the type of sections \(\prod_{x:\ensuremath{\mathbb{M}}_1}T_1(x)\).

In this section and for the remainder of the note, we will assume that the bundle is principal, that is that the bundle is in fact a map \(T:\ensuremath{\mathbb{M}}\to\mathrm{K}(\ensuremath{\mathbb{Z}},2)\), the type of \(S^1\)-torsors. This assumption is in principle not needed if \(M\) is equipped with an orientation \(\mathscr{O}\), but we are omitting a proof that such an \(\mathscr{O}\) provides a factorization of \(T\).

On the 0-skeleton \(X\) picks a point in each link, i.e. a neighbor of each vertex. On a path \(p:x=_\ensuremath{\mathbb{M}}y\), \(X\) assigns a dependent path over \(p\), which as we know is a term \(\pi:\mathsf{tr}(p)(X(x))=_{T y} X(y)\). We are very interested in working with the concatenation operation on dependent paths, which we call swirling.

5.2 Swirling of dependent paths

Consider the vertex \(v_1:\ensuremath{\mathbb{M}}\), a face \(F\) containing vertices \(v_1, v_2, v_3\), and the boundary path \(\ell\stackrel{\mathrm{def}}{=}e_{12}\cdot e_{23} \cdot e_{31}\). As we did in Section 4.2, denote \(T(v_i)\) by \(T_i\) and \(T(e_{ij})\) by \(T_{ji}\). The indices are swapped so that we can have expressions that respect function-composition order, such as \(T_{32}T_{21}(X_1):T_3\). We retain the opposite convention (which we can call path-concatenation order) for the vector field, e.g. \(X_{ij}\) which is a path in \(T_j\), as these are paths. Figure 7 shows in tabular form how we concatenate the dependent paths over \(e_{12}\cdot e_{23}\cdot e_{31}\). Figure 8 shows visually a possible example.

As we traverse an edge, say \(e_{12}\), we get a path in \(T_2\) which is the image of \(e_{12}\) under \(X\), denoted \(X_{12}\). As we traverse an additional edge, \(X_{12}\) is simply mapped to the next vertex by transport. The image is carried first to \(T_{32}(X_{12})\) then to \(T_{13}\circ T_{32}(X_{12})\).

We wish to simplify expressions such as \(T_{13}T_{32}X_{12}\cdot T_{13}X_{23}\cdot X_{31}\), which take place in a particular fiber (\(T_1\) in this case), and which depend on arranging for the endpoint of one segment to agree with the start of another. The simplification will empower us to easily perform calculations over the whole manifold, and to prove Theorem 52.

First we will choose a specific group that acts on all the fibers of \(T\). Recall from Section 2.1 that given some basepoint \(b:\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) and a type \(T_i:\mathrm{K}(\ensuremath{\mathbb{Z}},2)\), the group \(b=_{\mathrm{K}(\ensuremath{\mathbb{Z}},2)}b\) acts on \(T_i\). Suppose we have a master basepoint \(m:\ensuremath{\mathbb{M}}\), and choose \(T_m:\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) as the basepoint, so that all the fibers of \(T\) are now equipped with an action of \(T_m=_{\mathrm{K}(\ensuremath{\mathbb{Z}},2)}T_m\).

We will give this group a nickname for brevity. Recall the bundle \(\mathop{\mathrm{Aut}}T\) from Section 54.

We need to derive two operations from \(\mathscr{G}(m)\).

Each fiber \(T_i\) is pointed by \(X_i\), so we can define the map \(T_i\xrightarrow[]{-X_i}\mathscr{G}(m)\), and then give a name to the special term \(T_{ij}X_j - X_i\).

We can obtain a path in \(\mathscr{G}(m)\) from a dependent path by again subtracting the basepoint: \[\begin{aligned} \sigma_{ij}\stackrel{\mathrm{def}}{=}X_{ij}-X_j&:T_{ji}X_i-X_j=_{\mathscr{G}(m)}0 \\ &:\rho_{ji}=_{\mathscr{G}(m)}0. \end{aligned}\] Notice the reversal in indices between \(\sigma_{ij}\) and \(\rho_{ji}\), which reflects our opposite conventions for \(X_{ij}\) which we view as a path, and \(T_{ji}\) which we view as a function.

The key technical lemma is the following. Recall that dependent functions such as our vector field \(X\) send \(\ensuremath{\mathsf{refl}}_{v_i}\) to \(\ensuremath{\mathsf{refl}}_{X_i}\) (by path induction, see for example [6] Lemma 2.3.4). As stated, this can only be used when we have a path that is \(\ensuremath{\mathsf{refl}}\), for example when traversing \(e_{ij}\cdot e_{ji}\), i.e. an edge followed by its inverse. We will use subtraction together with the operation of Lemma 39 to lift this requirement, by obtaining paths in \(\mathscr{G}(m)\) that can be added without needing to be concatenated directly.

5.3 An example vector field on the sphere

Figure 9 shows an example of a vector field \(X_\ensuremath{\mathbb{O}}^s\) (\(s\) for “spin”) on the octahedron \(\ensuremath{\mathbb{O}}\). The picture can really only convey the value of \(X_\ensuremath{\mathbb{O}}^s\) on vertices, which it does by displaying it as an arrow on the surface itself, for example as an arrow from \(w\) to \(r\), instead of trying to draw the fiber at \(w\) which is where \(r:\mathop{\mathrm{\mathsf{link}}}(w)\) actually lives. But hopefully there is a net gain in clarity.

We will define \(X_\ensuremath{\mathbb{O}}^s\) on edges, and then compute the swirling around each face. These calculations will then be cited later when we discuss the total swirling on a realization. Here is all the data for \(X_\ensuremath{\mathbb{O}}^s\), which includes values when traversing an edge in either direction: \[\begin{array}{|c|c|} \hline \multicolumn{2}{|c|}{X_\ensuremath{\mathbb{O}}^s\text{ on vertices}} \\ \hline v & X_\ensuremath{\mathbb{O}}^s(v) \\ \hline w & r \\ r & g \\ g & w \\ \hline o & b \\ b & y \\ y & o \\ \hline \end{array}\, \begin{array}{|c|c|} \hline \multicolumn{2}{|c|}{X_\ensuremath{\mathbb{O}}^s\text{ on north edges}} \\ \hline e & X_\ensuremath{\mathbb{O}}^s(e) \\ \hline wr & yg \\ wg & rw \\ wo & wb \\ wb & ry \\ \hline rw & gr \\ gw & br \\ ow & br \\ bw & br \\ \hline \end{array}\, \begin{array}{|c|c|} \hline \multicolumn{2}{|c|}{X_\ensuremath{\mathbb{O}}^s\text{ on south edges}} \\ \hline e & X_\ensuremath{\mathbb{O}}^s(e) \\ \hline yr & yg \\ yg & ow \\ yo & wb \\ yb & oy \\ \hline ry & go \\ gy & go \\ oy & bo \\ by & go \\ \hline \end{array}\, \begin{array}{|c|c|} \hline \multicolumn{2}{|c|}{X_\ensuremath{\mathbb{O}}^s\text{ on equator edges}} \\ \hline e & X_\ensuremath{\mathbb{O}}^s(e) \\ \hline br & yg \\ rg & ow \\ go & wb \\ ob & ry \\ \hline rb & ry \\ gr & wg \\ og & ow \\ bo & yb \\ \hline \end{array}\] How do we read the tables for the edges? For example, \(X_\ensuremath{\mathbb{O}}^s(wr)\) should be a term of type \(\mathsf{tr}(wr)X_\ensuremath{\mathbb{O}}^s(w)=_{Tr}X_\ensuremath{\mathbb{O}}^s(r)\). Looking up \(X_\ensuremath{\mathbb{O}}^s\) on vertices means this type is \(\mathsf{tr}(wr)(r)=_{Tr}g\), and looking up \(\mathsf{tr}\) in Definition 33 means the type is \(y=_{Tr}g\). We can choose \(X_\ensuremath{\mathbb{O}}^s(wr)\) to be any path from \(y\) to \(g\) and we choose the short path \(yg\).

Next we want to compute \(X_\ensuremath{\mathbb{O}}^s\) around a face. We will do this for the four north faces only. In this calculation we will denote paths by listing the vertices, so \(rg\cdot gw\) is denoted \(rgw\) and \(wrgw\) is a loop at \(w\). \[\begin{aligned} X_\ensuremath{\mathbb{O}}^s(wrgw) &= \mathsf{tr}(rgw)X_\ensuremath{\mathbb{O}}^s(wr)\cdot\mathsf{tr}(gw)X_\ensuremath{\mathbb{O}}^s(rg)\cdot X_\ensuremath{\mathbb{O}}^s(gw)\\ &= \mathsf{tr}(rgw)(yg)\cdot\mathsf{tr}(gw)(ow)\cdot(br)\\ &= (yg\mapsto yo\mapsto \boxed{go})\cdot(ow\mapsto \boxed{ob})\cdot \boxed{br}\\ &= \boxed{gobr} \end{aligned}\] To help follow along, in the third line we are showing the results of intermediate transports, and put a box around the result. The other three faces give \[\begin{aligned} X_\ensuremath{\mathbb{O}}^s(wgow) &= \mathsf{tr}(gow)X_\ensuremath{\mathbb{O}}^s(wg)\cdot\mathsf{tr}(ow)X_\ensuremath{\mathbb{O}}^s(go)\cdot X_\ensuremath{\mathbb{O}}^s(ow)\\ &= \mathsf{tr}(gow)(rw)\cdot\mathsf{tr}(ow)(wb)\cdot(br)\\ &= (rw\mapsto gw\mapsto \boxed{gr})\cdot(wb\mapsto \boxed{rb})\cdot \boxed{br}\\ &= \boxed{gr} \end{aligned}\]

\[\begin{aligned} X_\ensuremath{\mathbb{O}}^s(wobw) &= \mathsf{tr}(obw)X_\ensuremath{\mathbb{O}}^s(wo)\cdot\mathsf{tr}(bw)X_\ensuremath{\mathbb{O}}^s(ob)\cdot X_\ensuremath{\mathbb{O}}^s(bw)\\ &= \mathsf{tr}(obw)(wb)\cdot\mathsf{tr}(bw)(ry)\cdot(br)\\ &= (wb\mapsto wr\mapsto \boxed{gr})\cdot(ry\mapsto \boxed{rb})\cdot \boxed{br}\\ &= \boxed{gr} \end{aligned}\]

\[\begin{aligned} X_\ensuremath{\mathbb{O}}^s(wbrw) &= \mathsf{tr}(brw)X_\ensuremath{\mathbb{O}}^s(wb)\cdot\mathsf{tr}(rw)X_\ensuremath{\mathbb{O}}^s(br)\cdot X_\ensuremath{\mathbb{O}}^s(rw)\\ &= \mathsf{tr}(brw)(ry)\cdot\mathsf{tr}(rw)(yg)\cdot(gr)\\ &= (ry\mapsto gy\mapsto \boxed{gr})\cdot(yg\mapsto \boxed{rg})\cdot \boxed{gr}\\ &= \boxed{gr} \end{aligned}\]

So we have these four edges in \(Tw\), which is pointed at \(X_\ensuremath{\mathbb{O}}^s(w)=r\): \(gobr, gr, gr, gr\). Lemma 39 tells us we can add these by transporting them so as to be concatenate-able. This gives \(gobr\cdot rb\cdot bo\cdot og=\ensuremath{\mathsf{refl}}_g\) in \(Tw\). So the total swirling in the northern hemisphere is trivial. We leave the computation in the southern hemisphere as an exercise, but it is very symmetrical with the northern hemisphere, and gives \(\ensuremath{\mathsf{refl}}_o\) in \(Ty\).

6 The total construction

We will place holonomy, flatness, and vector fields on the same footing, and combine them. We will prove a relation between the total curvature of a tangent bundle, and total index of a vector field. This is the key step in the simultaneous proof of the Gauss-Bonnet theorem and the Poincaré-Hopf theorem, lacking only the relationship with the Euler characteristic.

6.1 Index of the vector field on a face

The index of a vector field is derived from other data that we have. Consider a 2-dimensional simplicial complex \(M\) and its 2-dimensional realization \(\ensuremath{\mathbb{M}}=\ensuremath{\mathbb{M}}_0\to\ensuremath{\mathbb{M}}_1\to\ensuremath{\mathbb{M}}_2\), and a principal circle bundle \(T:\ensuremath{\mathbb{M}}\to\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) extending \(\mathop{\mathrm{\mathsf{link}}}\). Consider a face \(F:M_2\), with \(m:\ensuremath{\mathbb{M}}\) a vertex of \(F\) and \(\partial F:\partial\Delta^2\to\ensuremath{\mathbb{M}}\) the boundary loop of the face. We have accumulated the following constructions: \[\begin{aligned} \mathsf{tr}_F&\stackrel{\mathrm{def}}{=}\mathsf{tr}(\partial F)&&:Tm=Tm&&\text{holonomy}\\ \flat_F&\stackrel{\mathrm{def}}{=}\flat(\partial F)&&:\ensuremath{\text{id}}=_{Tm=Tm}\mathsf{tr}(\partial F)&&\text{flatness}\\ X_F&\stackrel{\mathrm{def}}{=}X(\partial F)&&:\mathsf{tr}(\partial F)(X(m))=_{Tm}X(m)&&\text{swirling.}\\ \end{aligned}\] The flatness is a path in automorphisms of \(Tm\) whereas the swirling is a path in \(Tm\), but we can view the latter as a path in automorphisms as well:

Now \(\sigma^X_F\stackrel{\mathrm{def}}{=}\mathrm{ev}(X(m))^{-1}(X_F)\) is the automorphism of \(Tm\) that corresponds to the swirling. We now have: \[\begin{aligned} \mathsf{tr}_F&:Tm=Tm&&\text{holonomy on }F\\ \flat_F&:\ensuremath{\text{id}}=_{Tm=Tm}\mathsf{tr}_F&&\text{flatness on }F\\ \sigma^X_F&:\mathsf{tr}_F=_{Tm=Tm}\ensuremath{\text{id}}&&\text{swirling on }F.\\ \end{aligned}\] These last two can be concatenated to make a loop. We can then obtain an integer by noting that the automorphisms are a circle \(\Omega_{Tm}(\mathrm{K}(\ensuremath{\mathbb{Z}},2))\simeq S^1\), and recalling the well known fact that loops in the circle are integers: \(\Omega(S^1,\ensuremath{\mathsf{base}})\simeq\ensuremath{\mathbb{Z}}\) (e.g. [6] Corollary 8.1.10).

We now have the final list of ingredients at a single face: \[\label{eq:face_elements} \begin{aligned} \mathsf{tr}_F&:Tm=Tm&&\text{holonomy on }F\\ \flat_F&:\ensuremath{\text{id}}=_{Tm=Tm}\mathsf{tr}_F&&\text{flatness on }F\\ \sigma^X_F&:\mathsf{tr}_F=_{Tm=Tm}\ensuremath{\text{id}}&&\text{swirling on }F\\ I^X_F&:\ensuremath{\mathbb{Z}}&&\text{index on }F. \end{aligned}\]

6.2 Total flatness, total index

Now we wish to compute a sum over all faces of the data. To do this we need all of our definitions plus two new ones that help us organize the sum and make a key assumption about cancellation of edges.

Some of the assumptions in these definitions are unnecessary because they are entailed in other assumptions, but we will not attempt to eliminate them.

For the rest of the note we will equip our simplicial complex \(M\) with an orientation \(\mathscr{O}\), and our realization \(\ensuremath{\mathbb{M}}\) with an oriented set of pointed faces.

We have seen in Lemma 39 how to perform the required sum.

The assumption about edges appearing twice, once in each direction, together with Lemma 41 proves the following

And making use of Lemma 42 we obtain

And finally, if we give the loop map \(\Omega\) the nickname “winding number”:

6.3 Calculation on the sphere

The flatness structures on the eight faces of \(\ensuremath{\mathbb{O}}\) in Definition 34 are all identical and equal to \(H_R:\ensuremath{\text{id}}=_{\mathbb{C}(4)=\mathbb{C}(4)}R\) on a fixed 4-gon. Composing \(R\) 8 times gives the identity, as required by Proposition 49. Adding the flatness structures gives \(8H_R:\ensuremath{\text{id}}=_{\mathbb{C}(4)=\mathbb{C}(4)}\ensuremath{\text{id}}\) whose winding number is 2.

Next we want to compute the total index of the vector field \(X_\ensuremath{\mathbb{O}}^s\) from Section 5.3. We saw that on the four faces in the northern hemisphere the swirling gave us these four paths in \(Tw\): \(gobr, gr, gr, gr\). The flatness structures on each of these faces is \(H_R:\ensuremath{\text{id}}=_{Tw=Tw}R\) where \(R\) rotates by one vertex clockwise. Using Definition 45 for the index we see that we first need to convert \(gobr\) and \(gr\) into paths of rotations, which give \[\begin{aligned} \sigma^{X_\ensuremath{\mathbb{O}}^s}_{wrgw}=H_R^3 &:R^{-3}=id \\ \sigma^{X_\ensuremath{\mathbb{O}}^s}_{wgow}=H_R^{-1}&:R=id \\ \sigma^{X_\ensuremath{\mathbb{O}}^s}_{wobw}=H_R^{-1}&:R=id \\ \sigma^{X_\ensuremath{\mathbb{O}}^s}_{wbrw}=H_R^{-1}&:R=id \\ \end{aligned}\] Now forming the concatenation of \(H_R\) with each of these gives \(H_R^4, \ensuremath{\mathsf{refl}}_\ensuremath{\text{id}}, \ensuremath{\mathsf{refl}}_\ensuremath{\text{id}}, \ensuremath{\mathsf{refl}}_\ensuremath{\text{id}}\) respectively. The winding numbers are \(1, 0, 0, 0\). So the index around the face that has all the swirling in Figure 9 is 1 and around the other three is 0. We haven’t written out the computation for the southern hemisphere but it will provide another 1 and three 0s, giving a total index of 2.

7 Appendix: the program ahead

Follow-up work could remove the need to assume that maps from the realization of oriented simplicial complexes factor through \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\), instead proving that this is the case. This would unify two assumptions of orientability into one. The assumption that edges appear twice, once with each orientation, could also be deduced from presumably standard material.

An internal definition of Euler characteristic is needed to provide the relationship between total index and the classic invariant.

More relationships with discrete differential geometry[13][14] could be explored.

The results could be formalized. A good starting point is Lemma 28 that the octahedron is equivalent to the 2-sphere.

Our hope is that this note can form the starting point for a complete formulation of the homotopical results of gauge theory and Chern-Weil theory. Classically we know the space of connections is contractible, and the group of based gauge transformations (see below) acts freely on it. Those statements should be easy to make in our framework. In [15] connections are presented as a splitting of a short exact sequence of bundles. The community has grappled with this picture (see the nLab at [16]), and it deserves clarification in HoTT.

The paper of Freed and Hopkins[17] seeks a classifying space for the space of connections on a principal bundle. Their paper served as a primary motivation for this work, and we hope we have taken a step in that direction. Its focus on homotopy theory, model structures, and groupoids should make it accessible to many HoTT theoreticians. We conjecture that the theory of Koszul complexes that arises is the infinitesimal shadow of the higher groupoid structure of the relevant HoTT classifying space.

7.1 Gauge transformations