Documentation

Mathlib.GroupTheory.Perm.DomMulAct

Subgroup of Equiv.Perm α preserving a function

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

theorem DomMulAct.mem_stabilizer_iff {α : Type u_1} {ι : Type u_2} {f : αι} {g : (Equiv.Perm α)ᵈᵐᵃ} :
g MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f f (DomMulAct.mk.symm g) = f
def DomMulAct.stabilizerEquiv_invFun {α : Type u_1} {ι : Type u_2} {f : αι} (g : (i : ι) → Equiv.Perm { a : α // f a = i }) (a : α) :
α

The invFun component of MulEquiv from MulAction.stabilizer (Perm α) f to the product of the `Equiv.Perm {a // f a = i}

Equations
theorem DomMulAct.stabilizerEquiv_invFun_eq {α : Type u_1} {ι : Type u_2} {f : αι} (g : (i : ι) → Equiv.Perm { a : α // f a = i }) {a : α} {i : ι} (h : f a = i) :
DomMulAct.stabilizerEquiv_invFun g a = ((g i) a, h)
theorem DomMulAct.comp_stabilizerEquiv_invFun {α : Type u_1} {ι : Type u_2} {f : αι} (g : (i : ι) → Equiv.Perm { a : α // f a = i }) (a : α) :
def DomMulAct.stabilizerEquiv_invFun_aux {α : Type u_1} {ι : Type u_2} {f : αι} (g : (i : ι) → Equiv.Perm { a : α // f a = i }) :

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.
def DomMulAct.stabilizerMulEquiv {α : Type u_1} {ι : Type u_2} (f : αι) :
(↥(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f))ᵐᵒᵖ ≃* ((i : ι) → Equiv.Perm { a : α // f a = i })

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.
theorem DomMulAct.stabilizerMulEquiv_apply {α : Type u_1} {ι : Type u_2} {f : αι} (g : (↥(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) {a : α} {i : ι} (h : f a = i) :
(((DomMulAct.stabilizerMulEquiv f) g i) a, h) = (DomMulAct.mk.symm (MulOpposite.unop g)) a
theorem DomMulAct.stabilizer_card {α : Type u_1} {ι : Type u_2} (f : αι) [Fintype α] [DecidableEq α] [DecidableEq ι] [Fintype ι] :
Fintype.card { g : Equiv.Perm α // f g = f } = i : ι, (Fintype.card { a : α // f a = i }).factorial

The cardinality of the type of permutations preserving a function

theorem DomMulAct.stabilizer_ncard {α : Type u_1} {ι : Type u_2} (f : αι) [Finite α] [Fintype ι] :
{g : Equiv.Perm α | f g = f}.ncard = i : ι, {a : α | f a = i}.ncard.factorial

The cardinality of the set of permutations preserving a function

theorem DomMulAct.stabilizer_card' {α : Type u_1} {ι : Type u_2} (f : αι) [Fintype α] [DecidableEq α] [DecidableEq ι] :
Fintype.card { g : Equiv.Perm α // f g = f } = iFinset.image f Finset.univ, (Fintype.card { a : α // f a = i }).factorial

The cardinality of the type of permutations preserving a function (without the finiteness assumption on target)