\(\newcommand{\textesh}{∫}\) \(\newcommand{\ensuremath}{}\) \(\newcommand{\raisebox}[2]{}\)
Download the PDF version or the slides.
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
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 51).
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].
Definition 1. Let \(G\) be a group with identity element \(e\) (with the usual classical structure and properties). A \(G\)-set is a set \(X\) equipped with a homomorphism \(\phi:(G,e)\to\mathop{\mathrm{Aut}}(X)\). If in addition we have a term of type \[\mathsf{is\raisebox{0.5pt}{\underline{\phantom{t}}}torsor}(X,\phi)\stackrel{\mathrm{def}}{=}||X||_{-1}\times \prod_{x:X}\mathsf{is\raisebox{0.5pt}{\underline{\phantom{t}}}equiv}(\phi(-,x):(G,e)\to (X,x))\] then we say \((X,\phi)\) is a \(G\)-torsor. Denote the type of \(G\)-torsors by \(BG\). Denote the \(G\)-torsor given by \(G\) itself under right-multiplication by \(\ensuremath{{G}_\mathrm{reg}}\).
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\).
Lemma 2. ([4] Lemma 5.2). If \((X,\phi),(Y,\psi):BG\) then there is a natural equivalence \((X=_{BG}Y) \simeq (X\to_G Y)\).
Lemma 3. ([4] Proposition 5.4). A \(G\)-set \((X,\phi)\) is a \(G\)-torsor if and only if there merely exists a \(G\)-equivariant equivalence \(\ensuremath{{G}_\mathrm{reg}}\to_G X\).
These lemmas lead to
Corollary 4. ([4] Corollary 5.5). The pointed type \((BG,\ensuremath{{G}_\mathrm{reg}})\) is a \(\mathrm{K}(G,1)\), that is \(BG\) is connected and has a pointed equivalence \(\Omega BG\simeq_* G\).
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?
Definition 5. Let \(G\) be a group. Let \[\mathrm{EM}(G,n)\stackrel{\mathrm{def}}{=}\mathop{\mathrm{BAut}}(\mathrm{K}(G,n))\stackrel{\mathrm{def}}{=}\sum_{Y:\mathcal{U}}||Y\simeq \mathrm{K}(G,n)||_{-1}\] be the connected component of \(\mathcal{U}\) containing \(\mathrm{K}(G,n)\). A \(\mathrm{K}(G,n)\)-bundle on a type \(M\) is a map \(M\to\mathrm{EM}(G,n)\).
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).
Definition 6. Given \(f:M\to\mathrm{EM}(G,n)\), the associated action of \(M\) on \(G\), denoted by \(f_\bullet\) is defined to be \(f_\bullet=F_\bullet\circ||\Sigma||_{n+1}\circ f\).
Theorem 7. (Scoccola[5] Proposition 2.39). A \(\mathrm{K}(G,n)\) bundle \(f:M\to\mathrm{EM}(G,n)\) factors through a map \(M\to\mathrm{K}(G,n+1)\), and so is a principal fibration, if and only if the associated action \(f_\bullet\) is merely homotopic to a constant map.
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)\).
Remark 8. Iterating the loop map gives the isomorphism \(\Omega^{(n+1)}:\mathrm{EM_{\bullet}}(G,n+1)\simeq \mathrm{K}(\mathop{\mathrm{Aut}}G,1)\) (see [5] Lemma 2.7). Theorem 7 therefore says that the map \(f\) factors through \(\mathrm{K}(G,n+1)\) if and only if the map into \(\mathrm{K}(\mathop{\mathrm{Aut}}G,1)\) is homotopic to a constant. In the case of \(G=\ensuremath{\mathbb{Z}}\), the map \(f_\bullet:M\to \mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\) deserves to be called the first Stiefel-Whitney class of \(f\) and one can interpret its triviality as orientability. . This point of view is discussed in Schreiber[7] (starting with Example 1.2.138) and in Myers[8].
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
Definition 9. An abstract simplicial complex \(M\) of dimension \(n\) is an ordered list \(M\stackrel{\mathrm{def}}{=}[M_0,\ldots,M_n]\) consisting of a set \(M_0\) of vertices, and for each \(0<k\leq n\) a set \(M_k\) of subsets of \(M_0\) of cardinality \(k+1\), such that for any \(j<k\), any \((j+1)\)-element subset of an element of \(M_k\) is an element of \(M_j\). The elements of \(M_k\) are called \(k\)-faces. Denote by \(\mathsf{SimCom_n}\) the type of abstract simplicial complexes of dimension \(n\). Let \(M_{\leq k}\stackrel{\mathrm{def}}{=}[M_0,\ldots,M_k]\) and note that \(M_{\leq n}=M\). We call \(M_{\leq k}\) the \(k\)-skeleton of \(M\), and it is a (\(k\)-)complex in its own right. A morphism \(f\) from \(M=[M_0,\ldots,M_m]\) to \(N=[N_0,\ldots,N_n]\) is a function on vertices \(f:M_0\to N_0\) such that for any face of \(M\) the image under \(f\) is a face of \(N\). \(M\) is automatically equipped with a chain of inclusions of the skeleta \(M_0\hookrightarrow M_{\leq 1}\hookrightarrow\cdots\hookrightarrow M_{\leq n}=M\), which are simply the inclusions of lists into longer lists.
We can imagine constructing a simplicial complex dimension by dimension.
Definition 10. Denote by \(\Delta(n)\) the simplicial complex obtained by taking the set of all subsets of the standard \((n+1)\)-element set \(\Delta(n)_0\stackrel{\mathrm{def}}{=}\{0,\ldots,n\}\). We call \(\Delta(n)\) the complete \(n\)-simplex. We will refer to the \((n-1)\)-skeleton \(\Delta(n)_{\leq(n-1)}\) with the suggestive notation \(\partial \Delta(n)\).
Note that \(\Delta(n)_{(n-1)}\) has \(n+1\) elements. For example, \(\Delta(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\).
Definition 11. In an abstract simplicial complex \(M\) of dimension \(n\), the link of a vertex \(v\) is the \((n-1)\)-dimensional subcomplex containing every face \(m\in M_{n-1}\) such that \(v\notin m\) and \(m\cup v\) is an \(n\)-face of \(M\).
The link is easier to understand as all the neighboring vertices of \(v\) and the subcomplex containing these. See for example Figure 3.
Remark 12. The geometric realization of a complex uses the combinatorial data to form pushouts of standard simplices inside the category of topological spaces. A simplicial sphere is a simplicial complex whose geometric realization is homeomorphic to a sphere. A classical 1940 result of Whitehead, building on Cairn, states that every smooth \(n\)-manifold is the geometric realization of a simplicial complex of dimension \(n\) such that the link is the geometric realization of an \((n-1)\)-sphere[10]. For more of this theory see the classic book by Kirby and Siebenmann[11].
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.
Definition 13. The realization \(\ensuremath{\mathbb{M}}_0\) of a 0-dimensional simplicial complex \(M_0\) is simply the set \(M_0\).
Definition 14. The simplicial 0-sphere \(\partial\Delta\mkern-11mu{\scalebox{0.7}{$\Delta$}}({1})\) is the realization of \(\partial \Delta(1)\).
Definition 15. The realization \(\ensuremath{\mathbb{M}}_1\) of a 1-dimensional simplicial complex \([M_0, M_1]\) is the pushout
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.
Definition 16. The simplicial 1-sphere \(\partial\Delta\mkern-11mu{\scalebox{0.7}{$\Delta$}}({2})\) is the realization of \(\partial \Delta(2)\).
Definition 17. A realization \(\ensuremath{\mathbb{M}}_2\) of a 2-dimensional simplicial complex \([M_0, M_1, M_2]\) is the pushout
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.
Definition 18. Given a notion of realization in dimension \(n-1\), a realization \(\ensuremath{\mathbb{M}}_n\) of an \(n\)-dimensional simplicial complex \([M_0, \ldots, M_n]\) is the pushout
where \(\mathbb{A}_n\) is such that the following commutes
Gathering some of the inductive process into one definition, we have
Definition 19. A realization \(\ensuremath{\mathbb{M}}\) of an abstract simplicial complex \(M:\mathsf{SimCom_n}\) consists of
\(n+1\) types \(\ensuremath{\mathbb{M}}_0,\ldots,\ensuremath{\mathbb{M}}_n\) where \(\ensuremath{\mathbb{M}}_0\stackrel{\mathrm{def}}{=}M_0\),
\(n\) spans \({\ensuremath{\mathbb{M}}_{i}}\xleftarrow[]{\mathbb{A}_{i}}{M_{i+1}\times \partial\Delta\mkern-11mu{\scalebox{0.7}{$\Delta$}}({i+1})}\xrightarrow[]{\ensuremath{\mathrm{pr}}_1}{M_{i+1}}\), \(i=0,\ldots,n-1\), where \(\partial\Delta^{i+1}\) is the realization of the boundary of a standard simplex and \(\mathbb{A}_i\) are called attachment maps,
\(n\) pushout squares from each span to \(\ensuremath{\mathbb{M}}_{i+1}\), with induced maps \(\imath_i:\ensuremath{\mathbb{M}}_i\to\ensuremath{\mathbb{M}}_{i+1}\), \(*_{\ensuremath{\mathbb{M}}_{i+1}}:M_{i+1}\to\ensuremath{\mathbb{M}}_{i+1}\) and proof of commutativity \(h_{i+1}\).
A cellular type \(\ensuremath{\mathbb{M}}\) is a sequence of types \(\ensuremath{\mathbb{M}}_0\xrightarrow[]{\imath_0}\ensuremath{\mathbb{M}}_1\xrightarrow[]{\imath_1}\cdots\xrightarrow[]{\imath_{n-1}}\ensuremath{\mathbb{M}}_n\), together with a proof of existence of some simplicial complex \(M\) and a realization inducing this sequence.
3.3 Polygons
The 1-type \(\partial\Delta\mkern-11mu{\scalebox{0.7}{$\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.
Definition 20. Define \(C(n)\), \(n\geq 3\) to be a simplicial complex with \(C(n)_{0}=\{v_1, \ldots, v_n\}\) and edges \[C(n)_1=\{e_1=\{v_1,v_2\}, \ldots, e_{n-1}=\{v_{n-1}, v_n\}, e_n=\{v_n, v_0\}\}.\] We call \(C(n)\) a polygon or \(n\)-gon. The realization of \(C(n)\) will be denoted \(\mathbb{C}(n)\). When it is convenient we may refer to an \(n\)-gon by \([{v_1\cdots v_n}]\) and to its realization by \([\![{v_1\cdots v_n}]\!]\).
We also have two special polygons:
Definition 21. The higher inductive type \(S^1\), also denoted \(\mathbb{C}(1)\), has constructors: \[\begin{aligned} S^1&:\mathsf{Type}\\ \mathsf{base}&:S^1\\ \mathsf{loop}&:\mathsf{base}=\mathsf{base} \end{aligned}\]
Definition 22. The higher inductive type \(\mathbb{C}(2)\) has constructors: \[\begin{aligned} \mathbb{C}(2) &:\mathsf{Type}\\ v_1, v_2&:\mathbb{C}(2) \\ \ell_{12}, r_{21}&:v_1=v_2\\ \end{aligned}\]
Lemma 23. \(\mathbb{C}(2)\simeq \mathbb{C}(1)\) and in fact \(\mathbb{C}(n)\simeq \mathbb{C}(n-1)\).
(Compare to [6] Lemma 6.5.1.)
First we will define \(f:\mathbb{C}(2)\to \mathbb{C}(1)\) and \(g:\mathbb{C}(1)\to \mathbb{C}(2)\), then prove they are inverses. \[\begin{aligned} f(v_1)=f(v_2)&=\ensuremath{\mathsf{base}}&\quad g(\ensuremath{\mathsf{base}})&=v_1\\ f(\ell_{12})&=\ensuremath{\mathsf{loop}}&\quad g(\ensuremath{\mathsf{loop}})&=\ell_{12}\cdot r_{21}\\ f(r_{21}) &= \ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{base}}}& & \\ \end{aligned}\]
We need to show that \(f\circ g\sim \ensuremath{\text{id}}_{\mathbb{C}(1)}\) and \(g\circ f\sim\ensuremath{\text{id}}_{\mathbb{C}(2)}\). Think of \(f\) as sliding \(v_2\) and \(v_1\) towards each other along \(r_{21}\) coalescing into just \(v_1\), as in Figure 4. This may help understand why the somewhat intricate proof is working.
We need terms \(p:\prod_{a:\mathbb{C}(1)}f(g(a))=a\) and \(q:\prod_{a:\mathbb{C}(2)}g(f(a))=a\). We will proceed by induction, defining appropriate paths on point constructors and then checking a condition on path constructors that confirms that the built-in transport of these type families respects the definition on points.
Looking first at \(g\circ f\), which shrinks \(r_{21}\), we have the following data to work with: \[\begin{aligned} g(f(v_1))=g(f(v_2))&=v_1\\ g(f(\ell_{12}))&=\ell_{12}\cdot r_{21}\\ g(f(r_{21})) &= \ensuremath{\mathsf{refl}}_{v_1}. \end{aligned}\] We then need to supply a homotopy from this data to \(\ensuremath{\text{id}}_{\mathbb{C}(2)}\), which consists of a section and pathovers over \(\mathbb{C}(2)\): \[\begin{aligned} p_1&:g(f(v_1))=v_1\\ p_2&:g(f(v_1))=v_2\\ H_\ell&:\mathsf{tr}(\ell_{12})(p_1)=p_2\\ H_r&:\mathsf{tr}(r_{21})(p_2)=p_1. \end{aligned}\] which simplifies to \[\begin{aligned} p_1&:v_1=v_1\\ p_2&:v_1=v_2\\ H_\ell&:g(f(\ell_{12}))^{-1}\cdot p_1\cdot \ell_{12}=p_2\\ H_r&:=g(f(r_{21}))^{-1}\cdot p_2\cdot r_{21}= p_1 \end{aligned}\] and then to \[\begin{aligned} p_1&:v_1=v_1\\ p_2&:v_1=v_2\\ H_\ell&:(\ell_{12}\cdot r_{21})^{-1}\cdot p_1\cdot \ell_{12}=p_2\\ H_r&:\ensuremath{\mathsf{refl}}_{v_1}\cdot p_2\cdot r_{21}= p_1 \end{aligned}\]
To solve all of these constraints we can choose \(p_1\stackrel{\mathrm{def}}{=}\ensuremath{\mathsf{refl}}_{v_1}\), which by consulting either \(H_\ell\) or \(H_r\) requires that we take \(p_2\stackrel{\mathrm{def}}{=}{r_{21}}^{-1}\).
Now examining \(f\circ g\), we have \[\begin{aligned} f(g(\ensuremath{\mathsf{base}}))&=\ensuremath{\mathsf{base}}&\\ f(g(\ensuremath{\mathsf{loop}}))&=f(\ell_{12}\cdot r_{21})=\ensuremath{\mathsf{loop}} \end{aligned}\] and so we have an easy proof that this is the identity.
The proof of the more general case \(\mathbb{C}(n) \simeq \mathbb{C}(n-1)\) is very similar. Take the maps \(f:\mathbb{C}(n)\to \mathbb{C}(n-1)\), \(g:\mathbb{C}(n-1)\to \mathbb{C}(n)\) to be \[\begin{aligned} f(v_i)=v_i&\quad(i=1,\ldots,n-1) & g(v_i)&=v_i&\quad(i=1,\ldots,n-1)\\ f(v_n)=v_1&\quad& g(e_{i,i+1})&=e_{i,i+1}&\quad(i=1,\ldots,n-2)\\ f(e_{i,i+1})=e_{i,i+1}&\quad(i=1,\ldots,n-1)& g(e_{n-1,1})&=e_{n-1,n}\cdot e_{n,1}&\\ f(e_{n-1,n})=e_{n-1,1}&&&&\\ f(e_{n,1})=\ensuremath{\mathsf{refl}}_{v_1}&&&& \end{aligned}\] where \(f\) should be thought of as shrinking \(e_{n,1}\) so that \(v_n\) coalesces into \(v_1\).
The proof that \(g\circ f\sim\ensuremath{\text{id}}_{\mathbb{C}(n)}\) proceeds as follows: the composition is definitionally the identity except \[\begin{aligned} g(f(v_n))&=v_1\\ g(f(e_{n-1,n}))&=e_{n-1,n}\cdot e_{n,1}\\ g(f(e_{n,1}))&= \ensuremath{\mathsf{refl}}_{v_1}. \end{aligned}\] Guided by our previous experience we choose \({e_{n,1}}^{-1}:g(f(v_n))=v_n\), and define the pathovers by transport.
The proof that \(f\circ g\sim\ensuremath{\text{id}}_{\mathbb{C}(n-1)}\) requires only noting that \(f(g(e_{n-1,1}))=f(e_{n-1,n}\cdot e_{n,1})=e_{n-1,1}\cdot\ensuremath{\mathsf{refl}}_{v_1}=e_{n-1,1}\).
Corollary 24. All polygons are equivalent to \(S^1\), i.e. we have terms \(e_n:\mathbb{C}(n)=S^1\), and hence we have constructed a map from the unit type \((\mathbb{C}(n), ||e_n||_{-1}):\mathsf{\mathbf{1}}\to \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\).
The proofs in Lemma 23 can be concatenated to give \(\mathbb{C}(n)\to\mathbb{C}(n-1)\to\cdots\to\mathbb{C}(2)\to S^1\).
Definition 25. Let \(R:[{v_1\cdots v_n}]\to [{v_1\cdots v_n}]\) (for “rotation”) be the map sending \(v_i\mapsto v_{i+1}\) and \(v_n\mapsto v_0\). This map clearly sends edges to edges, and so is a map of simplicial complexes, and extends to a map \([\![{R}]\!]:[\![{v_1\cdots v_n}]\!]\to [\![{v_1\cdots v_n}]\!]\).
The homotopical realization \([\![{R}]\!]\) has a path to the identity:
Lemma 26. The map \([\![{R}]\!]: [\![{v_1\cdots v_n}]\!]\to [\![{v_1\cdots v_n}]\!]\) is connected to \(\ensuremath{\mathsf{refl}}_{[\![{v_1\cdots v_n}]\!]}\) by a homotopy \(H_R:\prod_{x:[\![{v_1\cdots v_n}]\!]}x=[\![{R}]\!](x)\).
If \(x\) is a vertex, take \(H_R(x)\) to be the obvious unique edge back to the starting vertex. This extends in the obvious functorial way to edges.
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.
Definition 27. An orientation \(\mathscr{O}\) of a 2-dimensional simplicial complex \(M=[M_0, M_1, M_2]\) is an equivalence class of ordering maps \(O:M_2\to \mathsf{List}\) to the type of ordered lists, where \(O\) orders the vertices of every 2-face. If \(F:M_2\) is a face and \(F=\{a, b, c\}\) are its vertices, then \(O(F)\) is a list of all the vertices, e.g. \([b, c, a]\). Two orderings \(O, O'\) are said to have the same orientation if it is true for every face \(F\) that \(O(F)\) and \(O'(F)\) differ by a cyclic permutation. The inclusion \(e\subset F\) of an edge in a face induces an ordering of the vertices of the edge, called the induced order of \(e\subset F\).
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}}\).
Lemma 28. There is an equivalence \(\ensuremath{\mathbb{O}}\simeq S^2\).
Omitted.
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.
Definition 29. If \(\ensuremath{\mathbb{M}}\stackrel{\mathrm{def}}{=}\ensuremath{\mathbb{M}}_0\xrightarrow[]{\imath_0}\cdots\xrightarrow[]{\imath_{n-1}}\ensuremath{\mathbb{M}}_n\) is a cellular type and \(f_k:\ensuremath{\mathbb{M}}_k\to\mathcal{U}\) are type families on each skeleton such that all the triangles commute in the diagram:
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.
Definition 30. If \(\ensuremath{\mathbb{M}}\) is the realization of a simplicial complex, such that for each pushout defining \(\ensuremath{\mathbb{M}}_k\) we have the diagram
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
Lemma 31. Given \(f_{k-1}\) as above, a \(k\)-connection exists if and only if there exists a flatness structure for each \(k\)-face.
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.
Definition 32. \(T_0\stackrel{\mathrm{def}}{=}\mathop{\mathrm{\mathsf{link}}}:\ensuremath{\mathbb{O}}_0\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) is given by: \[\begin{aligned} \mathop{\mathrm{\mathsf{link}}}(w) &= [\![{brgo}]\!] & \mathop{\mathrm{\mathsf{link}}}(r) &= [\![{wbyg}]\!] \\ \mathop{\mathrm{\mathsf{link}}}(y) &= [\![{bogr}]\!] & \mathop{\mathrm{\mathsf{link}}}(g) &= [\![{wryo}]\!] \\ \mathop{\mathrm{\mathsf{link}}}(b) &= [\![{woyr}]\!] & \mathop{\mathrm{\mathsf{link}}}(o) &= [\![{wgyb}]\!] \end{aligned}\]
We chose these orderings for the vertices in the link, by visualizing standing at the given vertex as if it were the north pole, then looking south and enumerating the link in clockwise order, starting from \(w\) if possible, else \(b\).
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\).
Definition 33. Define \(T_1:\ensuremath{\mathbb{O}}_1\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) on just the 1-skeleton by extending \(T_0\) as follows: Transport away from \(w\):
\(T_1(wr):[\![{brgo}]\!]\mapsto [\![{bygw}]\!]\) (\(b, g\) fixed)
\(T_1(wg):[\![{brgo}]\!]\mapsto [\![{wryo}]\!]\)
\(T_1(wb):[\![{brgo}]\!]\mapsto [\![{yrwo}]\!]\) (\(r, o\) fixed)
\(T_1(wo):[\![{brgo}]\!]\mapsto [\![{bwgy}]\!]\)
Transport away from \(y\):
\(T_1(yb):[\![{bogr}]\!]\mapsto [\![{woyr}]\!]\)
\(T_1(yr):[\![{bogr}]\!]\mapsto [\![{bygw}]\!]\)
\(T_1(yg):[\![{bogr}]\!]\mapsto [\![{yowr}]\!]\)
\(T_1(yo):[\![{bogr}]\!]\mapsto [\![{bwgy}]\!]\)
Transport along the equator:
\(T_1(br):[\![{woyr}]\!]\mapsto [\![{wbyg}]\!]\)
\(T_1(rg):[\![{wbyg}]\!]\mapsto [\![{wryo}]\!]\)
\(T_1(go):[\![{wryo}]\!]\mapsto [\![{wgyb}]\!]\)
\(T_1(ob):[\![{wgyb}]\!]\mapsto [\![{woyr}]\!]\)
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.
Definition 34. Define \(T_2:\ensuremath{\mathbb{O}}\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) by extending \(T_1\) to the faces as follows (making use of \(H_R\) from Lemma 26):
\(T_2(wbr)=H_R\)
\(T_2(wrg)=H_R\)
\(T_2(wgo)=H_R\)
\(T_2(ybo)=H_R\)
\(T_2(yrb)=H_R\)
\(T_2(ygr)=H_R\)
\(T_2(yog)=H_R\)
\(T_2(ybo)=H_R\)
Defining these flatness structures suffices to define \(T_2\) by Lemma 31.
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\).
Definition 35. Given 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\) equipped with type family \(T:\ensuremath{\mathbb{M}}\to\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) extending \(\mathop{\mathrm{\mathsf{link}}}\), a vector field on \(\ensuremath{\mathbb{M}}\) is a section on the 1-skeleton, i.e. a term \(X:\prod_{x:\ensuremath{\mathbb{M}}_1}T(x)\).
Remark 36. The circle bundle extending \(\mathop{\mathrm{\mathsf{link}}}\) captures the unit spheres of the classical tangent bundle. A section of this bundle is therefore analogous to a classical nonvanishing vector field. To allow for classical vector fields with zeros, we are limiting the section \(X\) to the 1-skeleton of \(\ensuremath{\mathbb{M}}\).
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 51.
Recall that \(S^1\) acts on all the fibers of \(T\). We will derive two operations involving \(S^1\).
Definition 37. The map \(\ensuremath{\mathrm{pr}}_1\circ (\alpha, \ensuremath{\mathrm{pr}}_2)^{-1}:T_i\times T_i\to S^1\) is called subtraction. It maps \((x,y)\) to the unique term \(\delta:S^1\) such that \(\alpha(\delta, x)=y\). For brevity we denote \(\ensuremath{\mathrm{pr}}_1\circ (\alpha, \ensuremath{\mathrm{pr}}_2)^{-1}(x,y)\) by \(y-x\).
Lemma 38. If \(G\) is a higher group with multiplication \(\mu:G\times G\to G\) and proof of commutativity \(\mathsf{is\raisebox{0.5pt}{\underline{\phantom{t}}}comm}:\prod_{a,b:G}\mu(a, b)=\mu(b, a)\) then \(\mu\) induces a function \(\mu_=:(x=_G y)\times (x'=_G y')\to (\mu(x, x')=_G\mu(y,y'))\).
If \(p:x=_G y\) and \(p':x'=_G y'\), then we can define \(\mu_=(p, p')\) by concatenating the three paths \[\begin{aligned} \mu(x',p)&:\mu(x', x)=_G\mu(x', y)\\ \mathsf{is\raisebox{0.5pt}{\underline{\phantom{t}}}comm}(x',y)&:\mu(x',y)=_G\mu(y,x')\\ \mu(y, p')&:\mu(y, x')=_G\mu(y, y').\qedhere \end{aligned}\]
Each fiber \(T_i\) is pointed by \(X_i\), so we can define the map \(T_i\xrightarrow[]{-X_i}S^1\), and then give a name to the special term \(T_{ij}X_j - X_i\).
Definition 39. We define the rotation of \(T_{ij}\) by \(\rho_{ij}\stackrel{\mathrm{def}}{=}T_{ij}X_j - X_i\). The map \(+\rho_{ij}:S^1\to S^1\) makes the following diagram commute
Lemma 40. \(\rho_{ij}+\rho_{ji}=_{S^1}0\).
\[\begin{aligned} (X_i + \rho_{ij})+\rho_{ji} &=_{T_i} T_{ij}X_j + \rho_{ji}&&\text{by definition of }\rho_{ij}\\ &=_{T_i} T_{ij}(X_j + \rho_{ji})&&\text{by equivariance of transport} \\ &=_{T_i} T_{ij}(T_{ji}(X_i))&&\text{by definition of }\rho_{ji}\\ &=_{T_i} X_i&&\text{by definition of }T\qedhere \end{aligned}\]
We can obtain a path in \(S^1\) 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=_{S^1}0 \\ &:\rho_{ji}=_{S^1}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 38 to lift this requirement, by obtaining paths in \(S^1\) that can be added without needing to be concatenated directly.
Lemma 41. With the notation \(\sigma_{ij}\stackrel{\mathrm{def}}{=}X_{ij}-X_j\), and with addition of paths as in Lemma 38, we have \(\sigma_{ij}+\sigma_{ji}=_{0=_{S^1}0}\ensuremath{\mathsf{refl}}_0\).
First we need to show that the sum is a loop, then we can prove that it is \(\ensuremath{\mathsf{refl}}_0\). The terms have these types: \[\begin{aligned} \sigma_{ij}&:\rho_{ji}=_{S^1}0\\ \sigma_{ji}&:\rho_{ij}=_{S^1}0 \end{aligned}\] so when we add these paths with \(+\) we obtain a path \(\sigma_{ij}+\sigma_{ji}:\rho_{ji}+\rho_{ij}=_{S^1} 0\) which by Lemma 40 is \(0=_{S^1}0\). We compute \(+\) using the concatenations in Lemma 38, which gives \[\begin{aligned} \sigma_{ij}+\sigma_{ji} &: (0+0) \overset{\mathrm{Lemma~}\ref{lem:subtraction}}{=\mathrel{\mkern-3mu}=} (\rho_{ji}+\rho_{ij}) \overset{\sigma_{ij}+\rho_{ij}}{=\mathrel{\mkern-3mu}=} (0+\rho_{ij}) &&\overset{\mathsf{is\raisebox{0.5pt}{\underline{\phantom{t}}}comm}}{=\mathrel{\mkern-3mu}=} (\rho_{ij}+0) \overset{\sigma_{ji}}{=\mathrel{\mkern-3mu}=} (0+0)\\ \sigma_{ij}+\sigma_{ji}&=_{0=_{S^1}0} (\sigma_{ij}+\rho_{ij})\cdot \sigma_{ji}&& \\ &=_{0=_{S^1}0} ((X_{ij}-X_j)+\rho_{ij})\cdot (X_{ji} - X_i)&&\text{definition of }\sigma s\\ &=_{0=_{S^1}0} (T_{ij}(X_{ij})-X_i)\cdot (X_{ji} - X_i)&&\text{action of }\rho_{ij}\text{ (see (\ref{eq:action_of_rho}))} \\ &=_{0=_{S^1}0} \ensuremath{\mathsf{refl}}_{X_i}-X_i&&\text{path induction for }X\\ &=_{0=_{S^1}0} \ensuremath{\mathsf{refl}}_0&&\qedhere \end{aligned}\]
Remark 42. The classical argument of Hopf [2], which is presented in more detail in the more readily available [3], makes an implicit assumption that we can concatenate two terms of different type such as \(X_{ij}\) and \(X_{kl}\). The authors name such terms “change in angle across an edge” and stipulate that this is a function “defined on edges.” The extra work we are doing in this section amounts to a partial formalization of this idea.
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 &{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 &{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 &{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 &{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 38 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:
Proposition 43. Given a polygon \(\mathbb{C}(n):\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) and a point \(b:\mathbb{C}(n)\) the evaluation map \(\mathrm{ev}(b):(\mathbb{C}(n)=_{\mathrm{K}(\ensuremath{\mathbb{Z}},2)}\mathbb{C}(n))\to \mathbb{C}(n)\) is an equivalence.
See [4].
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).
Definition 44. The index of the vector field \(X\) on the face \(F\) is the integer \(I^X_F\stackrel{\mathrm{def}}{=}\flat_F\cdot \sigma^X_F:(\ensuremath{\text{id}}=_{Tm=Tm}\ensuremath{\text{id}})\).
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.
Definition 45. A 2-dimensional simplicial complex \(M^+=[M_0, M_1, M_2]\) with orientation \(\mathscr{O}\) is without boundary if every edge is a subset of exactly two faces, and if the orderings induced by the two inclusions differ by a swap of vertices.
Some of the assumptions in these definitions are unnecessary because they are entailed in other assumptions, but we will not attempt to eliminate them.
Definition 46. An oriented set of pointed faces of a realization \(\ensuremath{\mathbb{M}}\) of a 2-dimensional simplicial complex \(M=[M_0,M_1,M_2]\) with orientation \(\mathscr{O}\) is a choice \(v_F:F\) of a vertex in each face \(F:M_2\), and the boundary path \(\ell_F:v_F=v_F\) that concatenates the three edges of the face in the order determined by the orientation.
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 38 how to perform the required sum.
Definition 47. The net holonomy, total flatness, total swirling, and total index on an oriented set of pointed faces is \[\label{eq:tot_elements} \begin{aligned} \mathsf{tr}_\mathrm{tot}& \stackrel{\mathrm{def}}{=}\sum_F\mathsf{tr}_F &&:S^1\\ \flat_\mathrm{tot}& \stackrel{\mathrm{def}}{=}\sum_F\flat_F &&:\ensuremath{\mathsf{base}}=_{S^1}\mathsf{tr}_\mathrm{tot}\\ \sigma^X_\mathrm{tot}& \stackrel{\mathrm{def}}{=}\sum_F\sigma^X_F &&:\mathsf{tr}_\mathrm{tot}=_{S^1}\ensuremath{\mathsf{base}}\\ I^X_\mathrm{tot}& \stackrel{\mathrm{def}}{=}\sum_F I^X_F &&:\ensuremath{\mathbb{Z}}. \end{aligned}\]
The assumption about edges appearing twice, once in each direction, together with Lemma 40 proves the following
Proposition 48. The net holonomy is \(0\) in \(S^1\).
With a vector field \(X\) chosen, we can compute \[\sum_F\mathsf{tr}_F=\left[\sum_{(\mathrm{edges\ }e_{ij})} \rho_{ij}+\rho_{ji}\right]=_{S^1}0\] and note that the result does not depend on \(X\).
Corollary 49. Total flatness is a loop: \(\flat_\mathrm{tot}:\ensuremath{\mathsf{base}}=_{S^1}\ensuremath{\mathsf{base}}\).
Follows from Corollary 48.
And making use of Lemma 41 we obtain
Proposition 50. The total swirling is \(\ensuremath{\mathsf{refl}}_0\) in \(S^1\).
We can compute \[\sum_F\sigma^X_F=\left[\sum_{(\mathrm{edges\ }e_{ij})}\sigma_{ij}+\sigma_{ji}\right]=_{S^1}\ensuremath{\mathsf{refl}}_0.\qedhere\]
And finally, if we refer to the passage from a loop \(\ell:\ensuremath{\mathsf{base}}=_{S^1} \ensuremath{\mathsf{base}}\) to the corresopnding integer in \(\Omega S^1\) as “winding number”:
Theorem 51. The winding number of total flatness equals the total index.
Follows directly from \(I^X_\mathrm{tot}\stackrel{\mathrm{def}}{=}\flat_\mathrm{tot}\cdot \sigma^X_\mathrm{tot}\) and Proposition 50.
Remark 52. The Gauss-Bonnet theorem is often stated in the form \[\frac{1}{2\pi}\int_M K\,dA=\chi(M)\] and although we won’t attempt an exhaustive translation between this and our approach, we want to point out that the factor of \(\frac{1}{2\pi}\) is doing exactly what winding number is doing for us. It seems likely that attending fully to constant coefficients in other important formulas can yield conceptual fruit.
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 48. 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 44 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
Definition 53. Suppose we have \(T:M\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) and \(P\stackrel{\mathrm{def}}{=}\sum_{x:M}Tx\). Then we can form the type family \(\mathop{\mathrm{Aut}}T:M\to\mathcal{U}\) given by \(\mathop{\mathrm{Aut}}T(x)\stackrel{\mathrm{def}}{=}(Tx=Tx)\). The total space \(\mathop{\mathrm{Aut}}P\stackrel{\mathrm{def}}{=}\sum_{x:M}(Tx=Tx)\), which is a bundle of groups, is called the automorphism bundle or the gauge bundle and sections \(\prod_{x:M}(Tx=Tx)\), which are homotopies \(T\sim T\), are called automorphisms of \(P\) or gauge transformations. If \(m:M\) is a basepoint and if \(p:Tm\) is a basepoint in the fiber at \(m\), then the pointed automorphisms of \(P\) or based gauge transformations.