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

Abstract

Higher inductive types can capture some concepts of differential geometry in two dimensions including connections, curvature, and vector fields. We define connections on higher inductive types. We then define tangent bundles and vector fields by looking at the special subclass of combinatorial manifolds, which are discrete in the sense of real cohesion (Shulman, 2017), drawing inspiration from the field of discrete differential geometry. We prove the Gauss-Bonnet theorem and Poincaré-Hopf theorem for combinatorial manifolds.

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

Notes so far from Mathieu and Steve

0.1 November 21, Mathieu and Steve

Constructors are present in the HIT, and the HIT is a type. The universe must be closed under inductive types.

Polygons of different cardinality will tangle with transport.

Greg suggests I could use an isomorphism from a combinatorial manifold to a HIT with just one 2-cell to capture “total curvature”:

def S^1:
base: S^1
loop: base=base

def S^2:
N: S^2
surf: refl_N = refl_N

def torus:
b:torus
p,q:b=b
donut:p.q=q.p

The map \(\mathcal{R}\) (realization) is a lossy map. \(\mathcal{R}(S^2):\mathcal{U}\).

“strict morphism of HITs”: map constructors to constructors. \(C_4\to S^1\) is a strict map.

\(\mathcal{R}(C_4)\) has an equivalence to \(\mathcal{R}(S^1)\). Perhaps this is \(\mathcal{R}\)(the map \(C_4\to S^1\), the strict one). But \(S^1\to C_4\) is non-strict, uses generated data, uses data from \(\mathcal{R}(C_4)\).

Claim: we cannot see the one-notch “90 degree” rotation of \(C_4\) at the level of types.

0.1.1 Extension to next dimension as obstruction theory

• Consider a type \(X\) with 1-skeleton \(X_1\).

• HIT gives skeletal filtration

• functions naturally given as per-skeleton steps

• there are constraints/obstructions: obstruction to extend map \(T\) from vertices \(a, b\) to path \(e:a=b\) is that \(T(a)\) and \(T(b)\) are in the same connected component.

• say a 2-cell \(F\) contracts a loop \(L\), i.e. \(F:L=\ensuremath{\mathsf{refl}}_v\) some vertex \(v\)

• we have a choice of \(v\) for each face \(F\)

• then \(T(F)\) must be in same component as \(\ensuremath{\mathsf{refl}}_v\) (\(\ensuremath{\mathsf{refl}}_v:\pi_1 X\) with basepoint \(v\))

• \(T(F)\) is merely \(\ensuremath{\mathsf{refl}}\), and holonomy is merely \(\ensuremath{\mathsf{refl}}\), and connection on this face \(F\) is merely flat

• curvature is a function from 2-cells to \(\pi_1(X,v)\)

\[\begin{aligned} T(v)&:U\\ T(L)&:T(v)=T(v)\\ T(F)&:\ensuremath{\mathsf{refl}}_{T(v)}=T(L) \end{aligned}\]

The class \(||T(L)||:\pi_1(U,T(v))\) is an obstruction to having \(T(F)\), to extending \(T\) to \(F\).

The hierarchy of maps extending to higher skeletons, which we call connections of dimension 1, 2, etc. This works for ANY HIT. The combinatorial manifold structure is just one special case that gives me a specific map \(T\).

Then Mathieu drew on the board a patch of a combinatorial manifold with links of different vertex cardinalities. Then he wrote some maps that might help define the degree/index of a vector field.

0.2 November 27, Mathieu

An angle is: a path in \(S^1\) from \(\ensuremath{\mathsf{base}}\), which is equiv to a path in \(\mathop{\mathrm{Aut}}S^1\) from the identity to another automorphism. (automorphism is primary: aut of tangent circle).

Viewed as automorphisms we can compose them.

Viewed as paths, multiply path 2 by the element at the endpoint of path 1.

Curvature maps a loop in the base to a path in automorphisms of the tangent circle at the base.

A vector field + a trivialization (“fiducial v.f.” in the book by Needham) maps a loop in the base to the tangent circle at the basepoint. We can take the index/degree of this.

Given a loop \(L:v=v\), v.f. \(F\), take \(F(L):tr_L(F(v))=F(v)\) (\(\mathsf{apd}\), dependent action on paths).

Type family \(f:A\to U\), \(\prod_{a:A}fa\) is the type of dependent functions. Let \(X:\prod_{a:A}fa\). We can apply \(X\) to a path \(p:a=_A b\). \(X(p)\) is a path over \(p\). \[X(p):tr_p(X(a))=X(b)\] \(X(a), X(b)\) are terms of different types.

Greg reminded about horizontal projection interpretation of covariant derivative: covariant derivative of \(F\) along itself: lift \(F\) to \(F'\) horizontal on \(TP (P\to M)\), take \([F', F']\)

Tangent bundle \(TM\to M\) w/ connection \(\omega\). Covariant derivative of \(F\) in the direction of \(X\): \(\nabla_X(F)(x)\).

1. Lift \(X\) and \(F\) to horizontal fields \(X', F'\) in \(TTM\)

2. Compute \([X', F']\) to \(TTM\)

3. Decompose \([X', F'] = [X, F]' + \omega([X', F'])\)

Mathieu would rather use this formulation: \[\nabla_X(F) = [X, F] + \omega(X)(F)\] Now take \(X=F\): \[\nabla_F(F) = [F, F] + \omega(F)(F) = \omega(F)(F)\]

1 Overview

We will define

• combinatorial 2-manifolds

• circle bundles, and principal circle bundles of tangent bundles

• vector fields,

and then observe emerging from those definitions the presence of

• connections

• curvature

• the index of a vector field,

and prove

• the Gauss-Bonnet theorem

• and the Poincaré-Hopf theorem.

We will consider functions \(M\to \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) where \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) is the connected component in the universe of the Eilenberg-MacLane space \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\) which we will take to be \(S^1\), and where \(M\) is a combinatorial manifold of dimension 2, which is a simplicial complex encoded in a higher inductive type, such that each vertex has a neighborhood that looks like a disk with a discrete circle boundary (i.e. a polygon). We can call terms \(C:\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) “mere circles.”

We will see in Section 3.3 that \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) contains all the polygons. We will construct a map \(\mathop{\mathrm{\mathsf{link}}}:M\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) that maps each vertex to the polygon consisting of its neighbors. Then we can consider the type of pointed mere circles \(\mathrm{EM_{\bullet}}(\ensuremath{\mathbb{Z}},1)\stackrel{\mathrm{def}}{=}\sum_{Y:\mathrm{EM}(\ensuremath{\mathbb{Z}},1)}Y\) as well as the first projection that forgets the point. This is a univalent fibration (univalent fibrations are always equivalent to a projection of a type of pointed types to some connected component of the universe (Christensen, 2015)). If we form the pullback

then we have a bundle of mere circles, with total space given by the \(\sum_{}\)-type construction. We will show that this is not a principal bundle, i.e. a bundle of torsors. Torsors are types with the additional structure of a group action. But if \(\mathop{\mathrm{\mathsf{link}}}\) satisfies an additional property (amounting to an orientation) then the pullback is a principal fibration, i.e. \(\mathop{\mathrm{\mathsf{link}}}\) factors through a map \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\), where \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) is an Eilenberg-Mac Lane space.

We will argue that extending \(\mathop{\mathrm{\mathsf{link}}}\) to a function \(T\) on paths can be thought of as constructing a connection, notably one that is not necessarily flat (trivial). Moreover, lifting \(T\) to \(T_\bullet:M\to\mathrm{EM_{\bullet}}(\ensuremath{\mathbb{Z}},1)\) can be thought of as a nonvanishing vector field. There will in general not be a total lift, just a partial function. The domain of \(T_\bullet\) will have a boundary of circles, and the degree (winding number) on the disjoint union of these can be thought of as the index of \(T_\bullet\). We can then examine the total curvature and the total index and prove that they are equal, and argue that they are equal to the usual Euler characteristic. This will simultaneously prove the Poincaré-Hopf theorem and Gauss-Bonnet theorem in 2 dimensions, for combinatorial manifolds. This is similar to the classical proof of Hopf (Hopf, 1983), presented in detail in Needham (Needham, 2021).

1.1 Future work

The results of this note can be extended in many directions. There are higher-dimensional generalizations of Gauss-Bonnet, including the theory of characteristic classes and Chern-Weil theory (which links characteristic classes to connections and curvature). These would involve working with nonabelian groups like \(SO(n)\) and sphere bundles. Results from gauge theory could be imported into HoTT, as well as results from surgery theory and other topological constructions that may be especially amenable to this discrete setting. Relationships with computer graphics and discrete differential geometry (Crane et al., 2013) (Crane, 2010) could be explored. Finally, a theory that reintroduces smoothness could allow more formal versions of the analogies explored here.

2 Torsors and principal bundles

The classical theory of principal bundles tells us to look for an appropriate classifying space of torsors to map into.

If \((X,\phi),(Y,\psi):BG\) then a \(G\)-equivariant map 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\).

Denote by \(*\) the torsor given by \(G\) actions on its underlying set by left-translation. This serves as a basepoint for \(BG\) and we have a group isomorphism \(\Omega BG\simeq G\).

In particular, to classify principal \(S^1\)-bundles we map into the space \(\mathrm{K}(S^1, 1)\), a type of torsors of the circle. Since \(S^1\) is a \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\), we have \(\mathrm{K}(S^1,1)\simeq\mathrm{K}(\ensuremath{\mathbb{Z}},2)\).

2.1 Bundles of mere circles

We find it illuminating to look also at the slightly more general classifying space of \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\)-bundles, that is bundles whose fiber are equivalent to \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\). We can understand very well when these are in fact bundles of circle torsors, which will in turn shed light on orientation in this setting.

We will follow Scoccola (Scoccola, 2020). We will state the definitions and theorems for a general \(\mathrm{K}(G,n)\) but we will be focusing on \(n=1\) in this note.

Scoccola uses two self-maps on the universe: suspension followed by \((n+1)\)-truncation \(||\Sigma||_{n+1}\) and forgetting a point \(F_\bullet\) 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)\] from types to types with two points (north and south), to pointed types (by forgetting the south point).

Let’s relate this to orientation. Note that the obstruction in the theorem is about a map into \(\mathrm{EM_{\bullet}}(G,n+1)\) and further note that \(\mathrm{EM_{\bullet}}(G,n)\simeq \mathrm{K}(\mathop{\mathrm{Aut}}G,1)\) (independent of \(n\)). The theorem says that the data of a map into \(\mathrm{EM}(G,n)\) factors into data about a map into \(\mathrm{K}(G,n+1)\) and one into \(\mathrm{K}(\mathop{\mathrm{Aut}}G,1)\). Informally, \(\mathrm{EM}(G,n)\) is a little too large to be a \(K(G,n+1)\), as it includes data about automorphisms of \(G\).

In the special case of \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) the conditions of the theorem are met when \(f_\bullet:M\to\mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\) is contractible. \(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}\) consists of the \(\ensuremath{\mathbb{Z}}/2\ensuremath{\mathbb{Z}}\) worth of outer automorphisms given by multiplication by \(\pm 1\). If we look at the fiber sequence \[\mathrm{K}(S^1, 1)\to \mathop{\mathrm{BAut}}S^1\to \mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\] we see the automorphisms of the circle as an extension of the group of automorphisms that are homotopic to the identity (which are the torsorial actions) by the group that sends the loop in \(S^1\) to its inverse. This is another way to see that a map \(f:M\to \mathop{\mathrm{BAut}}S^1\simeq \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) factors through \(\mathrm{K}(S^1, 1)\simeq \mathrm{K}(\ensuremath{\mathbb{Z}},2)\) if and only if the composition to \(\mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}},1)\) is trivial. This amounts to a choice of loop-direction for all the circles, and so deserves the name “\(f\) is oriented.” In addition the map \(\mathop{\mathrm{BAut}}S^1\to \mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\) deserves to be called the first Stiefel-Whitney class of \(f\), and the requirement here is that it vanishes.

2.2 Pathovers in circle bundles

Suppose we have \(T:M\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) and \(P\stackrel{\mathrm{def}}{=}\sum_{x:M}T(x)\). We adopt a convention of naming objects in \(M\) with Latin letters, and the corresponding structures in \(P\) with Greek letters. 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):T(a)=T(b)\). This is a path in the codomain, which in this case is a type of types. Type theory also provides a function called transport, denoted \(\mathsf{tr}(p):T(a)\to T(b)\) which acts on the fibers of \(P\). \(\mathsf{tr}(p)\) is a function, acting on the terms of the types \(T(a)\) and \(T(b)\), 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)=_{T(b)}\beta\) between \(\alpha:T(a)\) and \(\beta:T(b)\) in the fibers. 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.

Lastly we want to 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\).

3 Combinatorial manifolds

3.1 Combinatorial manifolds

We will adapt to higher inductive types in a straightforward manner the classical construction of combinatorial manifolds. See for example the classic book by Kirby and Siebenmann (Kirby & Siebenmann, 1977). These are a subclass of simplicial complexes.

Note that we don’t require all subsets of \(M_0\) to be included – that would make \(M\) an individual simplex. A simplicial complex is a family of simplices that are identified along various faces.

The link is all the neighboring vertices of \(v\) and the codimension 1 faces joining those to each other. See for example Figure 2.

In a 2-dimensional combinatorial manifold the link is a polygon. See Figures 3, 4, and 5 for some examples of 2-dimensional combinatorial manifolds of genus 0, 1, and 3.

A classical 1940 result of Whitehead, building on Cairn, states that every smooth manifold admits a combinatorial triangulation (Whitehead, 1940). So it appears reasonably well motivated to study this class of objects.

3.2 Higher inductive combinatorial manifolds

We will convert a simplicial complex \(M\) of dimension at most 2 to a higher inductive type, in two steps.

We will assume there is a formal theory of such HITs, and that at least up to dimension 2 there are no obstructions to simply copying over the combinatorial data to the HIT constructors. We will further assume that taking the link of a point (Definition 5) can be imported verbatim to the HIT context without difficulty. For recent work on HITs see for example David Wärn’s discussion of pushouts (Wärn, 2024).

We’re making the distinction between \(\mathcal{H}\) and \(\mathcal{R}\) because we will mostly study functions and phenomena on \(\mathcal{H}(M)\) for some simplicial complex \(M\).

3.3 Polygons

We will now start looking at some examples, first by defining a type that is important both for the domain and the codomain of mere circles: a square.

The standard HoTT circle itself is a non-example of a combinatorial manifold since it lacks the second vertex of the edge:

Both of these are examples of a family of HIT data we will call \(\ensuremath{\mathsf{Gon}}\), the set of \(n\)-gon HITs for some natural number \(n\), following the pattern of the HITs above. We’ll see below that the realization of an \(n\)-gon is a mere circle, i.e. we have \(\mathcal{R}:\ensuremath{\mathsf{Gon}}\to \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\).

3.4 Adding and removing points from polygons

Recall that 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, where \(p:a=_A a'\) and \(q:\phi(a)=\psi(a)\) (see Figure 7): \[\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.

Proof. (Compare to (Univalent Foundations Program, 2013) Lemma 6.5.1.) In the case of \(C_1\) we will denote its constructors by \(\ensuremath{\mathsf{base}}\) and \(\ensuremath{\mathsf{loop}}\). For \(C_2\) we will denote the points by \(v_1, v_2\) and the edges by \(\ell_{12}, r_{21}\). For \(C_3\) and higher we will denote the points by \(v_1,\ldots,v_n\) and the edges by \(e_{i,j}:v_i=v_j\) where \(j=i+1\) except for \(e_{n,1}\).

First we will define \(f:C_2\to C_1\) and \(g:C_1\to 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}}_{C_1}\) and \(g\circ f\sim\ensuremath{\text{id}}_{C_2}\). Think of \(f\) as sliding \(v_2\) along \(r_{21}\) to coalesce with \(v_1\). This may help understand why the unfortunately intricate proof is working.

We need terms \(p:\prod_{a:C_1}f(g(a))=a\) and \(q:\prod_{a: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}}_{C_2}\), which consists of a section and pathovers over \(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 \(C_n \simeq C_{n-1}\) is very similar. Take the maps \(f:C_n\to C_{n-1}\), \(g:C_{n-1}\to 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}}_{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}}_{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}\). ◻

Proof. We can add \(n-1\) points to \(S^1\) and use Lemma 3. ◻

With \(m_k\) we can start with a collection of pentagons and hexagons and make the collection homogeneous: by applying \(m_6\) to the pentagons and \(m_5\) to the hexagons we obtain a collection of 30-gons. This will be useful when we work more with the link function.

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

We will create our first combinatorial surface, a 2-sphere. We will adopt the convention that a subscript indicates the dimension of a subskeleton of a complex. For instance, we have \(\mathsf{base}:S^1_0\).

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

4 Connections and vector fields

4.1 The function \(T\)

We will build up a map \(T\) out of \(\ensuremath{\mathbb{O}}\) which is meant to be like the circle bundle of a tangent bundle. And so we will begin with the intrinsic data of the link at each point: taking the link of a vertex gives us a map from vertices to polygons.

To extend \(T_0\) to a function \(T_1\) on the 1-skeleton we have complete freedom. Defining a map by induction makes clear that the action on paths is its own structure. Two functions on the octahedron could agree on points but differ on edges. We are going to identify this 1-dimensional freedom with a connection:

Continuing the example, we will do something “tangent bundley”, imagining 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 8 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.

Note by univalence the equivalence \(R\) gives a loop in the universe, a term of \(C_4=_{\mathrm{EM}(\ensuremath{\mathbb{Z}},1)}C_4\).

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.2 \(T\) on concatenations of faces

Consider Figure 9 and the diamond on the left. Denote the clockwise triangular path around the left triangle by \(bcab\), and around the right by \(bdcb\). These are loops at \(b\). Say that the tangent map \(T\) satisfies \(T(bcab)=R\) where \(R\) is some rotation of the 4-sided polygon \(Tb\), and similarly \(T(bdcb)=R\) as well.

Since \(bcab\) has a filler 2-cell, which we will call \(f_1\), we know that \(T(f_1)=H_R\) where \(H_R:R=\ensuremath{\mathsf{refl}}\) is a path in \(\mathop{\mathrm{Aut}}(Tb)\) from \(R\) to the identity. Similarly if \(f_2\) is the filler for \(bdcb\) then \(T(f_2)=H_R\).

The two faces can be horizontally composed giving \(f_1\star f_2\), which fills the diamond \(bdcab\). Then we also obtain \(T(f_1\star f_2):R^2=\ensuremath{\text{id}}\).

In this way, given an explicit ordering of the faces (a “plan” for visiting all faces of the manifold), we can “sum” the curvature. For our ocatahedron where each triangle produces a rotation of \(R\), we’d get \(R^8\).

4.3 The torus

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

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

This somewhat arbitrary and unfamiliar model of a torus has the helpful property that it is a combinatorial manifold that is somewhat minimal while still being representable by a donut shape. But the donut-shaped version suggests a very different connection than the flat model! Starting with the flat model, we can easily see how to define \(T_1\) by sliding a link rigidly along the page to the link of some adjacent vertex. Then we can see that transport around any loop is the identity and so \(T_2\) is always the identity (together with the homotopy \(\ensuremath{\mathsf{refl}}_\ensuremath{\text{id}}\) from the identity to itself). So if we imagine a way to visit every face like we did for the octahedron, starting and ending at some basepoint \(v\), we expect to see no net rotation at all of \(Tv\). Later we will call this “total curvature 0.”

The donut-shaped torus suggests a different connection, one determined by the embedding in 3-space that we have represented. But the easiest way to think about that bundle and its connection and curvature is to wait until we have a proof of the Poincaré-Hopf theorem, so that we can instead compute with a vector field.

4.4 Existence of connections

How confident can we be that we can always define a connection on an arbitrary combinatorial manifold? Two things make the octahedron example special: the link is a 4-gon at every vertex, and every edge extends to a symmetry of the entire octahedron, embedded 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

If \(T:\ensuremath{\mathbb{M}}\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) is a bundle of mere circles, then a vector field should be a partial function \(T_\bullet:\ensuremath{\mathbb{M}}\to\mathrm{EM_{\bullet}}(\ensuremath{\mathbb{Z}},1)\) that lifts \(T\). In other words, a pointing of some of the fibers. This aligns with the classical picture of a choice of nonzero vector at each point, except for some points where the vector field vanishes. So instead of having a notion corresponding to the full tangent vector space (one candidate for which would be the disk at each point, i.e. \(\mathop{\mathrm{\mathsf{link}}}\) plus its spokes and filler triangles) we are mapping some vertices to their circular fibers, and others to \(\star\). This lets us continue to work with \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) instead of a type of tangent spaces.

Figure 12 illustrates what removing the preimage of \(\star\) looks like. The resulting type is no longer a combinatorial manifold, since it fails the condition about every point having a circular link.

where \(T_\bullet=\overline{T}\circ X\). Note that \(\exp\) is different from \(\ensuremath{\mathrm{pr}}_1\) since it spreads a fiber out onto the manifold. The composition \(\exp\circ X\) is a map \(\ensuremath{\mathbb{M}}\setminus Z\to \ensuremath{\mathbb{M}}\), and can be thought of as the flow of the vector field.

Let’s see a few examples.

5.1 Index of a vector field

Index should be an integer that computes a winding number “of the vector field” around a zero. We can compute an integer from a map by taking its degree, which is a construction we will assume that we have, for example using (Buchholtz & (Favonia), 2018), where they indeed require that degree agrees with winding number for maps \(S^1\to S^1\).

Proof. \(\mathsf{apd}(X_{\mathrm{spin}})(br) = \ensuremath{\mathsf{refl}}_{X_{\mathrm{spin}}(r)}\) and similarly for the other edges and for \(X_{\mathrm{down}}\). So \(\mathsf{apd}\) on the loop around the equator is the identity, which has index 1. ◻

If these vector fields both have index +1, what does index –1 look like? We can see an example on the torus with its downward vector field.

On the torus we can also consider both a spinning vector field and a downward vector field. Figure 15 shows one way to spin the torus, and in this case there are no zeros so the index is the degree of a map from the empty set, which is 0 (as it factors through a constant map).

Figure 16 shows a downward flow with four zeros. Although this is a picture of the flat torus, the vector field is derived from the shape of Figure 10 where we actually have a notion of up and down. We see at the position labeled (outer, top of diamonds), i.e. the top of the torus, an everywhere outward pointing vector field. At (outer, bottom of diamonds) we see an inward pointing vector field. But at (hole, top of diamonds), i.e. the top of the hole, we see something else. Imagine transport from the neighbor to the lower right to the neighbor below, then continuing clockwise around the link. If we assume that we define \(\mathsf{apd}\) on these edges to be counterclockwise rotation, then transport around the whole link has degree –1. Similarly for the zero at (hole, bottom of diamonds). Adding these four indexes we again get 0.

Summarizing what we’ve seen in our examples, vector fields with isolated zeros have an index, and this index tracks with the total curvature, and the Euler characteristic.

5.2 Equality of total index and total curvature

Here we are inspired by the classical proof of Hopf (Hopf, 1983), presented in detail in Needham (Needham, 2021).

Proof. The algorithm that visits each face in order always starts and ends at \(a\) and so we can skip any faces we wish, to obtain an ordering of face constructors for the remaining union of faces. ◻

Note that on \(\ensuremath{\mathbb{M}}\setminus Z\) the vector field \(X\) trivializes the bundle by mapping into the contractible type of pointed types over \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\). So \(X\simeq Y:\ensuremath{\mathbb{M}}\setminus Z\to (Ta,a)\), the fixed pointed circle in the fiber of the basepoint \(a\).

Proof. The ordering of faces \(\{f_i\}-\{f_{zk}\}\) provides an ordering of all the edges, say \(\{e_l\}\). Each edge appears an even number of times in this list, traversed in opposite directions, except those bounding a replacement face. These replacement-bounding edges are traversed an odd number of times and can be concatenated to traverse the boundary counterclockwise. Concatenation of paths in \(S^1\) is abelian, so \(Y(\{e_l\})\) cancels except on the boundary of the replacement faces, which gives a map from the disjoint union of boundary circles to \(Ta\), with each boundary circle traversed in the counterclockwise direction. The orientation gives the minus sign. ◻

Consider now the total face \(f_{\ensuremath{\mathbb{M}}_Z}\) of \(\ensuremath{\mathbb{M}}_Z\) and its ordering of faces \(\{f_i\}\). \(Y\) is only defined on some of these faces. We will define a new function on all the \(\{f_i\}\).

Because \(\mathsf{apd}\) uses both transport and the value of the vector field, it couples the connection with the vector field, hence the name. Of course in HoTT this coupling is built into the definition of \(\mathsf{apd}\), so that’s another reminder that we aren’t straying far from the foundations to find these geometrical concepts.

The fact that \(C\) is defined on all the faces, by using the value of the vector field only on the 1-skeleton of \(\ensuremath{\mathbb{M}}_Z\) where it was always defined, lets us make the final part of the argument.

Proof. The data of the total face provides an ordering of all the edges. Each edge appears an even number of times, traversed in opposite directions, including the edges in the replacement faces. Concatenation of paths in the polygon \(Ta\) is abelian, so the paths all cancel. ◻

\(C\) is similar to \(X\) and \(Y\) except that it is a total function. On any given edge it computes a path, that is, a homotopy from the function \(\mathsf{tr}\) to the function \(X\), which we can call “the difference between transport and the vector field on that edge.” We have found a way to add all these homotopies together to get 0. We can call this total “the difference between the total index and the total curvature.”

Recall now that we made some arbitrary choices in Definition 26 of an enumeration, and hence the function \(C\). But since \(C\) is unconditionally constant, the space of extra data is contractible.

The last step is to link this value to the Euler characteristic.

5.3 Identification with Euler characteristic

Here we only point the way. Combinatorial manifolds are intuitive objects that connect directly to the classical definition of Euler characteristic. We can argue using Morse theory, the study of smooth real-valued functions on smooth manifolds and their singularities. Classically the gradient of a Morse function is a vector field that can be used to decompose the manifold into its handlebody decomposition. This would be an excellent story to pursue in future work.

Imagine starting with a classical 2-manifold of genus \(g\) that has been triangulated. Stand it upright with the holes forming a vertical sequence. Now install a vector field that points downward whenever possible. This vector field will have a zero at the top and bottom, and one at the top and bottom of each hole. The top and bottom will have zeros of (classical) index 1, and zeros in the holes will have index –1. We include some sketches in the case of a torus (Figure 17). This illustrates how we obtain the formula for genus \(g\): \(\chi(M)=2-2g\). If we choose the triangulation so that the zeros are at vertices, we should be able to import that data into \(\mathsf{CombMfd_2}\) and reproduce the computation using the tools in this note.