[Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group by AntoineChambert-Loir · Pull Request #17047 · leanprover-community/mathlib4

AntoineChambert-Loir · 2024-09-23T10:17:44Z

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

Mathlib/GroupTheory/Perm/Centralizer.lean

ocfnash

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.

Mathlib/GroupTheory/Perm/Centralizer.lean

Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

Mathlib/GroupTheory/Perm/Cycle/Type.lean

ocfnash

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

Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

ocfnash

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.

Mathlib/GroupTheory/NoncommPiCoprod.lean

Mathlib/GroupTheory/Perm/Centralizer.lean

Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

ocfnash

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/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

mathlib-bors · 2025-02-28T11:15:01Z

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

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

AntoineChambert-Loir · 2025-03-01T15:06:38Z

bors r+

… 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>

mathlib-bors · 2025-03-01T15:45:18Z

Pull request successfully merged into master.

Build succeeded:

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

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

take care of comments by Ruben-VandeVelde

6f8b69a

move the simp tag after the docstring

6c3fd6f

Merge branch 'master' into ACL/PermLemmas

c740010

AntoineChambert-Loir commented Feb 6, 2025

View reviewed changes

Mathlib/GroupTheory/Perm/Centralizer.lean Outdated Show resolved Hide resolved

AntoineChambert-Loir added 3 commits February 6, 2025 21:40

use le_centralizer

f5b3521

Update Mathlib/GroupTheory/Perm/Centralizer.lean

e5bbdcd

adjust open

4b68027

AntoineChambert-Loir removed the WIP Work in progress label Feb 7, 2025

ocfnash reviewed Feb 21, 2025

View reviewed changes

ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 21, 2025

AntoineChambert-Loir and others added 2 commits February 21, 2025 17:33

Apply suggestions from code review

53ac61d

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

address remarks of ON

165508b

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 21, 2025

AntoineChambert-Loir commented Feb 21, 2025

View reviewed changes

Mathlib/GroupTheory/Perm/Cycle/Type.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

d6dd1a5

ocfnash reviewed Feb 21, 2025

View reviewed changes

AntoineChambert-Loir and others added 2 commits February 21, 2025 19:40

Apply suggestions from code review

79bd779

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

some simplifications

020dfcb

ocfnash reviewed Feb 25, 2025

View reviewed changes

AntoineChambert-Loir added 3 commits February 27, 2025 17:03

address comments by OFC

64599ec

Merge branch 'master' into ACL/ConjClassCount-3

1dd0e18

adjust to deprecated lemma

551ab56

ocfnash approved these changes Feb 28, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 28, 2025

AntoineChambert-Loir and others added 2 commits March 1, 2025 12:37

Apply suggestions from code review

68a3358

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

simplify, add lemma

cdd62b3

mathlib-bors bot closed this Mar 1, 2025

mathlib-bors bot deleted the ACL/ConjClassCount-3 branch March 1, 2025 15:45

Conversation

AntoineChambert-Loir commented Sep 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 28, 2025

Uh oh!

AntoineChambert-Loir commented Mar 1, 2025

Uh oh!

mathlib-bors bot commented Mar 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

AntoineChambert-Loir commented Sep 23, 2024 •

edited

Loading