[Merged by Bors] - feat(linear_algebra/affine_space): affine spaces

[jsm28]

Define (very minimally) affine spaces (as an abbreviation for
add_torsor in the case where the group is a vector space), affine
subspaces, the affine span of a set of points and affine maps.

[jcommelin]

@jsm28 In the future, feel free to remove the changes-requested label once you've addressed comments!

[jcommelin]

Looks pretty good. I left some comments.

[semorrison]

Just noting that everything in this file works if you reduce the hypotheses to

variables (k : Type*) (V : Type*) {P : Type*} [ring k] [add_comm_group V] [module k V]

as long as you change subspace in vector_span to submodule (which is a synonym, in any case).

It seems there's no harm at all in generalising?

[jsm28]

Changed to use ring and module. As noted, the results so far would still be true for semiring and semimodule, but it's less clear if that's useful, and one proof would need to change to use those.

[urkud]

Here is an alternative approach. I'm not sure which one is better but I think that we should discuss the pros and cons of each approach.

1. Define affine_subspace using the following axioms:

structure affine_subspace (k : Type*) (V : Type*) (P : Type*) [ring k] [add_comm_group V]
    [module k V] [affine_space k V P] :=
(carrier : set P)
(add_mem' : ∀ p₁ p₂ p₃ ∈ carrier, (p₂ -ᵥ p₁) +ᵥ p₃ ∈ carrier)
(smul_mem' : ∀ (c : k) (p₁ p₂ ∈ carrier), c • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ carrier)

These axioms are equivalent to yours with two differences:

1. I don't include direction in the data (though it can be reconstructed).
2. I don't require the carrier to be nonempty.

The main "pro" of this approach is that the affine subspaces defined this way form a complete lattice. In particular, the intersection of two affine subspaces is always an affine subspace, you can define affine_span s = Inf {t : affine_subspace k V P | s ⊆ (t : set P)} and have a galois_connection between set P and affine_subspace k V P.

As for direction, there are a few different possibilities:

1. define direction' : with_bot (submodule k V) to be bot for the empty affine space or the set of p1 -ᵥ p2 otherwise.
2. define direction s [nonempty (s : set P)] : submodule k V;
3. define direction s : submodule k V to be the zero submodule for the empty affine space, otherwise as in 1.

Of course, you can add two of these definitions and prove that they agree (look at polynomial.degree vs polynomial.nat_degree).

[semorrison]

This does sounds pretty nice!

@jsm28, you're definitely allowed to include "sounds good, but I don't feel up to attempting this now" in your answer. :-)

[jsm28]

I think that may be my shorter answer, then.

As a longer answer, I suspect there might be use for both types eventually, but the one not requiring nonempty (i.e. sets of points containing all affine combinations) might best be called something other than affine_subspace. That one gives the abstract benefit of the lattice structure, but results in various other complications, and I'm less sure of having practical uses for it (but it may be hard to tell what complications arise with each approach without a lot more implemented that builds on affine subspaces).

Anything involving dimensions is likely to be more complicated with empty subspaces, because an empty space should have dimension -1, but dimensions are also naturally expected to be a nat, or a cardinal in the infinite-dimensional case, and to be the same as the dimension of the submodule that is the direction; dimension 0 is naturally equivalent to having a single point, so if you special-case empty subspaces as also having dimension 0 to keep the types convenient you lose that equivalence. Two subspaces should be parallel iff their directions are equal, but with empty subspaces that doesn't work if the direction has type submodule which would make empty spaces parallel to those with a single point. Without empty subspaces, two subspaces are equal iff they have nonempty intersection and the same direction. With empty subspaces, it's no longer the case that any subspace has an affine frame, and a subspace of dimension n only necessarily has a barycentric frame of n+1 points if your definition allows dimension -1 (and various definitions around barycentric coordinates would probably need special-casing for empty subspaces). Empty subspaces can't be converted to affine spaces on a subtype of points, whereas nonempty ones can.

As a general implementation principle, I hope that most definitions and proofs around affine subspaces and spans can do their main work through the corresponding definitions and results for submodules and spans in modules, rather than needing to repeat any logic that's already present in the module case.

I do know that for geometry I'll want types that build on top of nonempty subspaces by requiring them to have a given dimension, so that e.g. types line k V P or plane k V P can be defined to affine_subspace_n_dim k V P 1 or affine_subspace_n_dim k V P 2 or similar (and whenever a 0-dimensional subspace arises, it will probably be more convenient to convert it back to a point of type P).

I don't right now have any working code outside of this PR that builds on affine subspaces. (I do have code building on affine maps, at a fairly trivial level - constructing an affine_map from an isometry of Euclidean spaces.)

[urkud]

Just to be clear:

• This was a suggestion, i.e. I won't insist at least until I'll need this for some good reason (most probably I won't have a reason to use this part of mathlib in the next several months); if I'll have a good reason, I'll come again and will be ready to do the refactor.
• I do not suggest proving facts about the "bad" empty subspace when it's not convenient. Just add [nonempty (s : set P)] or (hs : (s : set P).nonempty) to any def/lemma.

[jcommelin]

lgtm, shall we get this merged? @urkud @semorrison

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs