Commit 2020-06-30 08:06 a143c386View on Github →
refactor(linear_algebra/affine_space): allow empty affine subspaces (#3219)
When definitions of affine spaces and subspaces were added in #2816,
there was some discussion of whether an affine subspace should be
allowed to be empty.
After further consideration of what lemmas need to be added to fill
out the interface for affine subspaces, I've concluded that it does
indeed make sense to allow empty affine subspaces, with
hypotheses then added for those results that need them, to avoid
nonempty hypotheses for other results on affine spans and
intersections of affine subspaces that don't depend on any way on
affine subspaces being nonempty and can be more cleanly stated if they
can be empty.
Thus, change the definition to allow affine subspaces to be empty and
remove the bundled
direction. The new definition of
vector_span of the points in the subspace, i.e. the
submodule.span of the
vsub_set of the points) is the zero
submodule for both empty affine subspaces and for those consisting of
a single point (and it's proved that in the nonempty case it contains
exactly the pairwise subtractions of points in the affine subspace).
This doesn't generally add new lemmas beyond those used in reproving
existing results (including what were previously the
axioms for affine subspaces) with the new definitions. It also
doesn't add the complete lattice structure for affine subspaces, just
helps enable adding it later.