Euclidean Geometry

Stream: Is there code for X?

[Adam Millar]

Is there a library or any kind of formalization of Basic Euclidean Geometry?
Like the kind you would find in a high school geometry course.

[Eric Rodriguez]

mathlib has a geometry/euclidean section, but it's quite different to what you'd usually see..

[Adam Millar]

Different indeed.
Going to have to brush up on my linear algebra.
Things around line 370 are closer to what I was looking for.
Thank you.

[Kevin Buzzard]

Here's a student project doing some of Euclid book one in lean: https://ja1941.github.io/hilberts-axioms/ and there are others too. Mathlib's main focus is the kind of mathematics being used and taught in a modern university course so Euclid is not high priority for mathlib, although personally I am looking forward to the day I can take lean into schools and prove the "seven circle theorems" (apparently UK schoolchildren are taught that there are seven, see eg https://www.bbc.co.uk/bitesize/guides/zsw397h/revision/1)

[Kevin Buzzard]

I think that proving these circle theorems would make a really nice game. The main issue to solve is how to make all the geometrically obvious assertions that points are on certain sides of lines easy

[Yaël Dillies]

cc @Bhavik Mehta and his axiomatic geometry

[Adam Millar]

Thank you @Kevin Buzzard and @Yaël Dillies
That is part of my motivation as well. There are some 'non-rigorous' things that bug me in some of the proofs presented, and I was curious exactly how much needs to be done under the hood to formalize it.
I want to find out if it feels rewarding, or if there are just too many cases where 'obvious' things are tedious to prove. :upside_down:

[Damiano Testa]

Proving obvious things should not too bother you too much, when formalizing mathematics... :smile:

[Patrick Massot]

@Adam Millar if you are specifically interested in elementary Euclidean geometry you should have a look at http://geocoq.github.io/GeoCoq/

[Joseph Myers]

My work on orientations is aiming towards defining oriented angles, which should be more convenient for circle theorems and most other uses of angles than the existing unoriented angles because they reduce configuration dependence (e.g. "angles in same segment" and "opposite angles of cyclic quadrilateral" become the same theorem for oriented angles mod π, and to apply that theorem you only need that the points are concyclic and distinct, without needing to be concerned about what order they appear on the circle in). I'm currently expecting to use real.angle (angles mod 2π) for those angles, and, where something is only true mod π, to express it in terms of twice those angles to keep it as an equality of angles mod 2π (not sure if (2:ℤ) • θ or (2:ℕ) • θ is the best expression to use in such statements).

To go from there to separate theorems "angles in same segment" and "opposite angles of cyclic quadrilateral" (whether for unoriented angles, or as equalities mod 2π rather than just mod π for oriented angles) would involve setting up a lot more API to talk about the order in which points appear on circles (probably involving bundled circles and arcs thereof, as distinct from bundled spheres which will be useful for talking about other concepts that work naturally in any dimension). We'll need that API anyway for the IMO Grand Challenge to be able to state those geometry problems that explicitly refer to arcs, cyclic quadrilaterals, etc., but I suspect for most geometry problems not referring to those concepts it will be more convenient to do things in a way with less configuration dependence.

[Kevin Buzzard]

"angle at centre equals twice angle at circumference" also becomes much nicer with oriented angles, although here one has to work mod 2pi

[Bhavik Mehta]

I ported a pretty big section of GeoCoq into lean in the GeoLean branch of mathlib, although mostly following Coq conventions and textbook ordering, rather than mathlib conventions

[Jovan Gerbscheid]

hello @Joseph Myers , I was wondering if triangle similarities will be added to lean, because that seems to be the only thing missing in order to prove IMO geometry problems in Lean. I read that you want to add similarities in a very general form, but the main things needed for IMO problems are angle angle, and side angle side similarities for oriented angles.

[Jovan Gerbscheid]

I also noticed that there is a proof of the isosceles triangle theorem, but if you already have triangle similarity, that can be proven very easily by considering the triangle being similar to itself, with the 2 base points swapped.

[Joseph Myers]

This question raises various issues that I'll discuss in the following order: (A) principles of generality; (B) similarities; (C) triangle lemmas; (D) implementation plans; (E) the overall state of Euclidean geometry in mathlib at present.

[Joseph Myers]

(A) The design of mathlib is that it's a highly integrated library of mathematics as a whole, with everything done in appropriate generality rather than just the particular case of interest for someone's problem. Sometimes we might find it useful to have both more and less general versions of a result, if the less general version is more convenient to apply in practical use cases, and sometimes we might decide a less general version is appropriate to accept (with possible future refactoring) when a more general version is significantly harder to prove, or when we need to develop applications of different versions before it becomes clear what a more general version should look like. But the starting point is that when adding a definition or lemma we work out what the appropriately general version of it is to add (and then a reviewer may point out a further generalization that was missed).

[Joseph Myers]

Euclidean geometry is no exception to this principle of generality. It may be almost a leaf of the import tree (the only import of anything in geometry.euclidean from elsewhere in mathlib proper is that of geometry.euclidean.inversion from analysis.complex.upper_half_plane.metric, and geometry.euclidean.inversion doesn't import any other geometry.euclidean files). But the same principle still applies - and many lemmas used in geometry in fact are proved in more general contexts, such as affine spaces or strictly convex spaces, and thus appear elsewhere in mathlib.

[Joseph Myers]

Thus, for geometry results we consider if there's a more general context they should be stated for - whether that's something more general than just a Euclidean context, or, in the Euclidean case, whether something can e.g. be defined in $n$ dimensions rather than just the two-dimensional case. For example, we define circumcenter for a simplex, not just a triangle, and define the monge_point of a simplex, not just the orthocenter of a triangle (though we prove that in the triangle case, it satisfies the expected orthocenter properties).

[Joseph Myers]

(B) Similarity and congruence results in geometry tend to be analogous, so I'll discuss both together. Typical questions to determine the right form of a particular result include: does it genuinely require three points, or work for more; does it genuinely require those points to be affinely independent, or does it work for a more general family of points? These will determine whether a result should be stated for a general indexed family of points, or more specifically for one that is affinely independent (a simplex, if also required to be finite), or only for three points (a triangle, if required to be affinely independent, or just three points passed as separate hypotheses, if not).

[Joseph Myers]

For example, SSS congruence or similarity will work for any indexed family of points. However, if the family is infinite and its affine span has infinite dimension, you have extra complications. (If we define two indexed families as congruent if there is an isometric equivalence between their spaces that maps one to the other, then two indexed families with the same pairwise distances are congruent if they span the whole of their respective spaces. But even if you only have a single space, in infinite dimensions you could e.g. have one family spanning the whole space and one spanning a subspace such that you can't find such an equivalence.) Those complications serve to justify having a separate version of the lemma, simpler to use, for the common case of families in the same space and indexed by a finite type - but I don't think there's any need to specialize further to a case for simplex or triangle.

[Joseph Myers]

As another example, if you're showing that equal angles imply similarity, that does genuinely need affine independence - or at least it doesn't work for three collinear points, maybe some condition weaker than affine independence suffices. But it's also the case that you don't need to have all angles between all triples of distinct points, if you take just two points and know all the angles at those two points then that's sufficient (and I think instead of affine independence it's enough that no triple of points that includes both of the points at which you're given the angles is collinear). So it's appropriate to state the result with such weaker conditions, and then probably have a special case for simplex (but that special case would still only involve the angles at two points, and not be limited to triangle).

[Joseph Myers]

When results involve oriented angles, they are genuinely limited to a planar context (so if they also involve a simplex, that simplex is a triangle, but they may well make sense for more general indexed families of points in the plane).

[Joseph Myers]

In order to state at all that two indexed families of points are similar, we first need #14315 (Dilations on metric spaces). Once my current open PR #17993 is in, I might look at picking up that old PR and seeing if I can get it ready for inclusion, if no-one else gets there first. I expect there will be lots more to do to make dilations and dilation_class as defined there as conveniently usable as isometries. There will also be work setting up things such as isometry_class and other missing pieces of the API for isometries. That sort of thing might sensibly start by updating Yaël's branch#rename_isometry and getting it into mathlib, as I mentioned in a comment on #14315.

[Joseph Myers]

(C) You remarked on the proof of pons asinorum. geometry.euclidean.triangle is really a very miscellaneous collection of results without much coherent design. Some I added, some other people added; sometimes the main goal was to check something off on Freek's list. I have some thoughts about how to split up and rearrange other geometry files, but don't know what a good arrangement for the current contents of geometry.euclidean.triangle is. Certainly some results should have oriented angle versions added, and quite possibly some unoriented angle results might best be proved via oriented angles; the proofs I added very early on in the development of Euclidean geometry in mathlib may not be the best ones now.

[Joseph Myers]

I suspect incidentally that proving unoriented angle results via oriented angles will be fiddly, given the need to move to a two-dimensional subspace (dealing with degenerate cases where the points are collinear and the ambient space may have less than two dimensions), prove things there and move back (with appropriate lemmas to transport geometrical properties in both directions, which may not currently exist in mathlib). As usual, the principles of generality apply to such lemmas for transporting results to and from a two-dimensional subspace; typically a transport lemma will apply to any similarity or any isometry, with the coercion map from a subtype to the full space being only a special case of that. Maybe the transport process could be simplified with appropriate tactics, but it would be necessary to prove several unoriented angle results using oriented angles by hand before it becomes clear what such a tactic should look like.

[Joseph Myers]

There is, in fact, one ad hoc similarity result for three points in geometry.euclidean.triangle: dist_mul_of_eq_angle_of_dist_mul. Maybe that result would be justified even in a more general context, as a lemma that might well be used in proving the more general forms of similarly results.

[Jovan Gerbscheid]

I think that for IMO problems, an oriented version of triangle similarities is very useful. This requires a concept of similar triangles having either the same orientation, or the opposite orientation, because this determines whether the oriented angles of the triangles are equal to each other, or are negative each other.
I saw there is the definition of the sign of an oriented angle, being 1 if it is in (0, pi) and -1 if it is in (-pi, 0) and 0 otherwise. If you already know that two triangles are similar in an absolute sense, this sign can be used to find the similarity in the oriented sense.
The theorems I would in particular like to have are the following 2, and each has two cases, one for the same orientation, and one for mirrored orientation:
(aa) if 2 triangles share 2 oriented angles, then they are similar. Here it is sufficient to have the given angles modulo pi, instead of modulo 2pi. It requires the 3 points to be affine linearly independent.
(sas) if 2 triangles share an angle and a ratio of side lengths around that angle, they are similar. this does require the angle to be known modulo 2pi, but there is no restriction on the points, and this also includes the case where some of the points coincide. The length ratio just needs to be given as a multiplication, to avoid division by zero.
The proofs of these 2 theorems follow respectively from the uniqueness of the intersection of non-parallel lines, and from the uniqueness of a complex number given the norm and argument. Because in both cases, you can find some distance-ratio preserving map that sends two of the points of one triangle to the corresponding points of the other triangle, and you just need to prove that then the third point also is mapped to the corresponding third point.

[Joseph Myers]

(D) The answer to almost any question about whether mathlib will get some feature is that it depends on whether someone implements it, but that's not very helpful. My current olympiad formalization project is to get all the problems from IMO 2019 into the mathlib archive. After Q2 (#17993) my inclination would be to do the remaining problems in the order Q5, Q3, Q6, but probably not until after the mathlib4 transition is complete; Q5 and Q3 are close to the rising tide of Lean 4 conversion, while Q6, another geometry problem, is a large project. I don't have concrete formalization plans after that; maybe I'll do IMO 2024 problems, maybe I'll do problems on which I was a coordinator, maybe I'll do other problems chosen for their formalization challenges or for the additional API they'll require to be added to mathlib, maybe I'll do pieces of the de facto IMO syllabus without reference to particular problems, maybe I'll take on a non-olympiad formalization project.

[Joseph Myers]

For IMO 2019 Q6 I'd probably go for solution 1 (which might end up involving some similarity results, in that it is using a form of converse of power of a point, which is very close to a combination of (opposite orientation) similar triangles and converse of inscribed angles). There's an extended set of six solutions from the coordinators, in which solution 5 (complex numbers) and solution 6 (a lot more use of similar triangles) might have lower dependencies than solution 1 (which involves developing various projective geometry) - but lower dependencies is not necessarily a feature when doing olympiad formalizations (much of the benefit of such formalizations is the API they result in being added to mathlib proper, see archive/imo/README.md, so arguably it's a good thing to choose a solution to formalize with substantial dependencies not yet in mathlib).

[Joseph Myers]

(E) "the only thing missing in order to prove IMO geometry problems in Lean" is wildly optimistic about the actual level of geometry coverage in mathlib at present. I've done two olympiad geometry problems in Lean (British MO 2020 problem 2, and IMO 2019 problem 2). The specific geometry used in those two solutions is well-covered; the vast bulk of other geometry isn't. Here are some of the many things (other than similarity / congruence definitions and lemmas) that should be added to cover the more basic concepts common in IMO geometry problems and solutions:

[Jovan Gerbscheid]

*actually for the oriented (sas) on triangles ABC and A'B'C', we do require a little bit, namely that A,B are different and A', B' are different, so that we can do the transformation sending A to A' and B to B' in the proof.

[Joseph Myers]

• incenter, excenter, angle bisectors (in $n$ dimensions, so the bisectors are of angles between oriented hyperplanes; I've thought quite a bit about how to set this up, which will involve manipulating orientations of up to three subspaces at the same time);
• tangency between sphere and affine subspace;
• tangency between two spheres;
• Ceva (in an affine space context);
• Menelaus (in an affine space context);
• diameters as an explicit notion, and Thales;
• cyclic polygons, i.e. ordering of points on a circle (see discussion in #16733);
• convex polygons;
• interior of a (not necessarily convex) polygon, or of a simplex (the latter involving more linkage of convexity to affine spaces; when you're dealing with nonconvex polygons a definition is probably based on topology rather than convex hulls);
• lots of things about areas of triangles / volumes of simplexes, via appropriate linkage of geometry to the measure theory parts of mathlib;
• an explicit definition of power of a point and the radical axis;
• various projective geometry, poles and polars,
• a notion of a list of points being in a given (weak or strict) order on a line (generalization to more than three points of the betweenness notions we have; often appears in IMO problem statements).

[Joseph Myers]

Some of those things are straightforward to define and set up API for, some are much more involved. The bulk of IMO problems need some of them; indeed most can't even be stated cleanly without more geometry than we currently have.

[Jovan Gerbscheid]

what do you mean with incenter, excenter, angle bisectors in more than 2 dimensions? is the incenter of a n dimensional simplex the point inside the simplex with equal distance to all n-1 dimensional sides?

[Joseph Myers]

By way of example, this is what I think is needed (and not yet present) just to cleanly state IMO geometry (non-combinatorial) problems from the past 10 years (proofs may well need more). IMO 2013 Q3: excircles / extouch points and tangency. IMO 2013 Q4: diameters. IMO 2014 Q3: convex polygons (quadrilateral), interior of a triangle, tangency. IMO 2014 Q4: I think that one can be stated right now. IMO 2015 Q3: cyclic order of five points on a circle, tangency of circles. IMO 2015 Q4: order of four points on a line. IMO 2016 Q1: angle bisectors. IMO 2017 Q4: diameters, tangency, major and minor arcs. IMO 2018 Q1: major and minor arcs. IMO 2018 Q6: convex quadrilateral and its interior. IMO 2019 Q2: can be stated, but that's because I did about 200 PRs aiming at stating and proving that problem. IMO 2019 Q6: incenter / incircle and tangency / intouch points. IMO 2020 Q1: convex quadrilateral and its interior, angle bisectors. IMO 2021 Q3: interior of a triangle. IMO 2021 Q4: convex quadrilateral, tangency. IMO 2022 Q4: convex pentagon and its interior, order of four points on a line. (End of points A to E above, following remarks are replies to other things in this discussion.)

[Joseph Myers]

For orientation-preserving / reversing similarities, I think Heather had ideas on setting up API to refer to an operation (linear_equiv, affine_equiv, etc.) as orientation-preserving / reversing more conveniently than at present. There are some things about such API that would naturally apply in any dimension (e.g. saying what a homothety with negative scale factor does to the orientation, depending on the parity of the dimension), though results about orientated angles would be two-dimensional.

[Joseph Myers]

Yes, the incenter of a simplex is inside the simplex and has equal distance to all $(n-1)$-dimensional faces. It's the intersection of the internal angle bisectors, where the bisectors in question are $(n-1)$-dimensional subspaces bisecting the angle between two $(n-1)$-dimensional faces. In $n$ dimensions there are up to $2^n$ points equidistant from all the $(n-1)$-dimensional faces. The incenter always exists, and the excenter opposite each vertex always exists. The other generalized excenters may not exist, depending on the choice of simplex (the barycentric coordinates are proportional to plus or minus the volumes of the $(n-1)$-dimensional faces, and if the signed sum is zero, there is no corresponding center for that choice of signs).

Note that if you set up consistent orientations of all the faces, reflecting in an internal angle bisector sends the orientation of one face to the negation of the orientation of the other face adjacent to that angle; it's the external bisector that sends the orientation of one edge to the orientation of the other when you reflect in it. (For example, in two dimensions, a consistent orientation of the edges has arrows cycling round the triangle - so at a vertex, one of the edges is oriented pointing in and one pointing out.)

[Joseph Myers]

Incidentally, there should be a place for the well known SSA congruence/similarity fallacy in mathlib. Correct statements relating the two possible triangles given two sides and an angle not between them would go in mathlib proper, as would variants giving a unique triangle up to congruence under additional hypotheses; these correct versions of SSA are occasionally useful, though not as much as congruent/similar triangles results that don't need such extra conditions. Then the counterexamples directory would be an appropriate place for an explicit construction of two triangles for which it's proved that two sides and an angle not between them are equal in the two triangles, but that the two triangles are not congruent.

[Yaël Dillies]

Joseph Myers said:

For orientation-preserving / reversing similarities, I think Heather had ideas on setting up API to refer to an operation (linear_equiv, affine_equiv, etc.) as orientation-preserving / reversing more conveniently than at present. There are some things about such API that would naturally apply in any dimension (e.g. saying what a homothety with negative scale factor does to the orientation, depending on the parity of the dimension), though results about orientated angles would be two-dimensional.

I think a design akin to docs#ring_hom_comp_triple will help us with orientation of maps.

[Jovan Gerbscheid]

If we want everything to be of the greatest generality, why do we restrict this geometry to real vector spaces? I would think that angles are also possible to define in something like a two dimensional vector space over rational numbers for example (or over any other subfield of R)?

[Jovan Gerbscheid]

*two dimensional inner product spaces

[Jovan Gerbscheid]

Yaël Dillies said:

I think a design akin to docs#ring_hom_comp_triple will help us with orientation of maps.

what sort of design do you mean?

[Yaël Dillies]

See https://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/

[Jovan Gerbscheid]

Joseph Myers said:

For example, SSS congruence or similarity will work for any indexed family of points. However, if the family is infinite and its affine span has infinite dimension, you have extra complications. (If we define two indexed families as congruent if there is an isometric equivalence between their spaces that maps one to the other, then two indexed families with the same pairwise distances are congruent if they span the whole of their respective spaces. But even if you only have a single space, in infinite dimensions you could e.g. have one family spanning the whole space and one spanning a subspace such that you can't find such an equivalence.) Those complications serve to justify having a separate version of the lemma, simpler to use, for the common case of families in the same space and indexed by a finite type - but I don't think there's any need to specialize further to a case for simplex or triangle.

You want to define two sets of points to be congruent if there is an isometry between the whole spaces, mapping one to the other. Maybe it is more convenient to define two sets of point to be congruent if there is an isometry between the respective spans of the two sets of points, mapping one to the other. This is a more general definition and means we can talk about congruence of a triangle in the plane, and a triangle in a higher dimensional space.

[Joseph Myers]

Regarding other inner product spaces, there's a difference between generality that is actually of mathematical interest and generality for generality's sake. Euclidean spaces in dimensions higher than two are legitimate objects of mathematical study; three-dimensional geometry hasn't appeared in post-1979 IMO problems (other than as a setting for combinatorial problems), but mathlib is for mathematics in general, not just the IMO syllabus. Whereas applying the same arguments to a subfield of the reals is of questionable interest, in a very well-defined way: anything you can do there could be done more conveniently by starting with extending the vector space to a real vector space and then working there. (So far mathlib's inner product spaces are only over the reals or the complex numbers.)

(There are cases where the most general form of some definition or result is not uniquely defined, because there are multiple ways to generalize something and they yield different consequences, and in those cases it's appropriate to include multiple generalizations in mathlib.)

[Joseph Myers]

Regarding the definition of congruence, I'd argue that defining in terms of existence of an isometric equivalence between the full spaces is more general than involving spans, because isometric equivalences are meaningful for general metric spaces and affine spans aren't. If you add a definition for mapping an indexed family of points from the ambient space to their span, you can then talk about congruence of the results of applying that operation, in cases where that's the form of congruence you want.

[Jovan Gerbscheid]

Joseph Myers said:

Regarding the definition of congruence, I'd argue that defining in terms of existence of an isometric equivalence between the full spaces is more general than involving spans, because isometric equivalences are meaningful for general metric spaces and affine spans aren't. If you add a definition for mapping an indexed family of points from the ambient space to their span, you can then talk about congruence of the results of applying that operation, in cases where that's the form of congruence you want.

Yes, I agree

[Jovan Gerbscheid]

So we want to define congruence using isometry equivalences, and not affine isometry equivalences, because of the fact that all isometries of real inner product spaces are linear isometries, right?

[Jovan Gerbscheid]

Is there already a proof of this somewhere in mathlib?

[Junyan Xu]

Maybe you could also define a congruence between two family of points $f, g: I \to X$ to mean that $d_X(f(i),f(j))=d_X(g(i),g(j))$ for all $i, j \in I$. If you consider $I$ equipped with the common metric, these are just two isometric embeddings. This gives a sensible definition in infinite-dimensions (without talking about spans) and spaces that are not isotropic/homogeneous like Euclidean spaces.

[Junyan Xu]

Such congruence of distances does appear in the context of comparison triangles (where an arbitrary metric space is compared against a nicely behaved (homogeneous and isotropic) model space (Euclidean space, sphere, or hyperbolic space)), but maybe it's not to be considered a form of congruence. The following pictures are taken from Bridson-Haefliger, Metric Spaces of Non-positive Curvature:
image.png
image.png
image.png
The current triangle APIs in mathlib is probably not developed with this in mind, and I'm not sure how well it generalizes to spheres and hyperbolic spaces.

[Jovan Gerbscheid]

Yes, that seems like a more natural definition to me. And the embeddings can also be in two different metric spaces X and Y.

[Jovan Gerbscheid]

we currently have

def angle (x y : V) : ℝ := real.arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

but I suppose this can be generalized to any metric space using the fact that in all real inner product spaces:

‖x + y‖^2 = ‖x‖^2 + 2 * ⟪x, y⟫ + ‖y‖^2

[Jovan Gerbscheid]

Which gives the same angles as using those comparison triangles

[Jovan Gerbscheid]

In this case all results about congruences generalize to arbitrary metric spaces.

[Yaël Dillies]

You mean normed spaces, right?

[Jovan Gerbscheid]

I think it works even for general metric spaces like this:

def angle' (p₁ p₂ p₃ : P) : ℝ := real.arccos ((dist p₁ p₂)^2 + (dist p₂ p₃)^2 - (dist p₁ p₃)^2 / (2 * (dist p₁ p₂) * (dist p₂ p₃)))

[Yaël Dillies]

But not all congruence results will generalise, because you will need homogeneity at some point.

[Jovan Gerbscheid]

We define what angles are based on the length, so any arguments about angle equalities and length equalities in a triangle implying each other don't care about what the ambient metric space is. We basically define angles so that the cosine rule holds, and then use that to prove SS and SAS congruences. AA will be a bit harder.

[Joseph Myers]

Jovan Gerbscheid said:

So we want to define congruence using isometry equivalences, and not affine isometry equivalences, because of the fact that all isometries of real inner product spaces are linear isometries, right?

Yes. The fact that an isometry of (affine spaces for) real inner product spaces is an affine isometry is a property of strictly convex spaces; see docs#isometry.affine_isometry_of_strict_convex_space (alternatively, since we're talking about isometric equivalences, strict convexity isn't needed and you can use Mazur-Ulam; see docs#isometric.to_real_affine_isometry_equiv).

[Joseph Myers]

I tend to think the definition of congruence in terms of existence of an isometric equivalence is more useful, since it means, for example, that given a congruence from some of the points in a configuration, you can apply that isometry to the whole diagram and start deducing things from there (and likewise for similarities, of course). Ultimately there are two mathematically meaningful concepts (pairwise equal distances, and existence of an isometric equivalence mapping one family of points to the other), and it's a theorem that needs to be proved in mathlib that, in appropriate circumstances (such as the family of points spanning the whole space, or a finite-dimensional subspace when the two spaces are the same), they coincide in Euclidean spaces: that equal distances implies the existence of an isometric equivalence.

[Joseph Myers]

I don't think defining angles in terms of distance like that for general metric spaces is a good idea. It certainly gives the wrong results on the sphere (where the angles in an equilateral triangle depend on its side length), and I doubt it gives good results in hyperbolic space either. Maybe at some point we want a type class for spaces with a notion of angle, so that it can be applied on Riemannian manifolds as well, but the definition wouldn't be the one in this discussion.

[Yaël Dillies]

Isn't there a general definition of angles coming from topological surfaces?

[Jovan Gerbscheid]

I don't see why congruence in terms of existence of an isometric equivalence is more useful, because you can just use the appropriate theorem to create this isometry on the whole diagram when you need it. Congruence in terms of pairwise equal distances seems like a simpler and more general definition, because we can talk about congruence of objects with different dimension ambient spaces. And you won't run into problems with spans in infinite dimensional spaces.

[Yaël Dillies]

How would you state pairwise equal distance? It seems like you would need an equivalence of the base type, sending each point in one family to a prescribed point in the second, and then separately state that the distances are pairwise preserved. Arguably, asking the distance to be preserved everywhere is a simpler definition.

[Jovan Gerbscheid]

I guess on topological surfaces, you can define oriented angles, modulo 2pi, if the surface is orientable, and in general you can define absolute angles, by considering the geodesics (assuming that the geodesic is unique). That uses the definition of (oriented) angles in the plane.

[Joseph Myers]

Existence of an isometric equivalence is more useful in the sense that if you're actually doing anything with congruence in a Euclidean context, you're probably transporting geometrical properties using a result that transports such properties across an isometry, and so you need the isometry. It may not matter so much which gets used as the definition, given that in the general (pseudo)(e)metric space context there's not much that can be said about either congruence concept (mainly that it's an equivalence relation, that congruences are also similarities, etc.), and that in the Euclidean context, the existence of the isometry is one of the most basic results to prove first (probably using docs#euclidean_geometry.inner_weighted_vsub / docs#euclidean_geometry.dist_affine_combination) and then you can use that isometry as needed.

Both concepts are genuinely mathematically meaningful with a mathematically meaningful result to be proved relating them in Euclidean space.

[Joseph Myers]

I think you need a Riemannian metric on your surface, not just a topology, to get meaningful angles.

[Jovan Gerbscheid]

Yaël Dillies said:

How would you state pairwise equal distance? It seems like you would need an equivalence of the base type, sending each point in one family to a prescribed point in the second, and then separately state that the distances are pairwise preserved. Arguably, asking the distance to be preserved everywhere is a simpler definition.

I would take an index type ι, and indexed sets of vertices (v₁ : ι → P₁) (v₂ : ι → P₂), and then require that all the corresponding lengths are the same.

[Joseph Myers]

We don't yet have Riemannian manifolds to define angles there, but there's a recent discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/riemannian.20geometry

[Joseph Myers]

So if you want to define congruent for indexed families of points in terms of pairwise equal distances, and so make SSS congruence a theorem about congruent implying the existence of isometries (for arbitrary indexed families of points in Euclidean space, with appropriate spanning or finite-dimensional conditions - not just for triangles) rather than a theorem saying "equal distances implies congruent", that will probably work reasonably well, since it's still proving sensible results about sensible mathematical concepts. (I don't think "take a relation of angles to distances in Euclidean space and then use that to define angles in other spaces" results in a sensible mathematical concept, however.)

[Jovan Gerbscheid]

For orientational congruence, I think we should implement it as a linear isomorphism of the whole spaces, preserving the points, in finite dimensional real inner product spaces, where the sign of the congruence is equal to the sign of the determinant of the linear map, which is +1 or -1. This generalizes it to higher dimensions, but I don't think there is any further generalization.

[Jovan Gerbscheid]

Do you have suggestions for what notation to use for this, as we want to be able to express congruence for same or opposite orientation. Maybe something like ≅ₒ₊ ≅ₒ₋ for positive and negative sign orientation?

[Jovan Gerbscheid]

Also, is the ≅ symbol for congruence used anywhere else in mathematics, or can we freely use it for congruence?

[Jovan Gerbscheid]

~ is already taken by list permutation equivalence, so for similarity we could take ~ₛ for example? And then the consistent ∼ₒ₊ ∼ₒ₋ for orientational similarity?

[Yaël Dillies]

To take care of the orientation, I reiterate that we should use something akin to docs#semilinear_map_class, where we take a parameter ± 1 so that we can freely compose orientation-preserving and orientation-reversing maps.

[Yaël Dillies]

In fact, I think the current setup is almost what we want already

[Joseph Myers]

I haven't thought in detail about exactly what types for bundled orientation-preserving and orientation-reversing maps should look like; other people here have clearly thought more about that. I will note that for most geometry purposes we're dealing with affine maps, not just linear ones, so you want such versions of affine_isometry_equiv as well as linear_isometry_equiv (and affine_dilation_equiv as well as linear_dilation_equiv once those exist). We do already have a range of lemmas about how linear equivs affect an orientation based on the sign of the determinant.

[Joseph Myers]

Adding those extra types of bundled isometries makes it all the more important to set up all the type classes for bundled isometries so we don't need to duplicate many lemmas for those new bundled types (for which branch#rename_isometry might be a sensible start, even though formally renaming existing definitions related to isometries is independent of adding new ones).

[Yaël Dillies]

Jovan is getting started so I thought I would let him perform the rename himself to get accustomed to the PR process. Hopefully the PR is out soon!

[Jovan Gerbscheid]

I did the renaming, but I didn't have PR rights, and then I couldn't use Gitpod anymore because I had used it too much, so I'd have to do it again once I get everything working with mathlib on my pc.

[Yaël Dillies]

@maintainers, could JovanGerb get mathlib access?

[Riccardo Brasca]

" Already has access to this repository "

[Yaël Dillies]

Ahah :upside_down:

[Jovan Gerbscheid]

thanks!

[Jovan Gerbscheid]

I've formalized the basic (unoriented) congruence cases for triangles, with congruence implemented as written above.
The proofs are as follows: from the definition of angles, we get the cosine rule, from which you can prove the SSS and SAS cases. Then use the cosine rule to prove the sine rule, by expressing the sine in terms of the cosine. Then use this to prove AAS congruence.
This is all in the setting of a general real affine space.

I'm not so familiar with the process, should I create a pull request so that you can see and comment on the code?

[Yaël Dillies]

Yes, pull requests are a great way to gather feedback :smile:

[Jovan Gerbscheid]

From here, we can also add more specific congruences, like SSR for right triangles. And proving the analogous results for triangle similarities will be quite simple, using these congruence results.
When the space is finite dimensional, we'll want to show that the isometry between the two triangles (or general sets of vertices) extends to a linear isometry on the span of the point, and to a linear isometry on the whole spaces. I found the theorem affine_basis.exists_affine_subbasis, which, given an affine spanning set, gives a basis. But what we want here is the more general result that we can restrict to a subset that has the same span and in independent, so I think that should be added there.

[Jovan Gerbscheid]

I was also wondering if there are any ideas about generalizing angles to for example angles between hyperplanes. And maybe oriented angles can be generalized too. But I don't know if this is useful.

[Joseph Myers]

Angles between hyperplanes are complicated because they involve dealing with three orientations at once (for the two hyperplanes and for the two-dimensional subspace used to define the sign of the angles), so there will probably be a lot of API to set up for manipulating orientations of multiple subspaces and how they relate to each other.

[Joseph Myers]

("angles between planes" in undergrad.yaml looks like a questionable translation to me; I'd understand "angles de droites" in the original French as "angles between lines", though I don't know what exact mathematical definition is intended.)

[Yaël Dillies]

Yes, droites ≠ planes, definitely.

[Jovan Gerbscheid]

Ok, I made the pull request

[Jovan Gerbscheid]

We can also define angles between lines, defining a line to be a one dimensional affine subspace. Then an oriented angle between lines would be modulo pi, instead of modulo 2pi. This could help to have a nicer form of theorems that use a silly 2* factor in the modulo 2pi angles.

[Joseph Myers]

The issue with angles mod pi is that then you need lots of extra API: either for an angle_mod_pi type (probably ending up duplicating much of the API for real.angle, as well as providing ways to move between both kinds of angles) or for an eq_mod_pi operation on angles (including various lemmas to allow rewriting by eq_mod_pi inside operands of eq_mod_pi; see discussion in #17993). If adding a new type or definition, there's a trade-off between more convenient API attached to that type or definition and it being more convenient just to use existing types and definitions directly without needing to convert between different pieces of API, and it's not clear if some API for angles mod pi would have sufficient advantages to justify the extra API and converting between the two APIs as needed.

[Jovan Gerbscheid]

If I were to define similarities, what variant of the definition works best? I'd think the most natural is:

∃ r : ℝ, r ≠ 0 → ∀ (i₁ i₂ : ι), (dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂))

but more generally we have

∃ r : ennreal, r ≠ 0 → r ≠ ⊤ → ∀ (i₁ i₂ : ι), (edist (v₁ i₁) (v₁ i₂) = r * edist (v₂ i₁) (v₂ i₂))

[Jovan Gerbscheid]

Or I could make it bundled as a structure with the value of r given, instead of having r in an existential quantifier.

[Jovan Gerbscheid]

for the definition of

def similarity (v₁ : ι → P₁) (v₂ : ι → P₂)
  [pseudo_emetric_space P₁] [pseudo_emetric_space P₂] : Prop :=

[Joseph Myers]

Whatever is done, it should be consistent with whatever form of #14315 (dliations in metric spaces) gets in, which currently indicates using edist and pseudo_emetric_space.

[Joseph Myers]

And it seems like a good idea to get congruences into good shape and into mathlib before starting on similarities, since the API for similarities should end up looking very much like that for congruences.

[Jovan Gerbscheid]

I think that congruence lemmas, and similarity lemmas about triangles should go in the trianlge.lean file, because the angle angle case needs to use the sine rule (which I put in triangle.lean), but conversely, I'd like to change the proof of pons asinorum (in triangle.lean) to use congruence, so that it is much shorter.

[Jovan Gerbscheid]

currently the file is ordered to first have the vector space results, and then the affine results, but this order then wouldn't be possible for the vector form of pons asinorum.

[Jovan Gerbscheid]

or that version can just be omitted

[Jovan Gerbscheid]

Instead of having 6 version of congruence.angle_angle_side and 3 versions of congruence.angle_side_angle, I think it's better to just have 3 versions of similarity.angle_angle and to have a congruence.of_similarity which uses an equal length to turn a similarity into a congruence.

[Jovan Gerbscheid]

Is there a generalization of euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two,
saying that the intersection of 2 spheres is a sphere in an affine subspace?

[Jovan Gerbscheid]

This affine subspace would be the radical axis of the two speres

[Jovan Gerbscheid]

I want to use this property to prove that, in finite dimension, a point is uniquely determined by the distances to the points in a fixed affine spanning set. I think the infinite dimensional version can then be concluded from the finite dimensional one.

[Jovan Gerbscheid]

I'm guessing that that should be proven in the new power.lean file, after defining the power and the radical axis.

[Jovan Gerbscheid]

Jovan Gerbscheid said:

I want to use this property to prove that, in finite dimension, a point is uniquely determined by the distances to the points in a fixed affine spanning set. I think the infinite dimensional version can then be concluded from the finite dimensional one.

I realize now that I can prove this in a different way, so we don't need to have the radical axis quite yet.

[Joseph Myers]

Jovan Gerbscheid said:

I think that congruence lemmas, and similarity lemmas about triangles should go in the trianlge.lean file, because the angle angle case needs to use the sine rule (which I put in triangle.lean), but conversely, I'd like to change the proof of pons asinorum (in triangle.lean) to use congruence, so that it is much shorter.

If it's useful to reorder that file, doing so is reasonable. I think pons asinorum is a basic enough result that it ought to have both vector and affine versions, but that doesn't say which is deduced from which.

[Joseph Myers]

Jovan Gerbscheid said:

Instead of having 6 version of congruence.angle_angle_side and 3 versions of congruence.angle_side_angle, I think it's better to just have 3 versions of similarity.angle_angle and to have a congruence.of_similarity which uses an equal length to turn a similarity into a congruence.

I think for these sorts of unbundled lemmas, it's best to have both congruence versions (set up so people can use them for any ordering of points) and similarity versions (likewise), to make it convenient for people to apply them. Yes, that does mean lots of similar lemma statements.

Now, for bundled isometries and similarities, some duplication can be avoided by having an instance deducing dilation_class from isometry_class, and then any result true for bundled dilations can be stated and proved just once for dilation_class, rather than for both, or, worse, separately for each of the many types of bundled isometries and dilations. But I'm not sure type class inference has a way to handle saying that the same lemma works for both the congruence predicate on two indexed families of points and the corresponding similarity predicate, so I think those get to be stated separately (even if one is proved using the other).

[Joseph Myers]

Jovan Gerbscheid said:

I want to use this property to prove that, in finite dimension, a point is uniquely determined by the distances to the points in a fixed affine spanning set. I think the infinite dimensional version can then be concluded from the finite dimensional one.

I think this could sensibly be deduced from inner_weighted_vsub / dist_affine_combination. Suppose you have a set of points, and two other points P and Q, such that the distances from P to points in the set equal those from Q to points in the set, and also that P lies in the affine span of that set. By dist_affine_combination on an appropriate indexed family of points, the same property holds for distances from P and Q to any point in the affine span of that set (via expressing that point in the affine span as an affine combination, and then dist_affine_combination gives the distance explicitly in terms of the various pairwise distances and the weights in the affine combination). But since we supposed P lies in the affine span, take an affine combination equal to P, and then the distances from P and Q to that combination are equal, so both 0, so P and Q are the same point. Note that nothing depends on the set spanning the whole space; you just need at least one of P and Q to lie in the span of the set to which they have equal distances.