On the area of a spherical triangle

Dear Self,

For future reference: Of course, this is outlined very nicely in Coxeter's Introduction to Geometry, (second edition), but as always the best way to learn math is to re-work it. Here, a proof-sketch without pictures.

By sphere S signify the level set---in some vector space V---of some positive-definite quadratic form; or equivalently the orbit of a generic point under the orthogonal group of the related inner-product. By a central plane signify any hyperplane including the origin and by hemisphere either of the two separated sets of points of S on one side of a central plane. By a convex lune signify the intersection of (at most) two hemispheres.

We now specialize to the vector space R³ with its usual inner-product, wherein central planes will have dimension two and meet any sphere (as defined!) in a circle, which we will call a great circle. The same great circle may also be refered to as the boundary of a hemisphere on either side of the same central plane. By a spherical triangle we will mean a non-empty intersection of three hemispheres such that the great circles that are their boundaries intersect pairwise, but not all three together. We claim without proof that the notion of angle between vectors corresponding to the inner product on R³ induces a notion of angle between hemispheres as well, and thus also an angle measure for lunes such that if a finite set of great circles and pairwise disjoint lunes has union the whole sphere, then the angles of those lunes have sum equal to 2π. Our final unproved claim is that both the property of being a lune and the angle of a lune are invariant under the action of the orthogonal group.

As a triangle ABC is an intersection of three hemispheres A,B,C, so the pairwise intersections of the same three hemispheres are three lunes AB,AC,BC, and the angles of these three lunes shall be called also the angles of the triangle. Related to the three hemispheres are their oposite hemispheres also A',B',C'; as these have the same respective boundaries, substituting any of A',B',C' for A,B,C, respectively, produces eight disjoint triangles (including ABC) --- we will extend the preceding notation for specific lunes and triangles to name these.

A more economical decomposition, however, is into the two disjoint triangles ABC and A'B'C', and the three lunes AB', BC', A'C. (This is a tedious exercise in propositional logic, or an easy picture to draw). Remark that AB and A'B' have the same angle, as have AB' and A'B.
These four lunes are disjoint and, together with the boundaries of A and B, they have union the whole sphere, so the angles of AB and AB' are suplementary. Similarly are the angles BC and BC', AC and A'C. The three lunes AB', BC', A'C, thus have angles summing to 3π less the sum of the angles of ABC. There is no finite set of great circles whose union together with that of the three triangles is the whole sphere; if three lunes orthogonally equivalent to AB', BC', A'C together with one more did give the whole sphere, then the fourth lune must have angle equal to the sum of the angles of ABC less π.

Sometimes a classical geometer