Commit 2024-01-06 18:06 c99fdac2
View on Github →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 ofp : α → ι
in(Equiv.Perm α)ᵈᵐᵃ
is the set ofg : (Equiv.Perm α)ᵈᵐᵃ
such thatp ∘ (mk.symm g) = p
. The natural equivalence fromstabilizer (Perm α)ᵈᵐᵃ p
to{ g : Perm α // p ∘ g = p }
can be obtained assubtypeEquiv mk.symm (fun _ => mem_stabilizer_iff)
DomMulAct.stabilizerMulEquiv
is theMulEquiv
from the MulOpposite of this stabilizer to the product, fori : ι
, ofEquiv.Perm {a // p a = i}
.- Under
Fintype α
andFintype ι
,DomMulAct.stabilizer_card p
computes the cardinality of the type of permutations preservingp
:Fintype.card {f : Perm α // p ∘ f = p} = ∏ i , (Fintype.card ({a // p a = i})).factorial
Co-Authored by : Junyan Xu junyanxu.math@gmail.com