The Type of Acute Triangles

This was originally going to be a comment on John’s post about the moduli space of acute triangles, but then it kept growing so I decided to turn it into a post on its own.

In my paper on orbifolds in homotopy type theory, I construct the moduli stack of elliptic curves as the type of pairs (V, \Lambda) where V is a 1d complex vector space and \Lambda is a lattice in V (a rank 2 free abelian subgroup of the additive group of V). I’d like to describe a construction of the moduli stack of acute triangles here, and maybe see if I can figure out how to compare them. I think of this way of doing things as “objective mathematics”, since we will work directly with mathematical objects rather than representatives of them. Another way to think of it would be as “natively categorified”.

So what is an acute triangle? We might as well define a triangle to be three distinct points in a plane, since any three points determine a triangle (if the points are colinear then this is a very degenerate triangle, but that won’t matter because such triangles are obtuse anyway). Two triangles are the same when they are similar; that is, when one can be brought to the other by shifting, rotating, reflecting, or scaling. These operations are precisely the conformal affine symmetries of the plane; those affine transformations of the plane which preserve angles.

If we defined a triangle to be three points in the plane (so that the space of triangles would be the set of injections \{0,1,2\} \hookrightarrow \mathbb{R}^2), we would be adorning the notion with way too much data that breaks the appropriate symmetries. We have given the angles a total ordering; we have given the plane a coordinate system, which endows the triangle with an absolute position, orientation, and size. Instead, we don’t want to order the angles of the triangle — so we should use any three element set T in place of \{0, 1, 2\} — and want to be able to freely move, reflect, and scale triangles in the plane — so we should use an abstract plane A instead of \mathbb{R}^2. But what is an abstract plane?

A good first start it that an abstract plane is a 2d real affine space. There are a few definitions, but the one I will use here is that an affine space is a pair (V, A) of a vector space V and a torsor A for its underlying additive group (this is the first definition on wikipedia). But the symmetries of such an affine space allow for any affine transformation; in other words, we can’t define a triangle to be three distinct points in an affine space, since we could then make any two triangles “similar”. We need to keep track of angles.

The usual way to compute angles in \mathbb{R}^2 is by the formula

\angle(v, w) = \arccos\left(\frac{\langle v \mid w \rangle}{||v|| \cdot ||w ||} \right)

and this relies on the inner product of \mathbb{R}^2. So should we endow our vector space V with an inner product?

Not so fast, a symmetry which preserves the inner product doesn’t just preserve angles — it also preserves lengths. However, if we look closely at the definition of an inner product \langle \cdot \mid \cdot \rangle : V \times V \to \mathbb{R}, we see that it relies only on the fact that \mathbb{R} is an oriented line. In order to say that \langle \cdot \mid \cdot \rangle is bilinear, we need to use the real vector space structure of \mathbb{R}; in order to say that \langle \cdot \mid \cdot \rangle is postive definite, we need to know when a real number is non-negative (or, at least when it is positive). An “oriented line” is a 1d real vector space L equipped with an element p : \pi_0(L - \{0\}) — the connected component of positive elements. We can now define an inner product on V valued in any such L as a bilinear map \langle \cdot \mid \cdot \rangle : V \otimes V \to L which is symmetric and positive definite (by which I will mean both that if \langle v \mid w \rangle = 0 for all w, then v = 0, and that if v is not zero, then \langle v \mid v \rangle \in p). We also get a strict ordering on any oriented line, where y > x means y - x \in p.

(As an aside: this definition makes my constructivity senses nervous. In general, the thinking goes that inner products should really be valued in the upper real — upper Dedekind cuts only — and not the two-sided Dedekind reals. But we are very finite dimensional here, so it should be fine. Of course, to be fully constructive, by “not zero” I should mean “apart from zero”. But then what does this definition have to say about numbers which aren’t apart from zero — if for example we were using the smooth reals instead of the Dedekind reals? We could instead define \bar{p} = \{r\ell \mid r \in [0, \infty),\, \ell \in p\} and then say that \langle v \mid v \rangle \in \bar{p}. We could also avoid using \pi_0 by defining p instead to be a ray. Without knowing what exactly I want to do at the end of the day, its hard to decide between these alternatives. It hardly matters, and they are all classically equivalent.)

In total, an abstract plane will be a triple (V, L, A) of a 2d real vector space V equipped with an inner product in the oriented line L and an affine space A over V. In particular, the symmetries of (\mathbb{R}^2, \mathbb{R}, \mathbb{R}^2) are precisely the affine translations whose linear factor preserves the inner product up to a scalar — the conformal affine translations. Ok, so it’s a little baroque; it would be nice to have a single structure whose symmetries are just the 2d conformal affine group (more on this later), but for now this is what we got.

Now, suppose that (V, L, A) is an abstract plane, which we will meronymically refer to as “A”. A “triangle” in A will be a three element set T together with an injection t : T \hookrightarrow A — that is, an unordered triple of distinct points in A. Given i,j : T, we define the vector t_{ij} : V to be t_j - t_i ("the vector from t_i to t_j). We will say that a triangle is “acute” if for every bijection i : \{0,1, 2\} \cong T, we have that:

\langle t_{i(0)i(1)} \mid t_{i(0)i(1)} \rangle + \langle t_{i(1)i(2)} \mid t_{i(1)i(2)} \rangle > \langle t_{i(0)i(2)} \mid t_{i(0)i(2)} \rangle .

We can now define the type of acute triangles to consist of the tuples (V, L, A , T, t) with the types as above such that t is acute. (It’s perhaps worth noting that degenerate triangles where t is not injective cannot be acute, so we could drop that extra assumption).

But this isn’t quite the moduli stack that John was talking about in his post — and it wouldn’t relate well to the moduli stack of elliptic curves. This is because there’s an extra bit of data missing here: we need to pick our favorite angle in the triangle. So, we pick an angle a : T to get a “pointed triangle”. The type of pointed acute triangles is then the type of tuples (V, L , A, T, t, a).

Now, the type of pointed triangles can be simplified. This is because giving a point (say, t(a)) of the affine space A is equivalent to identifying it with V (via the isomorphism x \mapsto x - t(a)). We are essentially putting t(a) at the origin. This gives us an equivalent type of tuples (V, L, T', t') where T' = T - \{a\} is a two element set and t' : T' \hookrightarrow V - \{0\} is i \mapsto t(i) - t(a). (To be clear, I am describing both the elements of the equivalent type and the equivalence itself as a map (V, L, A, T, t, a) \mapsto (V, L , T', t')).

John describes a map from the upper half plane \mathfrak{h} to the moduli stack of acute triangles; we can describe that as sending \tau : \mathfrak{h} to (\mathbb{C}, \mathbb{R}, \{1, 2\}, [1 \mapsto 1, 2 \mapsto \tau]).

This latter type of pointed acute triangles is the one I want to relate to the moduli stack of elliptic curves. By the moduli stack of elliptic curves, I will mean the type (V, \Lambda) where V is a 1d complex vector space and \Lambda is a lattice in V; the curve itself is actually the abelian group V/\Lambda. I hope these two types are equivalent — but I think one may have a bit more symmetry than the other. Lets see.

It seems obvious that we should keep the “plane” the same, and that the two other points of our triangle should generate our lattice. So, how do we take a pair (L, \langle \cdot \mid \cdot \rangle : V \otimes V \to L) of an oriented line L and an L-valued inner product on V and turn this into a complex structure on V? In fact, we want these two structures to be equivalent!

I’m running out of steam right now, so that’s where I’ll leave it. I would love to hear solutions to the puzzle in the comments!


I wonder if you can get some simplifications here by using complex numbers. A conformal affine symmetry is naturally a pair of complex numbers: a translation and an “amplitwist”, to use the terminology of Visual Complex Analysis. Then the conformal affine group is A = (\mathbb{C}, +) \ltimes (\mathbb{C} \setminus \{0\}, \cdot), and we can define the abstract plane to be a torsor of this. Of course, it doesn’t scale as well to multiple dimensions, but if all you care about is 2-dimensional stuff, it might make your life easier.


Yep, you read my mind! This was what I was thinking when I wrote the parenthetical “(more on this later)”, but I didn’t get around to writing in. I’m gonna pick up with more.

But yeah, basically we could instead define a plane to be a complex affine space. However, we lose out on reflections — which are anti-holomorphic complex affine transformations — though I imagine we can recover them by relabelling our triangle. There’s a bit to think about there. In that case, it is much easier to relate to the type of lattices; we have contracted away the affine space since we point our triangles, and then we just send (V, T', t') \mapsto (V, \{ a t'(i(1)) + bt'(i(2)) \mid a,b : \mathbb{Z},\, i : \{1,2\} \cong T'\}).

Though we need to check that acuteness implies the non-degeneracy of this lattice.

I am still curious about how to relate these two deloopings of the conformal affine group — there must be some construction that relates them…