Documentation

Mathlib.GroupTheory.Perm.Cycle.Type

Cycle Types #

In this file we define the cycle type of a permutation.

Main definitions #

Main results #

def Equiv.Perm.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :

The cycle type of a permutation

Equations
  • σ.cycleType = Multiset.map (Finset.card Equiv.Perm.support) σ.cycleFactorsFinset.val
Instances For
    theorem Equiv.Perm.cycleType_def {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    σ.cycleType = Multiset.map (Finset.card Equiv.Perm.support) σ.cycleFactorsFinset.val
    theorem Equiv.Perm.cycleType_eq' {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (s : Finset (Equiv.Perm α)) (h1 : fs, f.IsCycle) (h2 : (↑s).Pairwise Equiv.Perm.Disjoint) (h0 : s.noncommProd id = σ) :
    σ.cycleType = Multiset.map (Finset.card Equiv.Perm.support) s.val
    theorem Equiv.Perm.cycleType_eq {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (l : List (Equiv.Perm α)) (h0 : l.prod = σ) (h1 : σl, σ.IsCycle) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
    σ.cycleType = (List.map (Finset.card Equiv.Perm.support) l)
    @[simp]
    theorem Equiv.Perm.cycleType_eq_zero {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    σ.cycleType = 0 σ = 1
    theorem Equiv.Perm.card_cycleType_eq_zero {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    Multiset.card σ.cycleType = 0 σ = 1
    theorem Equiv.Perm.card_cycleType_pos {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    0 < Multiset.card σ.cycleType σ 1
    theorem Equiv.Perm.two_le_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : } (h : n σ.cycleType) :
    2 n
    theorem Equiv.Perm.one_lt_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : } (h : n σ.cycleType) :
    1 < n
    theorem Equiv.Perm.IsCycle.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) :
    σ.cycleType = [σ.support.card]
    theorem Equiv.Perm.card_cycleType_eq_one {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    Multiset.card σ.cycleType = 1 σ.IsCycle
    theorem Equiv.Perm.Disjoint.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h : σ.Disjoint τ) :
    (σ * τ).cycleType = σ.cycleType + τ.cycleType
    @[simp]
    theorem Equiv.Perm.cycleType_inv {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    σ⁻¹.cycleType = σ.cycleType
    @[simp]
    theorem Equiv.Perm.cycleType_conj {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
    (τ * σ * τ⁻¹).cycleType = σ.cycleType
    theorem Equiv.Perm.sum_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    σ.cycleType.sum = σ.support.card
    theorem Equiv.Perm.card_fixedPoints {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    Fintype.card (Function.fixedPoints σ) = Fintype.card α - σ.cycleType.sum
    theorem Equiv.Perm.sign_of_cycleType' {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    Equiv.Perm.sign σ = (Multiset.map (fun (n : ) => -(-1) ^ n) σ.cycleType).prod
    theorem Equiv.Perm.sign_of_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) :
    Equiv.Perm.sign f = (-1) ^ (f.cycleType.sum + Multiset.card f.cycleType)
    @[simp]
    theorem Equiv.Perm.lcm_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    σ.cycleType.lcm = orderOf σ
    theorem Equiv.Perm.dvd_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : } (h : n σ.cycleType) :
    theorem Equiv.Perm.orderOf_cycleOf_dvd_orderOf {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (x : α) :
    orderOf (f.cycleOf x) orderOf f
    theorem Equiv.Perm.two_dvd_card_support {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : σ ^ 2 = 1) :
    2 σ.support.card
    theorem Equiv.Perm.cycleType_prime_order {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : Nat.Prime (orderOf σ)) :
    ∃ (n : ), σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
    theorem Equiv.Perm.isCycle_of_prime_order {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h1 : Nat.Prime (orderOf σ)) (h2 : σ.support.card < 2 * orderOf σ) :
    σ.IsCycle
    theorem Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {g : Equiv.Perm α} (hf : f g.cycleFactorsFinset) :
    f.cycleType g.cycleType
    theorem Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {g : Equiv.Perm α} (hf : f g.cycleFactorsFinset) :
    (g * f⁻¹).cycleType = g.cycleType - f.cycleType
    theorem Equiv.Perm.isConj_of_cycleType_eq {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h : σ.cycleType = τ.cycleType) :
    IsConj σ τ
    theorem Equiv.Perm.isConj_iff_cycleType_eq {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
    IsConj σ τ σ.cycleType = τ.cycleType
    @[simp]
    theorem Equiv.Perm.cycleType_extendDomain {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] {p : βProp} [DecidablePred p] (f : α Subtype p) {g : Equiv.Perm α} :
    (g.extendDomain f).cycleType = g.cycleType
    theorem Equiv.Perm.cycleType_ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] {p : αProp} [DecidablePred p] {g : Equiv.Perm (Subtype p)} :
    (Equiv.Perm.ofSubtype g).cycleType = g.cycleType
    theorem Equiv.Perm.mem_cycleType_iff {α : Type u_1} [Fintype α] [DecidableEq α] {n : } {σ : Equiv.Perm α} :
    n σ.cycleType ∃ (c : Equiv.Perm α) (τ : Equiv.Perm α), σ = c * τ c.Disjoint τ c.IsCycle c.support.card = n
    theorem Equiv.Perm.le_card_support_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {n : } {σ : Equiv.Perm α} (h : n σ.cycleType) :
    n σ.support.card
    theorem Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two {α : Type u_1} [Fintype α] [DecidableEq α] {n : } {g : Equiv.Perm α} (hn2 : Fintype.card α < n + 2) (hng : n g.cycleType) :
    g.cycleType = {n}
    theorem Equiv.Perm.card_compl_support_modEq {α : Type u_1} [Fintype α] [DecidableEq α] {p : } {n : } [hp : Fact (Nat.Prime p)] {σ : Equiv.Perm α} (hσ : σ ^ p ^ n = 1) :
    σ.support.card Fintype.card α [MOD p]
    theorem Equiv.Perm.card_fixedPoints_modEq {α : Type u_1} [Fintype α] [DecidableEq α] {f : Function.End α} {p : } {n : } [hp : Fact (Nat.Prime p)] (hf : f ^ p ^ n = 1) :

    The number of fixed points of a p ^ n-th root of the identity function over a finite set and the set's cardinality have the same residue modulo p, where p is a prime.

    theorem Equiv.Perm.exists_fixed_point_of_prime {α : Type u_1} [Fintype α] {p : } {n : } [hp : Fact (Nat.Prime p)] (hα : ¬p Fintype.card α) {σ : Equiv.Perm α} (hσ : σ ^ p ^ n = 1) :
    ∃ (a : α), σ a = a
    theorem Equiv.Perm.exists_fixed_point_of_prime' {α : Type u_1} [Fintype α] {p : } {n : } [hp : Fact (Nat.Prime p)] (hα : p Fintype.card α) {σ : Equiv.Perm α} (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) :
    ∃ (b : α), σ b = b b a
    theorem Equiv.Perm.isCycle_of_prime_order' {α : Type u_1} [Fintype α] {σ : Equiv.Perm α} (h1 : Nat.Prime (orderOf σ)) (h2 : Fintype.card α < 2 * orderOf σ) :
    σ.IsCycle
    theorem Equiv.Perm.isCycle_of_prime_order'' {α : Type u_1} [Fintype α] {σ : Equiv.Perm α} (h1 : Nat.Prime (Fintype.card α)) (h2 : orderOf σ = Fintype.card α) :
    σ.IsCycle

    The type of vectors with terms from G, length n, and product equal to 1:G.

    Equations
    Instances For
      theorem Equiv.Perm.VectorsProdEqOne.mem_iff (G : Type u_2) [Group G] {n : } (v : Mathlib.Vector G n) :
      v Equiv.Perm.vectorsProdEqOne G n v.toList.prod = 1
      theorem Equiv.Perm.VectorsProdEqOne.zero_eq (G : Type u_2) [Group G] :
      Equiv.Perm.vectorsProdEqOne G 0 = {Mathlib.Vector.nil}
      theorem Equiv.Perm.VectorsProdEqOne.one_eq (G : Type u_2) [Group G] :
      Equiv.Perm.vectorsProdEqOne G 1 = {1 ::ᵥ Mathlib.Vector.nil}

      Given a vector v of length n, make a vector of length n + 1 whose product is 1, by appending the inverse of the product of v.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Given a vector v of length n whose product is 1, make a vector of length n - 1, by deleting the last entry of v.

        Equations
        Instances For

          Rotate a vector whose product is 1.

          Equations
          Instances For
            theorem exists_prime_orderOf_dvd_card {G : Type u_3} [Group G] [Fintype G] (p : ) [hp : Fact (Nat.Prime p)] (hdvd : p Fintype.card G) :
            ∃ (x : G), orderOf x = p

            For every prime p dividing the order of a finite group G there exists an element of order p in G. This is known as Cauchy's theorem.

            theorem exists_prime_addOrderOf_dvd_card {G : Type u_3} [AddGroup G] [Fintype G] (p : ) [Fact (Nat.Prime p)] (hdvd : p Fintype.card G) :
            ∃ (x : G), addOrderOf x = p

            For every prime p dividing the order of a finite additive group G there exists an element of order p in G. This is the additive version of Cauchy's theorem.

            theorem exists_prime_addOrderOf_dvd_card' {G : Type u_3} [AddGroup G] [Finite G] (p : ) [hp : Fact (Nat.Prime p)] (hdvd : p Nat.card G) :
            ∃ (x : G), addOrderOf x = p
            theorem exists_prime_orderOf_dvd_card' {G : Type u_3} [Group G] [Finite G] (p : ) [hp : Fact (Nat.Prime p)] (hdvd : p Nat.card G) :
            ∃ (x : G), orderOf x = p

            For every prime p dividing the order of a finite group G there exists an element of order p in G. This is known as Cauchy's theorem.

            theorem Equiv.Perm.subgroup_eq_top_of_swap_mem {α : Type u_1} [Fintype α] [DecidableEq α] {H : Subgroup (Equiv.Perm α)} [d : DecidablePred fun (x : Equiv.Perm α) => x H] {τ : Equiv.Perm α} (h0 : Nat.Prime (Fintype.card α)) (h1 : Fintype.card α Fintype.card H) (h2 : τ H) (h3 : τ.IsSwap) :
            H =
            def Equiv.Perm.partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
            (Fintype.card α).Partition

            The partition corresponding to a permutation

            Equations
            Instances For
              theorem Equiv.Perm.parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
              σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1
              theorem Equiv.Perm.filter_parts_partition_eq_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
              Multiset.filter (fun (n : ) => 2 n) σ.partition.parts = σ.cycleType
              theorem Equiv.Perm.partition_eq_of_isConj {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
              IsConj σ τ σ.partition = τ.partition

              3-cycles #

              def Equiv.Perm.IsThreeCycle {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :

              A three-cycle is a cycle of length 3.

              Equations
              • σ.IsThreeCycle = (σ.cycleType = {3})
              Instances For
                theorem Equiv.Perm.IsThreeCycle.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : σ.IsThreeCycle) :
                σ.cycleType = {3}
                theorem Equiv.Perm.IsThreeCycle.card_support {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : σ.IsThreeCycle) :
                σ.support.card = 3
                theorem card_support_eq_three_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
                σ.support.card = 3 σ.IsThreeCycle
                theorem Equiv.Perm.IsThreeCycle.isCycle {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : σ.IsThreeCycle) :
                σ.IsCycle
                theorem Equiv.Perm.IsThreeCycle.sign {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : σ.IsThreeCycle) :
                Equiv.Perm.sign σ = 1
                theorem Equiv.Perm.IsThreeCycle.inv {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} (h : f.IsThreeCycle) :
                f⁻¹.IsThreeCycle
                @[simp]
                theorem Equiv.Perm.IsThreeCycle.inv_iff {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} :
                f⁻¹.IsThreeCycle f.IsThreeCycle
                theorem Equiv.Perm.IsThreeCycle.orderOf {α : Type u_1} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (ht : g.IsThreeCycle) :
                theorem Equiv.Perm.IsThreeCycle.isThreeCycle_sq {α : Type u_1} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (ht : g.IsThreeCycle) :
                (g * g).IsThreeCycle
                theorem Equiv.Perm.isThreeCycle_swap_mul_swap_same {α : Type u_1} [Fintype α] [DecidableEq α] {a : α} {b : α} {c : α} (ab : a b) (ac : a c) (bc : b c) :
                (Equiv.swap a b * Equiv.swap a c).IsThreeCycle
                theorem Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles {α : Type u_1} [Fintype α] [DecidableEq α] {a : α} {b : α} {c : α} (ab : a b) (ac : a c) :
                Equiv.swap a b * Equiv.swap a c Subgroup.closure {σ : Equiv.Perm α | σ.IsThreeCycle}
                theorem Equiv.Perm.IsSwap.mul_mem_closure_three_cycles {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : σ.IsSwap) (hτ : τ.IsSwap) :
                σ * τ Subgroup.closure {σ : Equiv.Perm α | σ.IsThreeCycle}