# Zulip Chat Archive

## 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