Commit 2024-01-06 18:06 c99fdac2

feat(GroupTheory/Perm/DomMulAct) : Subgroup of Equiv.Perm α preserving 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