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
Instances For
    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.
    Instances For
      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.
      Instances For
        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 : αι) [Fintype α] [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)