Definition of `affine.simplex`

Stream: maths

[Yury G. Kudryashov]

@Joseph Myers I need degenerate triangles in a project I'm working on. What do you think about making def simplex P n := fin (n + 1) → P, def simplex.independent (K : Type*) [...] (s : simplex P n) := affine_independent K s?

[Yury G. Kudryashov]

This way we can have △ A B C and simplex.map (s : simplex P1 n) (f : affine_map k P1 P2) or even simplex.map (s : simplex P1 n) (f : P1 → P2).

[Joseph Myers]

I don't see the advantage over the unbundled map when degenerate triangles are allowed. The point of simplex is for definitions such as circumcenter that need affine independence (so e.g. centroid is defined for an unbundled function, not for a simplex, because it doesn't need affine independence). Normally when a geometry problem refers to a triangle ABC, it definitely means a nondegenerate one (so with current definitions, you can either declare a hypothesis using triangle and then refer to A, B and C using points, or declare A, B and C as points and then assert affine_independent ℝ ![A, B, C]).

map is simply function composition when there is no requirement of affine independence. (With the present definition of simplex it would be meaningful to define map for an injective affine map, though we don't yet have a lemma to say that injective affine maps preserve affine independence.)

[Yury G. Kudryashov]

There are quite a few theorems and definitions that don't need vertices to be independent: face, barycentric subdivision, subdivision of a triangle into 4 triangles with vertices A, B, C, and midpoints.

[Yury G. Kudryashov]

And in geometry sometimes it makes sense to consider degenerate triangles

[Yury G. Kudryashov]

For subdivisions we can prove theorems about unions and intersections of new simplexes

[Yury G. Kudryashov]

E.g., sometimes the following argument works: the main goal is to prove that some affine function is zero. We prove that it vanishes at many points, some of them correspond to degenerate configurations

[Joseph Myers]

Those all seem like reasonable things to do with an indexed family of points, but we have several different ways to express such an indexed family already when affine independence is not of the essence for what you want to do with the points; simplex is for when it is of the essence and when having affine independence bundled is useful. (Bundled face allows convenient statements of the form "the orthogonal projection of the circumcenter onto a face is the circumcenter of that face". The unbundled version is function composition with mono_of_fin. Or a definition of simplex.medial, that bundles affine independence, would immediately give you t.medial.circumcenter as the nine-point center of a triangle t, without needing to pass affine independence hypotheses around separately.) An indexed family could be a plain function (possibly indexed by a fintype, possibly using a finset of the index type, if finiteness is needed, possibly using fin if it seems useful to bundle the number of points). Or it could be an equiv or embedding if those properties of the function seem important to bundle for particular uses.

I don't know if there might be a use for additional bundled ways of talking about indexed families of points in an affine space (even if it's just another name for the unbundled function to allow some uses of dot notation), but I don't think having more such ways would take away the use of having a type for bundled affinely independent families with a given number of points (i.e. what simplex is at present).