Subgroup of Equiv.Perm α
preserving a function
Let α
and ι
by types and let f : α → ι
DomMulAct.mem_stabilizer_iff
proves that the stabilizer off : α → ι
in(Equiv.Perm α)ᵈᵐᵃ
is the set ofg : (Equiv.Perm α)ᵈᵐᵃ
such thatf ∘ (mk.symm g) = f
.The natural equivalence from
stabilizer (Perm α)ᵈᵐᵃ f
to{ g : Perm α // p ∘ g = f }
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 // f a = i}
.Under
Fintype α
andFintype ι
,DomMulAct.stabilizer_card p
computes the cardinality of the type of permutations preservingp
:Fintype.card {g : Perm α // f ∘ g = f} = ∏ i, (Fintype.card {a // f a = i})!
.
The invFun
component of MulEquiv
from MulAction.stabilizer (Perm α) f
to the product of the `Equiv.Perm {a // f a = i}
Equations
- DomMulAct.stabilizerEquiv_invFun g a = ↑((g (f a)) ⟨a, ⋯⟩)
Instances For
The invFun
component of MulEquiv
from MulAction.stabilizer (Perm α) p
to the product of the Equiv.Perm {a | f a = i} (as an
Equiv.Perm α`)
Equations
- One or more equations did not get rendered due to their size.
Instances For
The MulEquiv
from the MulOpposite
of MulAction.stabilizer (Perm α)ᵈᵐᵃ f
to the product of the Equiv.Perm {a // f a = i}
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cardinality of the type of permutations preserving a function