[Merged by Bors] - feat(GroupTheory/Perm/DomMulAct) : Subgroup of `Equiv.Perm α` preserving a function `p : α → ι` by AntoineChambert-Loir · Pull Request #9342 · leanprover-community/mathlib4

AntoineChambert-Loir · 2023-12-29T22:23:21Z

Subgroup of Equiv.Perm α preserving a function

Let α and ι by types and let p : α → ι

DomMulAct.mem_stabilizer_iff proves that the stabilizer of p : α → ι
in (Equiv.Perm α)ᵈᵐᵃ is the set of g : (Equiv.Perm α)ᵈᵐᵃ such that p ∘ (mk.symm g) = p.

The natural equivalence from stabilizer (Perm α)ᵈᵐᵃ p to { g : Perm α // p ∘ g = p }
can be obtained as subtypeEquiv mk.symm (fun _ => mem_stabilizer_iff)
DomMulAct.stabilizerMulEquiv is the MulEquiv from
the MulOpposite of this stabilizer to the product,
for i : ι, of Equiv.Perm {a // p a = i}.
Under Fintype α and Fintype ι, DomMulAct.stabilizer_card p computes
the cardinality of the type of permutations preserving p :
Fintype.card {f : Perm α // p ∘ f = p} = ∏ i , (Fintype.card ({a // p a = i})).factorial

Co-Authored by : Junyan Xu junyanxu.math@gmail.com

This was written by Junyan Xu after a request on Zulip, https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/permutations.20preserving.20a.20function/near/391930331

It appeared again in
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Cardinality.20of.20permutation/near/410241414

Mathlib/GroupTheory/Perm/ArrowAction.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/GroupTheory/Perm/ArrowAction.lean

AntoineChambert-Loir · 2023-12-29T23:56:21Z

With notation, it is more readable.
The file should be renamed DomMulAct ?

AntoineChambert-Loir · 2023-12-30T01:02:14Z

In the finite case, I added the proof that the cardinality is the product of the factorials.
This is quite short and shows that passing to DomMulAct is not too annoying.

alreadydone · 2023-12-30T07:31:45Z

Mathlib/GroupTheory/Perm/DomMulAct.lean

+theorem stabilizer_card:
+    Nat.card {f : Perm α // p ∘ f = p} =
+      Finset.univ.prod fun i => (Nat.card {a // p a = i}).factorial := by


I think Fintype.card is more appropriate here, since you assumed both α and ι are Fintype, and you have the necessary DecidableEq assumptions. (You could use Finset.card with Finset.filter but that seems uglier.) If you want Nat.card you only need ι to be Fintype, and α just need to be finite.
Also, I think It's better to write the RHS as Π i in ι, ....

i did that. For the proof, however, I have to resort to Nat.card because Fintype.card_congr does not find a necessary Fintype instance.

Question : maybe the namespace should be Equiv.Perm.DomMulAct rather than DomMulAct

I have to resort to Nat.card because Fintype.card_congr does not find a necessary Fintype instance.

Probably because DomMulAct doesn't inherit the Fintype instance?

Does it make sense to add that instance?

eric-wieser · 2023-12-30T19:53:12Z

Mathlib/GroupTheory/Perm/DomMulAct.lean

+
+/-- The cardinality of the type of permutations preserving a function -/
+theorem stabilizer_card:
+    Fintype.card {f : Perm α // p ∘ f = p} =


It's a bit confusing here that p is the function and f is the permutation,

In my mind, p was the projection of a fibration and the permutations are called f all over mathlib.
I'll make the change.

It might be worth waiting for a second opinion; an alterative would be to change the docstring to use the word fibration somehow

I have done it already, that was quick…

AntoineChambert-Loir · 2023-12-30T22:38:28Z

I have been able (I use it elsewhere) to remove the finiteness assumption for the target in the formula for the cardinality.
I can PR it here or do it later when it will be useful…

alreadydone · 2024-01-01T03:45:40Z

remove the finiteness assumption for the target in the formula for the cardinality.

How do you state that? There's tsum but tprod isn't in mathlib yet? Or you just restrict to the finite subset where the fiber is nonempty?

AntoineChambert-Loir · 2024-01-01T12:37:42Z

Yes, I restrict the product to Finset.image f. The proof can be seen in PR #9359, same file

jcommelin

Thanks 🎉

bors merge

…ing a function `p : α → ι` (#9342) Subgroup of `Equiv.Perm α` preserving a function Let `α` and `ι` by types and let `p : α → ι` * `DomMulAct.mem_stabilizer_iff` proves that the stabilizer of `p : α → ι` in `(Equiv.Perm α)ᵈᵐᵃ` is the set of `g : (Equiv.Perm α)ᵈᵐᵃ` such that `p ∘ (mk.symm g) = p`. The natural equivalence from `stabilizer (Perm α)ᵈᵐᵃ p` to `{ g : Perm α // p ∘ g = p }` can be obtained as `subtypeEquiv mk.symm (fun _ => mem_stabilizer_iff)` * `DomMulAct.stabilizerMulEquiv` is the `MulEquiv` from the MulOpposite of this stabilizer to the product, for `i : ι`, of `Equiv.Perm {a // p a = i}`. * Under `Fintype α` and `Fintype ι`, `DomMulAct.stabilizer_card p` computes the cardinality of the type of permutations preserving `p` : `Fintype.card {f : Perm α // p ∘ f = p} = ∏ i , (Fintype.card ({a // p a = i})).factorial` Co-Authored by : Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

mathlib-bors · 2024-01-06T19:17:17Z

Pull request successfully merged into master.

Build succeeded:

initial commit

067cd48

github-actions bot reviewed Dec 29, 2023

View reviewed changes

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

change docstring and indent

798f8ff

github-actions bot reviewed Dec 29, 2023

View reviewed changes

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

Antoine Chambert-Loir added 2 commits December 29, 2023 23:28

update Mathlib.lean

5cb81dd

update indent (again)

5cf1ae9

AntoineChambert-Loir added the awaiting-review label Dec 29, 2023

add docstring to local instance

a3e095c

eric-wieser reviewed Dec 29, 2023

View reviewed changes

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

Update Mathlib/GroupTheory/Perm/ArrowAction.lean

e8ca729

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser reviewed Dec 29, 2023

View reviewed changes

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

eric-wieser reviewed Dec 29, 2023

View reviewed changes

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

alreadydone reviewed Dec 29, 2023

View reviewed changes

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

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

Antoine Chambert-Loir added 3 commits December 30, 2023 00:40

convert to DomMulAct

4b6add9

subtype-ify

b3ec644

Use dma notation

38eb1cd

Antoine Chambert-Loir added 2 commits December 30, 2023 01:56

rename file to DomMulAct, add cardinality

ec75dc6

update docstring

cbe02b2

alreadydone reviewed Dec 30, 2023

View reviewed changes

Antoine Chambert-Loir added 2 commits December 30, 2023 12:02

change to Fintype and use prod notation

c64f96b

Make p argument explicit in DomMulAct.stabilizer_card

dd9f86e

AntoineChambert-Loir mentioned this pull request Dec 30, 2023

[Merged by Bors] - feat: some lemmas on permutation #9359

Closed

4 tasks

eric-wieser reviewed Dec 30, 2023

View reviewed changes

change p to f…

1b01799

factorial notation

ed2e7b5

golfs

6ed6dc2

alreadydone approved these changes Jan 1, 2024

View reviewed changes

AntoineChambert-Loir changed the title ~~feat(GroupTheory/Perm/ArrowAction) : Subgroup of Equiv.Perm α preserving a function p : α → ι~~ feat(GroupTheory/Perm/DomMulAct) : Subgroup of Equiv.Perm α preserving a function p : α → ι Jan 2, 2024

jcommelin approved these changes Jan 6, 2024

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 6, 2024

mathlib-bors bot changed the title ~~feat(GroupTheory/Perm/DomMulAct) : Subgroup of Equiv.Perm α preserving a function p : α → ι~~ [Merged by Bors] - feat(GroupTheory/Perm/DomMulAct) : Subgroup of Equiv.Perm α preserving a function p : α → ι Jan 6, 2024

mathlib-bors bot closed this Jan 6, 2024

mathlib-bors bot deleted the ACL/ArrowAction branch January 6, 2024 19:17

Conversation

AntoineChambert-Loir commented Dec 29, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

AntoineChambert-Loir commented Dec 29, 2023

Uh oh!

AntoineChambert-Loir commented Dec 30, 2023

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!

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!

AntoineChambert-Loir commented Dec 30, 2023

Uh oh!

alreadydone commented Jan 1, 2024

Uh oh!

AntoineChambert-Loir commented Jan 1, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 6, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

AntoineChambert-Loir commented Dec 29, 2023 •

edited

Loading