[Merged by Bors] - feat(algebra/add_torsor): torsors of additive group actions #2720

jsm28 · 2020-05-17T22:43:46Z

Define torsors of additive group actions, to the extent needed for
(and with notation motivated by) affine spaces, to the extent needed
for Euclidean spaces. See
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations
for the discussion leading to this particular structure.

…actions Define torsors of additive commutative group actions, to the extent needed for (and with notation motivated by) affine spaces, to the extent needed for Euclidean spaces. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations for the discussion leading to this particular structure.

src/algebra/add_comm_torsor.lean

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

sgouezel

Nice, thanks!

src/algebra/add_comm_torsor.lean

urkud · 2020-05-18T21:02:26Z

See also https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232720.20torsors

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

jsm28 · 2020-05-19T01:20:56Z

I've made +ᵥ act with the vector on the left and renamed lemmas following the discussion on Zulip.

rwbarton · 2020-05-19T02:23:32Z

I'd like to step back and think about how this fits into the rest of the library. Presumably we will want torsors for a (multiplicative) group at some point, which raises the following questions.

Should additive torsors be related to multiplicative torsors via to_additive? They will satisfy the same basic theorems after all.
Especially if the answer is yes, but also if not, is "vector" really a good name for the group elements at this level of generality? I'm trying to think of other examples where additive notation for a torsor is natural, but one wouldn't call the group elements "vectors". I guess maybe one is the points of a genus one curve?
We have mul_action already, with smul corresponding to vadd, and it seems logical for a multiplicative torsor to extend that. For parallelism, should an additive torsor be split into add_action and add_torsor?

I know these can be annoying questions to think about when you just want to do Euclidean geometry, but otherwise these questions will just come up in the future when it's more difficult to modify the foundations.

jsm28 · 2020-05-19T10:24:28Z

From observation of mathlib development over the past few months, it seems pretty good at large-scale refactorings whenever someone wants to do something that implies refactoring existing code (and the further something is from the foundations, the fewer changes are needed to it in such a refactoring beyond simple renaming of results). Changing names (of lemmas, classes, "vector" and notation) is easy, now (if someone can say what the names should be) or in future, if desired (but don't keep switching back and forth between wanting +ᵥ to act on the left and the right).

src/algebra/add_comm_torsor.lean

jcommelin · 2020-05-19T11:37:48Z

@jsm28 It's possible, but it's usually not so much fun. So if we can avoid such a refactor with a bit of careful planning ahead, I would very much prefer that 😉

jsm28 · 2020-05-19T13:31:22Z

I've now changed this to define separate has_vadd, has_vsub, add_action and add_torsor (with a nonempty field), with those lemmas not needing commutativity no longer needing it (I don't know if the others actually need commutativity, or if it might just be my proofs that do in some cases). Group elements are referred to as such rather than as vectors, but it still uses vadd, vsub, +ᵥ and -ᵥ in the absence of suggested better alternatives.

src/algebra/add_torsor.lean

urkud · 2020-05-25T05:40:33Z

bors merge

Define torsors of additive group actions, to the extent needed for (and with notation motivated by) affine spaces, to the extent needed for Euclidean spaces. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations for the discussion leading to this particular structure.

bors · 2020-05-25T07:23:54Z

Pull request successfully merged into master.

Build succeeded:

The definition of `vsub_set` in `algebra/add_torsor` does something similar to `set.image2`, but expressed directly with `∃` inside `{...}`. Various lemmas in `linear_algebra/affine_space/basic` likewise express such sets of subtractions with a given point on one side directly rather than using `set.image`. These direct forms can be inconvenient to use with lemmas about `set.image2`, `set.image` and `set.range`; in particular, they have the equality inside the binders expressed the other way round, leading to constructs such as `conv_lhs { congr, congr, funext, conv { congr, funext, rw eq_comm } }` when it's necessary to convert one form to the other. The form of `vsub_set` was suggested in review of #2720, the original `add_torsor` addition, based on what was then used in `algebra/pointwise`. Since then, `image2` has been added to mathlib and `algebra/pointwise` now uses `image2`. Thus, convert these definitions to using `image2` or `''` as appropriate, so simplifying various proofs. This PR deliberately only addresses `vsub_set` and related definitions for such sets of subtractions; it does not attempt to change any other definitions in `linear_algebra/affine_space/basic` that might also be able to use `image2` or `''` but are not such sets of subtractions, and does not change the formulations of lemmas not involving such sets even if a rearrangement of equalities and existential quantifiers in some such lemmas might bring them closer to the formulations about images of sets.

…set (#3858) The definition of `vsub_set` in `algebra/add_torsor` does something similar to `set.image2`, but expressed directly with `∃` inside `{...}`. Various lemmas in `linear_algebra/affine_space/basic` likewise express such sets of subtractions with a given point on one side directly rather than using `set.image`. These direct forms can be inconvenient to use with lemmas about `set.image2`, `set.image` and `set.range`; in particular, they have the equality inside the binders expressed the other way round, leading to constructs such as `conv_lhs { congr, congr, funext, conv { congr, funext, rw eq_comm } }` when it's necessary to convert one form to the other. The form of `vsub_set` was suggested in review of #2720, the original `add_torsor` addition, based on what was then used in `algebra/pointwise`. Since then, `image2` has been added to mathlib and `algebra/pointwise` now uses `image2`. Thus, convert these definitions to using `image2` or `''` as appropriate, so simplifying various proofs. This PR deliberately only addresses `vsub_set` and related definitions for such sets of subtractions; it does not attempt to change any other definitions in `linear_algebra/affine_space/basic` that might also be able to use `image2` or `''` but are not such sets of subtractions, and does not change the formulations of lemmas not involving such sets even if a rearrangement of equalities and existential quantifiers in some such lemmas might bring them closer to the formulations about images of sets.

…er-community#2720) Define torsors of additive group actions, to the extent needed for (and with notation motivated by) affine spaces, to the extent needed for Euclidean spaces. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations for the discussion leading to this particular structure.

jsm28 added 4 commits May 17, 2020 22:39

Lower instance priority, as requested by linter failure.

2e2bd72

Fix instance priority of the right instance.

a52db41

Add another cancellation lemma.

4535ce6

urkud reviewed May 18, 2020

View reviewed changes

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

urkud changed the title ~~feat(algebra/add_comm_torsor): torsors of additive commutative group …~~ feat(algebra/add_comm_torsor): torsors of additive commutative group actions May 18, 2020

urkud reviewed May 18, 2020

View reviewed changes

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

jsm28 and others added 2 commits May 18, 2020 11:14

Update src/algebra/add_comm_torsor.lean

76ba361

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Change style of vsub_set implementation, as per PR review.

9b68524

sgouezel reviewed May 18, 2020

View reviewed changes

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

jsm28 and others added 2 commits May 18, 2020 23:38

Update src/algebra/add_comm_torsor.lean

892a41e

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Various changes as per review.

4b4863d

rwbarton reviewed May 19, 2020

View reviewed changes

src/algebra/add_comm_torsor.lean Outdated Show resolved Hide resolved

Restructure to refer to general additive torsors and group elements.

ad457fe

jsm28 changed the title ~~feat(algebra/add_comm_torsor): torsors of additive commutative group actions~~ feat(algebra/add_torsor): torsors of additive group actions May 19, 2020

Complete refactor.

1694bcf

Adjust comment about additive group actions.

034bb38

jsm28 added the awaiting-review The author would like community review of the PR label May 20, 2020

Eliminate remaining unnecessary commutativity assumptions.

7c8355d

urkud reviewed May 22, 2020

View reviewed changes