Subgroup of Equiv.Perm α preserving a function

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

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

  The natural equivalence from stabilizer (Perm α)ᵈᵐᵃ f to { g : Perm α // p ∘ g = f } 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 // f a = i}.

• Under Fintype α and Fintype ι, DomMulAct.stabilizer_card p computes the cardinality of the type of permutations preserving p : Fintype.card {g : Perm α // f ∘ g = f} = ∏ i, (Fintype.card {a // f a = i})!.

• Without Fintype ι, DomMulAct.stabilizer_card' p gives an equivalent formula, where the product is restricted to Finset.univ.image f.

theorem DomMulAct.mem_stabilizer_iff {α : Type u_1} {ι : Type u_2} {f : α → ι} {g : (Equiv.Perm α)ᵈᵐᵃ} : g ∈ MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f ↔ f ∘ ⇑(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}

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) : 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 : α) : f (stabilizerEquiv_invFun g a) = f a

def DomMulAct.stabilizerEquiv_invFun_aux {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (i : ι) → Equiv.Perm { a : α // f a = i }) : Equiv.Perm α

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 α`)

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}

theorem DomMulAct.stabilizerMulEquiv_apply {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (↥(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) {a : α} {i : ι} (h : f a = i) : ↑(((stabilizerMulEquiv f) g i) ⟨a, h⟩) = (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 } = ∏ i ∈ Finset.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)