[Merged by Bors] - feat: Scaling of affine bases by YaelDillies · Pull Request #14863 · leanprover-community/mathlib4

YaelDillies · 2024-07-18T09:33:27Z

Given a group G acting on the ring k, provide the G-action over the k-affine bases of a k-module V.

This could be generalised using some IsScalarTower conditions but I'm a bit lazy to sort out exactly what those are and what API we are missing.

github-actions · 2024-07-18T09:34:09Z

PR summary feee1d67b9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ affineIndependent_smul
+ basisOf_smul
+ coord_smul
+ direction_smul
+ instMulAction
+ instSMul
+ instance [SMul G G'] [IsScalarTower G G' V] : IsScalarTower G G' (AffineBasis ι k V)
+ instance [SMulCommClass G G' V] : SMulCommClass G G' (AffineBasis ι k V)
+ mulAction
+ pointwiseSMul
+ pointwiseVAdd
+ reindex_smul
+ smul_bot
+ smul_eq_map
+ smul_mem_smul_iff
+ smul_mem_smul_iff_of_isUnit
+ smul_mem_smul_iff₀
+ smul_span
+ smul_top
+ weightedVSubOfPoint_smul
+ weightedVSub_smul
+ ⟨AffineIndependent.of_smul,
++ coe_smul

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Provide the multiplication action of the units of the ring `k` over the `k`-affine bases of a `k`-module `V`.

Mathlib/LinearAlgebra/AffineSpace/Basis.lean

eric-wieser · 2024-07-19T18:01:27Z

Mathlib/LinearAlgebra/AffineSpace/Basis.lean

+        rw [Pi.smul_def, ← smul_set_range, Units.smul_def, ← AffineSubspace.smul_span, b.tot,
+          AffineSubspace.smul_top a.isUnit] }
+
+@[simp, norm_cast] lemma coe_smul (a : kˣ) (b : AffineBasis ι k V) : ⇑(a • b) = a • ⇑b := rfl


Can you add some lemmas about the other basic operations too, like we did for vadd?

The ones I don't have here are the ones I failed to prove. Feel free to add them yourself though

Mathlib/LinearAlgebra/AffineSpace/Basis.lean

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

eric-wieser · 2024-07-28T20:49:57Z

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

+@[simp] lemma smul_top (ha : IsUnit a) : a • (⊤ : AffineSubspace k V) = ⊤ := by
+  ext x; simpa [smul_eq_map, map_top] using ⟨ha.unit⁻¹ • x, smul_inv_smul ha.unit _⟩
+
+lemma smul_span (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) := map_span _ s


Suggested change

lemma smul_span (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) := map_span _ s

lemma smul_affineSpan (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) := map_span _ s

(unless there is precedent otherwise)

Sadly, there is precedent here: AffineSubspace.span_union. I would like to clean things up but I already have too many things on my plate

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

Mathlib/LinearAlgebra/AffineSpace/Combination.lean

eric-wieser

bors d+

Please fix the PR description before merging, it no longer reflects the state of the PR

mathlib-bors · 2024-08-12T22:29:57Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

YaelDillies · 2024-08-13T08:31:05Z

bors merge

mathlib-bors · 2024-08-13T08:32:15Z

Canceled.

YaelDillies · 2024-08-13T08:32:24Z

bors merge

Given a group `G` acting on the ring `k`, provide the `G`-action over the `k`-affine bases of a `k`-module `V`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2024-08-13T09:26:43Z

Pull request successfully merged into master.

Build succeeded:

Given a group `G` acting on the ring `k`, provide the `G`-action over the `k`-affine bases of a `k`-module `V`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

YaelDillies added the t-euclidean-geometry Affine and axiomatic geometry label Jul 18, 2024

YaelDillies requested a review from eric-wieser July 18, 2024 09:33

YaelDillies mentioned this pull request Jul 18, 2024

[Merged by Bors] - feat: Intercalate a simplex between a point and a neighborhood #14660

Closed

3 tasks

feat: Scaling of affine bases

9e834eb

Provide the multiplication action of the units of the ring `k` over the `k`-affine bases of a `k`-module `V`.

YaelDillies force-pushed the affine_basis_smul branch from e19495c to 9e834eb Compare July 19, 2024 13:59

eric-wieser reviewed Jul 19, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Basis.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 19, 2024

View reviewed changes

generalise to any group action

4a86dda

YaelDillies mentioned this pull request Jul 20, 2024

[Merged by Bors] - feat: add SMul instances to Basis #14945

Closed

1 task

eric-wieser reviewed Jul 26, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Basis.lean Show resolved Hide resolved

YaelDillies and others added 4 commits July 27, 2024 05:17

Merge branch 'master' into affine_basis_smul

2ae7841

basisOf, coord

d825611

remove unused variables

6ebc42d

instances, comment, and TODO

8406c87

eric-wieser reviewed Jul 28, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Basis.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean Outdated Show resolved Hide resolved

eric-wieser and others added 3 commits July 28, 2024 21:52

Update Basis.lean

84e35db

add todo

5454b74

Merge branch 'master' into affine_basis_smul

75b8a97

eric-wieser reviewed Aug 12, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Combination.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Aug 12, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean Outdated Show resolved Hide resolved

generalise to an action by a group

266f8b8

eric-wieser reviewed Aug 12, 2024

View reviewed changes

Mathlib/LinearAlgebra/AffineSpace/Combination.lean Outdated Show resolved Hide resolved

G-generalise

6decaa1

eric-wieser approved these changes Aug 12, 2024

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 12, 2024

Change smul_mem_smul_iff

5d3d05e

style

feee1d6

mathlib-bors bot pushed a commit that referenced this pull request Aug 13, 2024

feat: Scaling of affine bases (#14863)

b113092

Given a group `G` acting on the ring `k`, provide the `G`-action over the `k`-affine bases of a `k`-module `V`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors bot changed the title ~~feat: Scaling of affine bases~~ [Merged by Bors] - feat: Scaling of affine bases Aug 13, 2024

mathlib-bors bot closed this Aug 13, 2024

mathlib-bors bot deleted the affine_basis_smul branch August 13, 2024 09:26

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

feat: Scaling of affine bases (#14863)

a8395d3

Given a group `G` acting on the ring `k`, provide the `G`-action over the `k`-affine bases of a `k`-module `V`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

feat: Scaling of affine bases (#14863)

b6f8045

Given a group `G` acting on the ring `k`, provide the `G`-action over the `k`-affine bases of a `k`-module `V`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024

feat: Scaling of affine bases (#14863)

747d65c

Given a group `G` acting on the ring `k`, provide the `G`-action over the `k`-affine bases of a `k`-module `V`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

	lemma smul_span (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) := map_span _ s
	lemma smul_affineSpan (a : M) (s : Set V) : a • affineSpan k s = affineSpan k (a • s) := map_span _ s

Conversation

YaelDillies commented Jul 18, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 18, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary feee1d67b9

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

eric-wieser Jul 19, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 19, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser Jul 28, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 28, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Aug 12, 2024

Uh oh!

YaelDillies commented Aug 13, 2024

Uh oh!

mathlib-bors bot commented Aug 13, 2024

Uh oh!

YaelDillies commented Aug 13, 2024

Uh oh!

mathlib-bors bot commented Aug 13, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

YaelDillies commented Jul 18, 2024 •

edited

Loading

github-actions bot commented Jul 18, 2024 •

edited

Loading