[Merged by Bors] - feat: Tannaka duality for finite groups by ybenmeur · Pull Request #22176 · leanprover-community/mathlib4

ybenmeur · 2025-02-21T21:11:45Z

Proves Tannaka duality for finite groups.

depends on: [Merged by Bors] - feat: lemma eval_of_algHom #23065

github-actions · 2025-02-21T21:12:44Z

PR summary 8db35b4205

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ equiv
+ equivHom_surjective
+ leftRegularFDRepHom
+ ofRightFDRep
+ sumSMulInv
+ sumSMulInv_single_id
+ toRightFDRepComp_in_rightRegular
+ toRightFDRepComp_injective

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

jcommelin · 2025-02-24T09:28:36Z

Hi! It's really cool to see this formalized. Note that your entire proof works verbatim over domains, and mostly even over (nontrivial) commutative rings.
I've just created #22235 for the generalization of FDRep.

See 80f3a63 for the generalization.

Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

Co-authored-by: Johan Commelin <johan@commelin.net>

alreadydone · 2025-04-30T14:20:53Z

+lemma sumSMulInv_single_id [Fintype G] [DecidableEq G] {X : FDRep k G} (v : X) :
+    ∑ s : G, (single 1 1 : G → k) s • (X.ρ s⁻¹) v = v := by


Why are you not using sumSMulInv for the LHS? And can you use Fintype.sum_eq_single in the proof?

Because sumSMulInv is tagged simps. I just tried untagging it and it was slightly worse in my opinion.

alreadydone · 2025-04-30T21:28:16Z

+    apply congrArg f
+    exact mul_assoc ..
+
+lemma toRightFDRepComp_in_rightRegular [IsDomain k] (η : Aut (forget k G)) :


Note to myself: as commented in a previous PR, this works for an "indecomposable (commutative) semiring" k (a typeclass I'm about to introduce). TODO: allow Semiring in FDRep.

alreadydone

Thanks 🎉
maintainer delegate

alreadydone · 2025-05-02T00:39:56Z

+  map_add' _ _ := by
+    simp [add_smul, sum_add_distrib]
+  map_smul' _ _ := by
+    simp [smul_sum, smul_smul]


Suggested change

map_add' _ _ := by

simp [add_smul, sum_add_distrib]

map_smul' _ _ := by

simp [smul_sum, smul_smul]

map_add' _ _ := by simp [add_smul, sum_add_distrib]

map_smul' _ _ := by simp [smul_sum, smul_smul]

alreadydone · 2025-05-02T00:41:48Z

+  have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
+  have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
+  rw [h, ← h2] at h1
+  simpa using congr(Hom.hom $h1 (single 1 1))


Suggested change

simpa using congr(Hom.hom $h1 (single 1 1))

simpa using congr(($h1).hom (single 1 1))

(untested, you might also try without the parentheses)

alreadydone · 2025-05-02T00:43:03Z

+    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
+      congrFun congr((Hom.hom $nat (single u 1))).symm 1
+    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
+      congr($hs ((leftRegular t⁻¹) (single u 1)))


Suggested change

congr($hs ((leftRegular t⁻¹) (single u 1)))

congr($hs (leftRegular t⁻¹ (single u 1)))

alreadydone · 2025-05-02T00:44:34Z

+  calc
+    _ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
+    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
+      congrFun congr((Hom.hom $nat (single u 1))).symm 1


Suggested change

congrFun congr((Hom.hom $nat (single u 1))).symm 1

congr(($nat.symm).hom (single u 1) 1)

(untested)

For some reason this one doesn't work without congrFun. It was also the case when I was using apply_fun.

alreadydone · 2025-05-02T00:45:04Z

+    _ = _ := by
+      by_cases u = t * s <;> simp_all [single_apply]


Suggested change

_ = _ := by

by_cases u = t * s <;> simp_all [single_apply]

_ = _ := by by_cases u = t * s <;> simp_all [single_apply]

alreadydone

Thanks 🎉
maintainer delegate

github-actions · 2025-05-02T00:45:37Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

github-actions · 2025-05-02T00:45:39Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

riccardobrasca · 2025-05-02T01:35:20Z

@erdOne can you also have a look at #23066 (that is a prerequisite to this one)? Thanks!

ybenmeur · 2025-05-02T09:21:01Z

@riccardobrasca #23066 is just the first half of this PR. It was just split to make reviewing potentially easier. I removed the dependency.

mathlib4-dependent-issues-bot · 2025-05-02T09:23:47Z

This PR/issue depends on:

~~[Merged by Bors] - feat: lemma eval_of_algHom #23065~~
By Dependent Issues (🤖). Happy coding!

riccardobrasca · 2025-05-02T14:54:36Z

Thanks!

bors d+

mathlib-bors · 2025-05-02T14:54:38Z

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

ybenmeur · 2025-05-02T16:05:17Z

bors r+

Proves Tannaka duality for finite groups. - [x] depends on: #23065 Co-authored-by: Johan Commelin <johan@commelin.net>

mathlib-bors · 2025-05-02T16:12:22Z

Pull request successfully merged into master.

Build succeeded:

Proves Tannaka duality for finite groups. - [x] depends on: #23065 Co-authored-by: Johan Commelin <johan@commelin.net>

ybenmeur added 6 commits February 21, 2025 18:23

feat: Tannaka duality for finite groups

2fed255

first part

3f05321

fix CI error

1a057b3

second part

7bbbf3c

third part

e15d912

rename

d762416

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 21, 2025

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label Feb 21, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 21, 2025

jcommelin added 2 commits February 24, 2025 10:24

generalize most of the file to commrings

7d4db7c

generalize to domains

80f3a63

meaningful names

90d2c06

ybenmeur added a commit that referenced this pull request Feb 24, 2025

update from #22176

21cc95f

ybenmeur and others added 4 commits February 24, 2025 20:54

fix docstring

410737c

Apply suggestions from code review

f974f9c

Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

Update Mathlib/RepresentationTheory/Tannaka.lean

ca4846e

Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

further simplification

677b3fd

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 25, 2025

Merge remote-tracking branch 'upstream/master' into yb_tannaka3

0fa0947

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 28, 2025

ybenmeur and others added 6 commits March 6, 2025 02:20

Apply suggestions from code review

0c859d2

Co-authored-by: Johan Commelin <johan@commelin.net>

remove one change

edc6a06

attempt to remove changes (with some erw for now)

42b313f

fix

4c844f3

no changes

8a6f4d5

fix

34be1f6

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 8, 2025

Merge branch 'master' into yb_tannaka3

8ffe5c3

ybenmeur added 3 commits April 28, 2025 18:34

Merge remote-tracking branch 'upstream/master' into yb_tannaka3

232d0dd

fix finite/fintype assumptions

f7e6293

details

cebbec0

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 28, 2025

alreadydone reviewed Apr 30, 2025

View reviewed changes

apply review suggestions

da6e937

ybenmeur added a commit that referenced this pull request May 1, 2025

match #22176

2553fe2

alreadydone approved these changes May 2, 2025

View reviewed changes

github-actions Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 2, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 2, 2025

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 2, 2025

last suggestions

8db35b4

mathlib-bors Bot pushed a commit that referenced this pull request May 2, 2025

feat: Tannaka duality for finite groups (#22176)

d516886

Proves Tannaka duality for finite groups. - [x] depends on: #23065 Co-authored-by: Johan Commelin <johan@commelin.net>

mathlib-bors Bot changed the title ~~feat: Tannaka duality for finite groups~~ [Merged by Bors] - feat: Tannaka duality for finite groups May 2, 2025

mathlib-bors Bot closed this May 2, 2025

mathlib-bors Bot deleted the yb_tannaka3 branch May 2, 2025 16:12

pfaffelh pushed a commit that referenced this pull request May 2, 2025

feat: Tannaka duality for finite groups (#22176)

5e1da71

Proves Tannaka duality for finite groups. - [x] depends on: #23065 Co-authored-by: Johan Commelin <johan@commelin.net>

riccardobrasca pushed a commit that referenced this pull request May 7, 2025

feat: Tannaka duality for finite groups (#22176)

b4f15f7

Proves Tannaka duality for finite groups. - [x] depends on: #23065 Co-authored-by: Johan Commelin <johan@commelin.net>

tannerduve pushed a commit that referenced this pull request May 13, 2025

feat: Tannaka duality for finite groups (#22176)

64391d0

Proves Tannaka duality for finite groups. - [x] depends on: #23065 Co-authored-by: Johan Commelin <johan@commelin.net>

		lemma sumSMulInv_single_id [Fintype G] [DecidableEq G] {X : FDRep k G} (v : X) :
		∑ s : G, (single 1 1 : G → k) s • (X.ρ s⁻¹) v = v := by

	simpa using congr(Hom.hom $h1 (single 1 1))
	simpa using congr(($h1).hom (single 1 1))

	congr($hs ((leftRegular t⁻¹) (single u 1)))
	congr($hs (leftRegular t⁻¹ (single u 1)))

	congrFun congr((Hom.hom $nat (single u 1))).symm 1
	congr(($nat.symm).hom (single u 1) 1)

	_ = _ := by
	by_cases u = t * s <;> simp_all [single_apply]
	_ = _ := by by_cases u = t * s <;> simp_all [single_apply]

Conversation

ybenmeur commented Feb 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8db35b4205

Import changes for modified files

Declarations diff

Uh oh!

jcommelin commented Feb 24, 2025

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented May 2, 2025

Uh oh!

github-actions Bot commented May 2, 2025

Uh oh!

riccardobrasca commented May 2, 2025

Uh oh!

ybenmeur commented May 2, 2025

Uh oh!

mathlib4-dependent-issues-bot commented May 2, 2025

Uh oh!

riccardobrasca commented May 2, 2025

Uh oh!

mathlib-bors Bot commented May 2, 2025

Uh oh!

ybenmeur commented May 2, 2025

Uh oh!

mathlib-bors Bot commented May 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

ybenmeur commented Feb 21, 2025 •

edited

Loading

github-actions Bot commented Feb 21, 2025 •

edited

Loading