[Merged by Bors] - feat: Tannaka duality for finite groups #22176

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.

Sign up for GitHub

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

Jump to bottom

Closed

ybenmeur wants to merge 35 commits into master from yb_tannaka3

Collaborator

ybenmeur commented Feb 21, 2025 •

edited

Loading

Proves Tannaka duality for finite groups.

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

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 label

github-actions bot commented Feb 21, 2025 •

edited

Loading

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).

github-actions bot added the t-algebra label

mathlib4-dependent-issues-bot added the blocked-by-other-PR label

jcommelin added 2 commits

February 24, 2025 10:24


          generalize most of the file to commrings

7d4db7c


          generalize to domains

80f3a63

Member

jcommelin commented Feb 24, 2025

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.


          meaningful names

90d2c06

ybenmeur added a commit that referenced this pull request


          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 <[email protected]>


          Update Mathlib/RepresentationTheory/Tannaka.lean

ca4846e

Co-authored-by: smorel394 <[email protected]>


          further simplification

677b3fd

leanprover-community-bot-assistant added the merge-conflict label


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

0fa0947

github-actions bot removed the merge-conflict label

ybenmeur and others added 6 commits

March 6, 2025 02:20


          Apply suggestions from code review

0c859d2

Co-authored-by: Johan Commelin <[email protected]>


          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 label


          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 label

alreadydone reviewed

View reviewed changes

Mathlib/RepresentationTheory/Tannaka.lean Outdated Show resolved Hide resolved

Mathlib/RepresentationTheory/Tannaka.lean Outdated Show resolved Hide resolved

Mathlib/RepresentationTheory/Tannaka.lean

Comment on lines +164 to +165

    
              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

Contributor

alreadydone Apr 30, 2025

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

Collaborator Author

ybenmeur May 1, 2025

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

Mathlib/RepresentationTheory/Tannaka.lean Outdated Show resolved Hide resolved

Mathlib/RepresentationTheory/Tannaka.lean Outdated Show resolved Hide resolved

Mathlib/RepresentationTheory/Tannaka.lean Outdated Show resolved Hide resolved

Mathlib/RepresentationTheory/Tannaka.lean Outdated Show resolved Hide resolved

Mathlib/RepresentationTheory/Tannaka.lean

    
                  apply congrArg f

                  exact mul_assoc ..

              lemma toRightFDRepComp_in_rightRegular [IsDomain k] (η : Aut (forget k G)) :

Contributor

alreadydone Apr 30, 2025

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.


          apply review suggestions

da6e937

ybenmeur added a commit that referenced this pull request


          match #22176

2553fe2

alreadydone approved these changes

View reviewed changes

Contributor

alreadydone left a comment

Thanks 🎉
maintainer delegate

Mathlib/RepresentationTheory/Tannaka.lean Outdated

Comment on lines 157 to 160

    
                map_add' _ _ := by

                  simp [add_smul, sum_add_distrib]

                map_smul' _ _ := by

                  simp [smul_sum, smul_smul]

Contributor

alreadydone May 2, 2025

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]

Mathlib/RepresentationTheory/Tannaka.lean Outdated

    
                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))

Contributor

alreadydone May 2, 2025

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)

Mathlib/RepresentationTheory/Tannaka.lean Outdated

    
                  _ = (η.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)))

Contributor

alreadydone May 2, 2025

Suggested change

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

Mathlib/RepresentationTheory/Tannaka.lean Outdated

    
                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

Contributor

alreadydone May 2, 2025

Suggested change

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

(untested)

Collaborator Author

ybenmeur May 2, 2025

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

Mathlib/RepresentationTheory/Tannaka.lean Outdated

Comment on lines 214 to 215

    
                  _ = _ := by

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

Contributor

alreadydone May 2, 2025

Suggested change

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

alreadydone approved these changes

View reviewed changes

Contributor

alreadydone left a comment

Thanks 🎉
maintainer delegate

github-actions bot commented May 2, 2025

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

github-actions bot added the maintainer-merge label

github-actions bot commented May 2, 2025

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

Member

riccardobrasca commented May 2, 2025

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

Collaborator Author

ybenmeur commented May 2, 2025

@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 removed the blocked-by-other-PR label

Collaborator

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

This PR/issue depends on:

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

Member

riccardobrasca commented May 2, 2025

Thanks!

bors d+

Contributor

mathlib-bors bot commented May 2, 2025

✌️ 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.

leanprover-community-mathlib4-bot added delegated and removed maintainer-merge labels


          last suggestions

8db35b4

Collaborator Author

ybenmeur commented May 2, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request


          feat: Tannaka duality for finite groups (#22176)

d516886

Proves Tannaka duality for finite groups.

- [x] depends on: #23065



Co-authored-by: Johan Commelin <[email protected]>

Contributor

mathlib-bors bot commented May 2, 2025

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~feat: Tannaka duality for finite groups~~ [Merged by Bors] - feat: Tannaka duality for finite groups

mathlib-bors bot closed this

mathlib-bors bot deleted the yb_tannaka3 branch

May 2, 2025 16:12

pfaffelh pushed a commit that referenced this pull request


          feat: Tannaka duality for finite groups (#22176)

5e1da71

Proves Tannaka duality for finite groups.

- [x] depends on: #23065



Co-authored-by: Johan Commelin <[email protected]>

riccardobrasca pushed a commit that referenced this pull request


          feat: Tannaka duality for finite groups (#22176)

b4f15f7

Proves Tannaka duality for finite groups.

- [x] depends on: #23065



Co-authored-by: Johan Commelin <[email protected]>

tannerduve pushed a commit that referenced this pull request


          feat: Tannaka duality for finite groups (#22176)

64391d0

Proves Tannaka duality for finite groups.

- [x] depends on: #23065



Co-authored-by: Johan Commelin <[email protected]>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated new-contributor t-algebra