[Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup #9111

utensil · 2023-12-16T16:12:06Z

In this PR, we define lipschitzGroup, pinGroup and spinGroup, and prove some basic lemmas.

Ported from leanprover-community/mathlib3/pull/16040.

Co-authored-by: Jiale Miao [email protected]
Co-authored-by: Eric Wieser [email protected]

This PR is a port of leanprover-community/mathlib3#16040 .

This PR can be reviewed here or discussed on Zulip.

… a new file

…elements

Co-authored-by: Jiale Miao <[email protected]>

Co-authored-by: Eric Wieser <[email protected]>

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean

utensil · 2023-12-17T14:35:12Z

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean

-    simp only [SMul.smul, SetLike.mem_coe, LinearMap.mem_range, DistribMulAction.toLinearMap_apply,
-      ConjAct.ofConjAct_toConjAct] at ha
-    rcases ha with ⟨⟨b, hb⟩, ha1⟩
+    (hx : x ∈ lipschitz Q) : ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) := by


@_Eric Wieser|310045 said:

Having dot notation work on bundled morphisms like this was often convenient in Lean 3; it would be a shame to lose it

@_Yaël Dillies|387244 said:

This is the general issue with bundled morphisms not taking dot notation anymore. This is really annoying.

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T15:57:44Z

Build failed (retrying...):

Build

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T17:32:46Z

Build failed (retrying...):

Build

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T18:47:58Z

Build failed (retrying...):

Build

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T19:19:30Z

Build failed:

Build

eric-wieser · 2024-08-19T20:44:27Z

My personal opinion is that this PR has been in an acceptable state for a(n unacceptably) long time, and that the Subgroup vs Submonoid design choice is not something that should prevent future work from happening. I agree that this can be figured out in a later PR. So...

I agree with this, but didn't find the time to come back and say it. Sorry for letting this drag on so long @utensil!

github-actions · 2024-08-19T20:48:35Z

PR summary 1a12eaa0eb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup`	1258

Declarations diff

+ coe_mem_iff_mem
+ instance : Group (pinGroup Q)
+ instance : Group (spinGroup Q)
+ instance : Inhabited (pinGroup Q)
+ instance : Inhabited (spinGroup Q)
+ instance : Star (pinGroup Q)
+ instance : Star (spinGroup Q)
+ instance : StarMul (pinGroup Q)
+ instance : StarMul (spinGroup Q)
+ involute_eq
+ lipschitzGroup
+ mem_even
+ mem_lipschitzGroup
+ mem_pin
+ mem_unitary
+ pinGroup
+ spinGroup
+ units_involute_act_eq_conjAct
+ units_mem_iff
++ coe_mul_star_self
++ coe_star
++ coe_star_mul_self
++ mem_iff
++ mul_star_self
++ mul_star_self_of_mem
++ star_eq_inv
++ star_eq_inv'
++ star_mem
++ star_mem_iff
++ star_mul_self
++ star_mul_self_of_mem
++ toUnits
++ toUnits_injective
++ units_mem_lipschitzGroup
+++ conjAct_smul_range_ι
+++ conjAct_smul_ι_mem_range_ι
+++ involute_act_ι_mem_range_ι

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.

eric-wieser · 2024-08-19T20:59:41Z

bors merge

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T21:11:30Z

Build failed:

Build

bryangingechen · 2024-08-19T21:50:19Z

Weird, looks like one of the runners went offline before the build finished: https://github.com/leanprover-community/mathlib4/actions/runs/10460865400

Let's try again.
bors r+

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T22:10:53Z

Build failed (retrying...):

Build

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-19T22:11:18Z

Build failed:

Build

bryangingechen · 2024-08-20T00:18:08Z

One of the runners ran out of space. Re-running
bors r+

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

mathlib-bors · 2024-08-20T00:28:49Z

Pull request successfully merged into master.

Build succeeded:

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib3/pull/16040. Co-authored-by: Jiale Miao <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: utensil <[email protected]> Co-authored-by: Utensil <[email protected]>

eric-wieser and others added 10 commits December 15, 2023 13:00

chore(LinearAlgebra/CliffordAlgebra): move results about inversion to…

ecca82c

… a new file

docstring

a8b1c2e

oops

2d5711c

feat(LinearAlgebra/CliffordAlgebra): invertibility of quadratic form …

5b0b2d7

…elements

golf and extra lemmas

609e408

cursed whitespace

043e03d

Initial mathport of leanprover-community/mathlib3#16040

3eb14a6

Co-authored-by: Jiale Miao <[email protected]>

Fix [s]pin_group/clifford_algebra in comments

dad62b9

Reprove invertible_of_invertible_ι

a495508

Co-authored-by: Eric Wieser <[email protected]>

Port to Lean 4, error free

ba1a92e

github-actions bot reviewed Dec 16, 2023

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

lint

c4675b8

github-actions bot reviewed Dec 16, 2023

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

utensil and others added 3 commits December 17, 2023 00:33

reviewdog 🐶

7a94323

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

reviewdog 🐶

76c7ca3

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

reviewdog 🐶

d962d2c

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

github-actions bot reviewed Dec 16, 2023

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

github-actions bot reviewed Dec 16, 2023

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

check that all files are imported

2cea172

utensil changed the title ~~feat: port LinearAlgebra.CliffordAlgebra.SpinGroup~~ feat(LinearAlgebra/CliffordAlgebra): port SpinGroup Dec 16, 2023

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 16, 2023

utensil added 7 commits December 17, 2023 18:30

fix comments and invertibleOfInvertibleι

bd5ae80

[linter.unusedVariables]

7b53507

Replace a simp with simp only

22ec7c9

Remove macro_rules

8cc8431

lint

7ca2725

Improve def and doc of lipschitz

9f4fe7f

synthInstance no longer time out

2edd1b8

utensil commented Dec 17, 2023

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean Outdated Show resolved Hide resolved

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 19, 2024

Merge remote-tracking branch 'origin/master' into utensil/SpinGroup

7b4b7e9

fix errors from new mathlib

1a12eaa

mathlib-bors bot changed the title ~~feat(LinearAlgebra/CliffordAlgebra): port SpinGroup~~ [Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup Aug 20, 2024

mathlib-bors bot closed this Aug 20, 2024

mathlib-bors bot deleted the utensil/SpinGroup branch August 20, 2024 00:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup #9111

[Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup #9111

utensil commented Dec 16, 2023 •

edited

Loading

utensil Dec 17, 2023 •

edited

Loading

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

eric-wieser commented Aug 19, 2024

github-actions bot commented Aug 19, 2024 •

edited

Loading

Declarations diff

eric-wieser commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

bryangingechen commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

bryangingechen commented Aug 20, 2024

mathlib-bors bot commented Aug 20, 2024

[Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup #9111

[Merged by Bors] - feat(LinearAlgebra/CliffordAlgebra): port SpinGroup #9111

Conversation

utensil commented Dec 16, 2023 • edited Loading

utensil Dec 17, 2023 • edited Loading

Choose a reason for hiding this comment

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

eric-wieser commented Aug 19, 2024

github-actions bot commented Aug 19, 2024 • edited Loading

PR summary 1a12eaa0eb

Import changes for modified files

Declarations diff

eric-wieser commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

bryangingechen commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

bryangingechen commented Aug 20, 2024

mathlib-bors bot commented Aug 20, 2024

utensil commented Dec 16, 2023 •

edited

Loading

utensil Dec 17, 2023 •

edited

Loading

github-actions bot commented Aug 19, 2024 •

edited

Loading