-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(linear_algebra/affine_space/affine_subspace/pointwise): Translations are an action on affine subspaces #14230
Conversation
|
… hzhang-affine_space_action
Since we're spliting this off to a new |
Let's try to avoid making multiple refactors at once. That does sound like a reasonable idea for a follow-up PR. |
@YaelDillies @eric-wieser I've fixed the names, lmk if there's anything else |
@YaelDillies @eric-wieser When you guys have time please take a look at this again, thank you! |
Sorry, this might have to wait a week. This looks good overall but I don't have time to agree on the details. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Another good lemma to have would be that the affine span of a pointwise vadd on a set is the same as the pointwise vadd on the span of the set (which should follow immediately from affine_subspace.map_span
)
If it looks good overall, may I have merging permission? 👀 |
exact submodule.map_id _, | ||
end | ||
|
||
lemma pointwise_vadd_span (v : V) {s : set P} : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lemma pointwise_vadd_span (v : V) {s : set P} : | |
lemma pointwise_vadd_span (v : V) (s : set P) : |
@[simp] lemma coe_pointwise_vadd (v : V) (s : affine_subspace k P) : | ||
((v +ᵥ s : affine_subspace k P) : set P) = v +ᵥ s := rfl | ||
|
||
lemma vadd_mem_pointwise_vadd_iff (v : V) {s : affine_subspace k P} {p : P} : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lemma vadd_mem_pointwise_vadd_iff (v : V) {s : affine_subspace k P} {p : P} : | |
lemma vadd_mem_pointwise_vadd_iff {v : V} {s : affine_subspace k P} {p : P} : |
variables {V₁ P₁ V₂ P₂ V₃ P₃ : Type*} | ||
variables [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] | ||
variables [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] | ||
variables [add_comm_group V₃] [module k V₃] [add_torsor V₃ P₃] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is V₃ used here? If not, can you remove all mentions of it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Let's just wait for CI to pass.
✌️ winston-h-zhang can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…ions are an action on affine subspaces (#14230) Co-authored-by: Hanting Zhang <hantingzhang03@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Defines
instance : has_vadd V (affine_subspace k P)
andinstance : add_action V (affine_subspace k P)
of the formp → v +ᵥ p
.I feel like this is really about sub-torsors, but that would require refactoring... :(