Skip to content
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

[Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group #17047

Closed
wants to merge 176 commits into from
Closed

[Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group #17047

wants to merge 176 commits into from

Conversation

AntoineChambert-Loir
Copy link
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Sep 23, 2024 •
edited
Loading

Let α : Type with Fintype α (and DecidableEq α).
The main goal of this file is to compute the cardinality of
conjugacy classes in alternatingGroup α.
Every g : Equiv.Perm α has a cycleType α : Multiset ℕ.
By Equiv.Perm.isConj_iff_cycleType_eq,
two permutations are conjugate in Equiv.Perm α iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

This PR builds on the case of the full permutation group which is treated in #17522

Open in Gitpod

Antoine Chambert-Loir and others added 30 commits December 30, 2023 00:08
initial commit
972be5e
delegate cardinality to ArrowAction
320c553
A working file. Names need to be cleaned up.
e66eedf
adjust Mathlib.lean and import DomMulAct
2b363b8
avoid the use of finite sets
d9fc7f5
update (linter)
6c2e67d
linter (isolated by)
a42782f
delete ArrowAction
99a506c
update (bad ConjAct.toConjAct)
a59e9af
adjust docstring
7c34d07
merge and adjust DomMulAct
02777f8
adjust sections and docstring
ee2a9c4
remove buggy examples, lint100, use factorial notation
9674747
adjust docstring
23f08e6
delete #align lines
13a230c
update following suggestions of jmc
548fbcc
tidy up residues of one #align line
e4344f8
feat: lemmas on permutations, cycles, etc.
efdcff8
add Mathlib.GroupTheory.Perm.ConjAct in Mathlib.lean
1e36ff2
@AntoineChambert-Loir
rw [ConjAct.smul_def]
bd7b7b1
apply RB's suggestions
af58d27
a forgotten one
5a38e91
lint100
842d3ba
update the name of a lemma
5e3c875
update the name of a lemma
455b6a6
use "generalizing" in induction proofs
1501d2b
fix : remove "intro… "
02eb460
@AntoineChambert-Loir
take care of comments by Ruben-VandeVelde
6f8b69a
@AntoineChambert-Loir
move the simp tag after the docstring
6c3fd6f
@riccardobrasca
Merge branch 'master' into ACL/PermLemmas
c740010
@AntoineChambert-Loir AntoineChambert-Loir removed the WIP Work in progress label Feb 7, 2025
ocfnash
ocfnash reviewed Feb 21, 2025
View reviewed changes
Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, these are nice results.

I have left some superficial golfing suggestions and two suggestions for relocating lemmas.

I will do a more thorough review once you've looked at these suggestions.

@ocfnash ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 21, 2025
@AntoineChambert-Loir AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes label Feb 21, 2025
ocfnash
ocfnash reviewed Feb 21, 2025
View reviewed changes
Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Another round of superficial remarks. Unfortunately I'm out of time till tomorrow but I should be able to finish then.

ocfnash
ocfnash reviewed Feb 25, 2025
View reviewed changes
Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few more minor comments. Sorry this is such a fragmented review experience (my time is currently a bit fragmented).

I'm confident I'll run out of nitpicks on my final review.

ocfnash
ocfnash approved these changes Feb 28, 2025
View reviewed changes
Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks so much for all of this!

I have a final round of minor suggestions but otherwise this looks great to me.

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 28, 2025

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

@AntoineChambert-Loir
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2025
@AntoineChambert-Loir @leanprover-community-mathlib4-bot
feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the…
8236a8b 
… centralizer of a permutation in the alternating group (#17047)

Let α : Type with Fintype α (and DecidableEq α).
The main goal of this file is to compute the cardinality of
conjugacy classes in `alternatingGroup α`.
Every g : Equiv.Perm α has a cycleType α : Multiset ℕ.
By Equiv.Perm.isConj_iff_cycleType_eq,
two permutations are conjugate in Equiv.Perm α iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

This PR builds on the case of the full permutation group which is treated in #17522




Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 1, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group [Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group Mar 1, 2025
@mathlib-bors mathlib-bors bot closed this Mar 1, 2025
@mathlib-bors mathlib-bors bot deleted the ACL/ConjClassCount-3 branch March 1, 2025 15:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees
No one assigned
Labels
delegated t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@AntoineChambert-Loir @mathlib4-dependent-issues-bot @ocfnash @joneugster @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot @riccardobrasca