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
Instances For
    theorem Equiv.Perm.cycleType_def {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    Equiv.Perm.cycleType σ = Multiset.map (Finset.card Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset σ).val
    theorem Equiv.Perm.cycleType_eq' {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (s : Finset (Equiv.Perm α)) (h1 : fs, Equiv.Perm.IsCycle f) (h2 : Set.Pairwise (s) Equiv.Perm.Disjoint) (h0 : Finset.noncommProd s id (_ : Set.Pairwise s fun (a b : Equiv.Perm α) => Commute (id a) (id b)) = σ) :
    Equiv.Perm.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 : List.prod l = σ) (h1 : σl, Equiv.Perm.IsCycle σ) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
    Equiv.Perm.cycleType σ = (List.map (Finset.card Equiv.Perm.support) l)
    @[simp]
    theorem Equiv.Perm.cycleType_eq_zero {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    theorem Equiv.Perm.card_cycleType_eq_zero {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    Multiset.card (Equiv.Perm.cycleType σ) = 0 σ = 1
    theorem Equiv.Perm.card_cycleType_pos {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} :
    0 < Multiset.card (Equiv.Perm.cycleType σ) σ 1
    theorem Equiv.Perm.two_le_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : } (h : n Equiv.Perm.cycleType σ) :
    2 n
    theorem Equiv.Perm.one_lt_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : } (h : n Equiv.Perm.cycleType σ) :
    1 < n
    @[simp]
    theorem Equiv.Perm.sign_of_cycleType' {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    Equiv.Perm.sign σ = Multiset.prod (Multiset.map (fun (n : ) => -(-1) ^ n) (Equiv.Perm.cycleType σ))
    theorem Equiv.Perm.sign_of_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) :
    Equiv.Perm.sign f = (-1) ^ (Multiset.sum (Equiv.Perm.cycleType f) + Multiset.card (Equiv.Perm.cycleType f))
    theorem Equiv.Perm.dvd_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : } (h : n Equiv.Perm.cycleType σ) :
    theorem Equiv.Perm.two_dvd_card_support {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : σ ^ 2 = 1) :
    theorem Equiv.Perm.isCycle_of_prime_order {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h1 : Nat.Prime (orderOf σ)) (h2 : (Equiv.Perm.support σ).card < 2 * orderOf σ) :
    theorem Equiv.Perm.cycleType_ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] {p : αProp} [DecidablePred p] {g : Equiv.Perm (Subtype p)} :
    Equiv.Perm.cycleType (Equiv.Perm.ofSubtype g) = Equiv.Perm.cycleType g
    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) :
    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
    def Equiv.Perm.vectorsProdEqOne (G : Type u_2) [Group G] (n : ) :
    Set (Vector G n)

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

    Equations
    Instances For

      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
        • One or more equations did not get rendered due to their size.
        Instances For

          Rotate a vector whose product is 1.

          Equations
          • One or more equations did not get rendered due to their size.
          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 : ) [hp : 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 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 : Equiv.Perm.IsSwap τ) :
            H =

            The partition corresponding to a permutation

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

              3-cycles #

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

              A three-cycle is a cycle of length 3.

              Equations
              Instances For
                theorem Equiv.Perm.IsThreeCycle.sign {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle σ) :
                Equiv.Perm.sign σ = 1
                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) :
                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) :