Zulip Chat Archive

Stream: maths

Topic: Bundling `direction` into `affine_subspace`


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 15:05):

Of course.

view this post on Zulip 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.

view this post on Zulip 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