## Stream: maths

### Topic: Definition of affine.simplex

#### Yury G. Kudryashov (Aug 22 2020 at 15:26):

@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 (Aug 22 2020 at 15:34):

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 (Aug 22 2020 at 15:53):

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 (Aug 22 2020 at 16:09):

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 (Aug 22 2020 at 16:12):

And in geometry sometimes it makes sense to consider degenerate triangles

#### Yury G. Kudryashov (Aug 22 2020 at 16:12):

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

#### Yury G. Kudryashov (Aug 22 2020 at 16:16):

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 (Aug 22 2020 at 18:37):

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).

Last updated: May 11 2021 at 16:22 UTC