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})!.

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

• DomMulAct.stabilizerEquiv_invFun g a = ↑((g (f a)) { val := a, property := ⋯ })

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) { val := a, property := h })

theorem DomMulAct.comp_stabilizerEquiv_invFun {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (i : ι) → Equiv.Perm { a : α // f a = i }) (a : α) : f (DomMulAct.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 α`)

Equations

• DomMulAct.stabilizerEquiv_invFun_aux g = { toFun := DomMulAct.stabilizerEquiv_invFun g, invFun := DomMulAct.stabilizerEquiv_invFun fun (i : ι) => (g i).symm, left_inv := ⋯, right_inv := ⋯ }

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) { val := a, property := h }) = (DomMulAct.mk.symm ↑(MulOpposite.unop g)) a

theorem DomMulAct.stabilizer_card {α : Type u_1} {ι : Type u_2} (f : α → ι) [Fintype α] [Fintype ι] [DecidableEq α] [DecidableEq ι] : Fintype.card { g : Equiv.Perm α // f ∘ ⇑g = f } = Finset.prod Finset.univ fun (i : ι) => Nat.factorial (Fintype.card { a : α // f a = i })

The cardinality of the type of permutations preserving a function