## Stream: maths

### Topic: Bundling direction into affine_subspace

#### Yury G. Kudryashov (Oct 19 2020 at 13:52):

@Joseph Myers @Patrick Massot What do you think about rewriting the definition of affine_subspace in the following way?

structure affine_subspace (k : Type*) {V : Type*} (P : Type*) [ring k] [add_comm_group V]
[module k V] [affine_space V P] :=
(carrier : set P)
(direction : submodule k V)
(vadd_mem_iff' : ∀ (p ∈ carrier) (v), v +ᵥ p ∈ carrier ↔ v ∈ direction)
(nonempty' : direction ≠ ⊥ → carrier.nonempty)


This approach allows us to define subspaces with good defeq properties of direction, and is more consistent with what we do for affine_maps. @Joseph Myers I'm sorry if I was the one who advised against bundling direction when you were writing this part of the library.

#### Patrick Massot (Oct 19 2020 at 14:32):

This should be fine, as long as you provide a function constructing this from the old definition of course.

Of course.

#### Joseph Myers (Oct 19 2020 at 19:21):

I think this should mainly just rearrange details of which lemmas are true by rfl and which actually require something to be proved.

#### Joseph Myers (Oct 19 2020 at 19:23):

You originally suggested unbundled direction along with allowing empty affine subspaces. When I became convinced that empty affine subspaces were indeed useful, I then moved to unbundled direction along with allowing them (but of course you can bundle direction and still allow empty affine subspaces, via nonempty' as you have above).

Last updated: May 09 2021 at 09:11 UTC