# Cycle Types #

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

## Main definitions #

• Equiv.Perm.cycleType σ where σ is a permutation of a Fintype
• Equiv.Perm.partition σ where σ is a permutation of a Fintype

## Main results #

• sum_cycleType : The sum of σ.cycleType equals σ.support.card
• lcm_cycleType : The lcm of σ.cycleType equals orderOf σ
• isConj_iff_cycleType_eq : Two permutations are conjugate if and only if they have the same cycle type.
• exists_prime_orderOf_dvd_card: 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.
def Equiv.Perm.cycleType {α : Type u_1} [] [] (σ : ) :

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} [] [] (σ : ) :
σ.cycleType = Multiset.map (Finset.card Equiv.Perm.support) σ.cycleFactorsFinset.val
theorem Equiv.Perm.cycleType_eq' {α : Type u_1} [] [] {σ : } (s : Finset ()) (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} [] [] {σ : } (l : List ()) (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} [] [] {σ : } :
σ.cycleType = 0 σ = 1
@[simp]
theorem Equiv.Perm.cycleType_one {α : Type u_1} [] [] :
theorem Equiv.Perm.card_cycleType_eq_zero {α : Type u_1} [] [] {σ : } :
Multiset.card σ.cycleType = 0 σ = 1
theorem Equiv.Perm.card_cycleType_pos {α : Type u_1} [] [] {σ : } :
0 < Multiset.card σ.cycleType σ 1
theorem Equiv.Perm.two_le_of_mem_cycleType {α : Type u_1} [] [] {σ : } {n : } (h : n σ.cycleType) :
2 n
theorem Equiv.Perm.one_lt_of_mem_cycleType {α : Type u_1} [] [] {σ : } {n : } (h : n σ.cycleType) :
1 < n
theorem Equiv.Perm.IsCycle.cycleType {α : Type u_1} [] [] {σ : } (hσ : σ.IsCycle) :
σ.cycleType = [σ.support.card]
theorem Equiv.Perm.card_cycleType_eq_one {α : Type u_1} [] [] {σ : } :
Multiset.card σ.cycleType = 1 σ.IsCycle
theorem Equiv.Perm.Disjoint.cycleType {α : Type u_1} [] [] {σ : } {τ : } (h : σ.Disjoint τ) :
(σ * τ).cycleType = σ.cycleType + τ.cycleType
@[simp]
theorem Equiv.Perm.cycleType_inv {α : Type u_1} [] [] (σ : ) :
σ⁻¹.cycleType = σ.cycleType
@[simp]
theorem Equiv.Perm.cycleType_conj {α : Type u_1} [] [] {σ : } {τ : } :
(τ * σ * τ⁻¹).cycleType = σ.cycleType
theorem Equiv.Perm.sum_cycleType {α : Type u_1} [] [] (σ : ) :
σ.cycleType.sum = σ.support.card
theorem Equiv.Perm.sign_of_cycleType' {α : Type u_1} [] [] (σ : ) :
Equiv.Perm.sign σ = (Multiset.map (fun (n : ) => -(-1) ^ n) σ.cycleType).prod
theorem Equiv.Perm.sign_of_cycleType {α : Type u_1} [] [] (f : ) :
Equiv.Perm.sign f = (-1) ^ (f.cycleType.sum + Multiset.card f.cycleType)
@[simp]
theorem Equiv.Perm.lcm_cycleType {α : Type u_1} [] [] (σ : ) :
σ.cycleType.lcm =
theorem Equiv.Perm.dvd_of_mem_cycleType {α : Type u_1} [] [] {σ : } {n : } (h : n σ.cycleType) :
n
theorem Equiv.Perm.orderOf_cycleOf_dvd_orderOf {α : Type u_1} [] [] (f : ) (x : α) :
orderOf (f.cycleOf x)
theorem Equiv.Perm.two_dvd_card_support {α : Type u_1} [] [] {σ : } (hσ : σ ^ 2 = 1) :
2 σ.support.card
theorem Equiv.Perm.cycleType_prime_order {α : Type u_1} [] [] {σ : } (hσ : ().Prime) :
∃ (n : ), σ.cycleType = Multiset.replicate (n + 1) ()
theorem Equiv.Perm.isCycle_of_prime_order {α : Type u_1} [] [] {σ : } (h1 : ().Prime) (h2 : σ.support.card < 2 * ) :
σ.IsCycle
theorem Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset {α : Type u_1} [] [] {f : } {g : } (hf : f g.cycleFactorsFinset) :
f.cycleType g.cycleType
theorem Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub {α : Type u_1} [] [] {f : } {g : } (hf : f g.cycleFactorsFinset) :
(g * f⁻¹).cycleType = g.cycleType - f.cycleType
theorem Equiv.Perm.isConj_of_cycleType_eq {α : Type u_1} [] [] {σ : } {τ : } (h : σ.cycleType = τ.cycleType) :
IsConj σ τ
theorem Equiv.Perm.isConj_iff_cycleType_eq {α : Type u_1} [] [] {σ : } {τ : } :
IsConj σ τ σ.cycleType = τ.cycleType
@[simp]
theorem Equiv.Perm.cycleType_extendDomain {α : Type u_1} [] [] {β : Type u_2} [] [] {p : βProp} [] (f : α ) {g : } :
(g.extendDomain f).cycleType = g.cycleType
theorem Equiv.Perm.cycleType_ofSubtype {α : Type u_1} [] [] {p : αProp} [] {g : } :
(Equiv.Perm.ofSubtype g).cycleType = g.cycleType
theorem Equiv.Perm.mem_cycleType_iff {α : Type u_1} [] [] {n : } {σ : } :
n σ.cycleType ∃ (c : ) (τ : ), σ = c * τ c.Disjoint τ c.IsCycle c.support.card = n
theorem Equiv.Perm.le_card_support_of_mem_cycleType {α : Type u_1} [] [] {n : } {σ : } (h : n σ.cycleType) :
n σ.support.card
theorem Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two {α : Type u_1} [] [] {n : } {g : } (hn2 : < n + 2) (hng : n g.cycleType) :
g.cycleType = {n}
theorem Equiv.Perm.card_compl_support_modEq {α : Type u_1} [] [] {p : } {n : } [hp : Fact p.Prime] {σ : } (hσ : σ ^ p ^ n = 1) :
σ.support.card [MOD p]
theorem Equiv.Perm.card_fixedPoints_modEq {α : Type u_1} [] [] {f : } {p : } {n : } [hp : Fact p.Prime] (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} [] {p : } {n : } [hp : Fact p.Prime] (hα : ¬) {σ : } (hσ : σ ^ p ^ n = 1) :
∃ (a : α), σ a = a
theorem Equiv.Perm.exists_fixed_point_of_prime' {α : Type u_1} [] {p : } {n : } [hp : Fact p.Prime] (hα : ) {σ : } (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) :
∃ (b : α), σ b = b b a
theorem Equiv.Perm.isCycle_of_prime_order' {α : Type u_1} [] {σ : } (h1 : ().Prime) (h2 : < 2 * ) :
σ.IsCycle
theorem Equiv.Perm.isCycle_of_prime_order'' {α : Type u_1} [] {σ : } (h1 : ().Prime) (h2 : ) :
σ.IsCycle
def Equiv.Perm.vectorsProdEqOne (G : Type u_2) [] (n : ) :
Set (Vector G n)

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) [] {n : } (v : Vector G n) :
v.toList.prod = 1
theorem Equiv.Perm.VectorsProdEqOne.zero_eq (G : Type u_2) [] :
= {Vector.nil}
theorem Equiv.Perm.VectorsProdEqOne.one_eq (G : Type u_2) [] :
= {1 ::ᵥ Vector.nil}
Equations
Equations
@[simp]
theorem Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply (G : Type u_2) [] (n : ) (v : (Equiv.Perm.vectorsProdEqOne G (n + 1))) :
.symm v = (v).tail
@[simp]
theorem Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe (G : Type u_2) [] (n : ) (v : Vector G n) :
() = v.toList.prod⁻¹ ::ᵥ v

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
def Equiv.Perm.VectorsProdEqOne.equivVector (G : Type u_2) [] (n : ) :
Vector G (n - 1)

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
theorem Equiv.Perm.VectorsProdEqOne.card (G : Type u_2) [] (n : ) [] :
= ^ (n - 1)
def Equiv.Perm.VectorsProdEqOne.rotate {G : Type u_2} [] {n : } (v : ) (k : ) :

Rotate a vector whose product is 1.

Equations
• = (v).rotate k, ,
Instances For
theorem Equiv.Perm.VectorsProdEqOne.rotate_zero {G : Type u_2} [] {n : } (v : ) :
theorem Equiv.Perm.VectorsProdEqOne.rotate_rotate {G : Type u_2} [] {n : } (v : ) (j : ) (k : ) :
theorem Equiv.Perm.VectorsProdEqOne.rotate_length {G : Type u_2} [] {n : } (v : ) :
theorem exists_prime_orderOf_dvd_card {G : Type u_3} [] [] (p : ) [hp : Fact p.Prime] (hdvd : ) :
∃ (x : G), = 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} [] [] (p : ) [hp : Fact p.Prime] (hdvd : ) :
∃ (x : G), = 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} [] [] {H : } [d : DecidablePred fun (x : ) => x H] {τ : } (h0 : ().Prime) (h1 : ) (h2 : τ H) (h3 : τ.IsSwap) :
H =
def Equiv.Perm.partition {α : Type u_1} [] [] (σ : ) :
().Partition

The partition corresponding to a permutation

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

### 3-cycles #

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

A three-cycle is a cycle of length 3.

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