How to define polygons (both convex and concave)?

Stream: new members

[Ilmārs Cīrulis]

I'm looking at Wikipedia article about polygon and seeing that I need a 'simple polygon'. Is the wiki's definition okay? Or there's something better?

[Ilmārs Cīrulis]

My definition of (closed simple) polygonal chain:

import Mathlib

structure closed_simple_polygonal_chain (n : ℕ) [NeZero n] where
  points : Fin n → EuclideanSpace ℝ (Fin 2)
  prop1 : ∀ i, points i ≠ points (i + 1)
  prop2 : ∀ i p,
    p ∈ segment ℝ (points i) (points (i + 1)) →
    p ∈ segment ℝ (points (i + 1)) (points (i + 2)) →
    p = points (i + 1)
  prop3 : ∀ i j p, i ≠ j → i ≠ j + 1 → j ≠ i + 1 →
    p ∈ segment ℝ (points i) (points (i + 1)) →
    p ∈ segment ℝ (points j) (points (j + 1)) →
    False

Looks good to me, at least for the start.

Should I prove some case of Jordan curve theorem? Then I should be able talk about the "inside" and "outside" of the polygon in addition to the border.

[Ilmārs Cīrulis]

(It seems that Mathlib is without Jordan curve theorem. How reasonable would be to try to prove this theorem for relative beginner? And, of course, maybe someone is already working on it.)

Edit: Probably not reasonable.

[Jovan Gerbscheid]

This seems related to Geometry.SimplicialComplex, though defining it in terms of that may be tricky.

[Jovan Gerbscheid]

I think your prop3 may be wrong. In the current form it is stronger than prop2.

[Jovan Gerbscheid]

The question is a bit what you actually want to do with the polygons. If you want to compare two polygons for equality, then a structure containing a Fin n → P will give you problems, because ![a,b,c] and ![b,c,a] will give "different" polygons

[Ilmārs Cīrulis]

Yes, prop3 looks wrong. Will fix it.

[Ilmārs Cīrulis]

It needs to exclude cases i = j + 1 and j = i + 1, too. The case of consecutive segments.

[Ilmārs Cīrulis]

Jovan Gerbscheid said:

This seems related to Geometry.SimplicialComplex, though defining it in terms of that may be tricky.

:eyes: At the first moment this structure terrifies me, but I will try to use it.

[Jovan Gerbscheid]

Yeah, I agree it doesn't look very simple. It might be easier to not use it. But if you do want to use it, here's my first stab at defining a polygon:

import Mathlib

namespace Geometry

variable {𝕜 E} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]

def SimplicialComplex.IsSimplePolygon (K : SimplicialComplex 𝕜 E) : Prop :=
  open Classical in
  ∃ n : Nat, ∃ points : Fin (n + 3) → E,
    (Pairwise fun i j ↦ points i ≠ points j) ∧
    K.facets = Set.range fun i ↦ {points i, points (i + 1)}

Note that the file defining SimplicialComplex has a TODO about generalizing it to affine spaces, which would be needed to use it for euclidean geometry.

[Ilmārs Cīrulis]

If I use the definition with 𝕜 = ℝ and E = EuclideanSpace ℝ (Fin 2), does it fail in some way?

[Jovan Gerbscheid]

Yeah, EuclideanSpace ℝ (Fin 2) doesn't have a 0, but E needs to be an AddCommGroup. That's the point of a space being affine: it has no fixed zero point.

[Weiyi Wang]

I didn't read the context but EuclideanSpace ℝ (Fin 2) does have a 0?

import Mathlib
example : EuclideanSpace ℝ (Fin 2) := 0

[Jovan Gerbscheid]

Oh sorry my bad.

[Ilmārs Cīrulis]

Yes, it seems I got it. If we use affine space then E can't be AddCommGroup because there's no zero. So the definition has to be upgraded somehow.

[Aaron Liu]

seems to be convexHull that needs generalizing

[Jovan Gerbscheid]

Indeed, and I think for that we need to generalize Convex, which is awaiting the new definition of ConvexSpace in #Is there code for X? > convex combinations?

[Aaron Liu]

did we have an old definition of ConvexSpace?

[Jovan Gerbscheid]

No

[Ilmārs Cīrulis]

Is using affine space necessary (to generalize, probably?), if I want to talk about polygons?

If affirmative, then I could use Euclidean space for now and wait for the upgrade, and then update my definitions and proofs.

[Jovan Gerbscheid]

Yes, I think you should be able to do everying for EuclideanSpace for the short term. And then later it shouldn't be too hard to generalize them. Or rather, you could do it for 2-dimensional real vector spaces.

[Joseph Myers]

I think SimplicialComplex overly complicates things and a polygon should simply be a structure containing Fin n → P for an affine space P (and then you add definitions for all the properties you might want a polygon to have - vertices coplanar, boundary a simple curve, convex, etc., and prove results using the minimum conditions required for each result).

The lack of convexity for affine spaces is not an obstacle here because convexity of sets of points doesn't seem particularly helpful in defining convex polygons. You could define a convex polygon, for example, as one with at least three vertices where, for every two consecutive vertices, all the others are on the same side (AffineSubspace.SSameSide) of the line through those two vertices (which implies the vertices are coplanar, there's no need to restrict to an ambient 2-dimensional space), or many other possible definitions.

Since I want to be able to state problems with conditions of the form "Let ABCDE be a convex pentagon" (where it's definitely meaningful to say that vertex 0 is A, vertex 1 is B, etc., and so to distinguish ABCDE from BCDEA), the consequences for equality of using Fin n → P are exactly what I want.

[Ilmārs Cīrulis]

@Jovan Gerbscheid Apologies for a noob question... Can such polygon, defined as you show, be concave too? Or only convex?

[Jovan Gerbscheid]

The SimplicialComplex requires

• The points of the faces are affine independent (which doesn't mean anything if the faces are up to 1 dimensional)
• For any face, a sub-face is inside. This means that for each edge {i, i+1}, there must also be the singleton faces {i} and {i+1}.
• inter_subset_convexHull, which gives that for any two faces, the intersection of their convex hulls is the convex hull of their intersection. In our case, this means that if two line segments of our polygon intersect, they must actually share an end-point.

So we get that the polygon is not self intersecting, but we don't get that it is convex

[Ilmārs Cīrulis]

Thank you!

[Jovan Gerbscheid]

Oh and the part about affine independence says that it is an implementation detail. I think it might be possible to prove this from the other axioms?