# Documentation

Mathlib.GroupTheory.Perm.Cycle.Type

# 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

Instances For
theorem Equiv.Perm.cycleType_def {α : Type u_1} [] [] (σ : ) :
= Multiset.map (Finset.card Equiv.Perm.support) ().val
theorem Equiv.Perm.cycleType_eq' {α : Type u_1} [] [] {σ : } (s : Finset ()) (h1 : ∀ (f : ), f s) (h2 : Set.Pairwise (s) Equiv.Perm.Disjoint) (h0 : Finset.noncommProd s id (_ : Set.Pairwise s fun a b => Commute (id a) (id b)) = σ) :
= Multiset.map (Finset.card Equiv.Perm.support) s.val
theorem Equiv.Perm.cycleType_eq {α : Type u_1} [] [] {σ : } (l : List ()) (h0 : = σ) (h1 : ∀ (σ : ), σ l) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
= ↑(List.map (Finset.card Equiv.Perm.support) l)
@[simp]
theorem Equiv.Perm.cycleType_eq_zero {α : Type u_1} [] [] {σ : } :
σ = 1
@[simp]
theorem Equiv.Perm.cycleType_one {α : Type u_1} [] [] :
theorem Equiv.Perm.card_cycleType_eq_zero {α : Type u_1} [] [] {σ : } :
Multiset.card () = 0 σ = 1
theorem Equiv.Perm.card_cycleType_pos {α : Type u_1} [] [] {σ : } :
0 < Multiset.card () σ 1
theorem Equiv.Perm.two_le_of_mem_cycleType {α : Type u_1} [] [] {σ : } {n : } (h : ) :
2 n
theorem Equiv.Perm.one_lt_of_mem_cycleType {α : Type u_1} [] [] {σ : } {n : } (h : ) :
1 < n
theorem Equiv.Perm.IsCycle.cycleType {α : Type u_1} [] [] {σ : } (hσ : ) :
theorem Equiv.Perm.card_cycleType_eq_one {α : Type u_1} [] [] {σ : } :
Multiset.card () = 1
theorem Equiv.Perm.Disjoint.cycleType {α : Type u_1} [] [] {σ : } {τ : } (h : ) :
@[simp]
theorem Equiv.Perm.cycleType_inv {α : Type u_1} [] [] (σ : ) :
@[simp]
theorem Equiv.Perm.cycleType_conj {α : Type u_1} [] [] {σ : } {τ : } :
theorem Equiv.Perm.sum_cycleType {α : Type u_1} [] [] (σ : ) :
theorem Equiv.Perm.sign_of_cycleType' {α : Type u_1} [] [] (σ : ) :
Equiv.Perm.sign σ = Multiset.prod (Multiset.map (fun n => -(-1) ^ n) ())
theorem Equiv.Perm.sign_of_cycleType {α : Type u_1} [] [] (f : ) :
Equiv.Perm.sign f = (-1) ^ ( + Multiset.card ())
@[simp]
theorem Equiv.Perm.lcm_cycleType {α : Type u_1} [] [] (σ : ) :
theorem Equiv.Perm.dvd_of_mem_cycleType {α : Type u_1} [] [] {σ : } {n : } (h : ) :
n
theorem Equiv.Perm.orderOf_cycleOf_dvd_orderOf {α : Type u_1} [] [] (f : ) (x : α) :
theorem Equiv.Perm.two_dvd_card_support {α : Type u_1} [] [] {σ : } (hσ : σ ^ 2 = 1) :
theorem Equiv.Perm.cycleType_prime_order {α : Type u_1} [] [] {σ : } (hσ : Nat.Prime ()) :
n, = Multiset.replicate (n + 1) ()
theorem Equiv.Perm.isCycle_of_prime_order {α : Type u_1} [] [] {σ : } (h1 : Nat.Prime ()) (h2 : < 2 * ) :
theorem Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset {α : Type u_1} [] [] {f : } {g : } (hf : ) :
theorem Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub {α : Type u_1} [] [] {f : } {g : } (hf : ) :
theorem Equiv.Perm.isConj_of_cycleType_eq {α : Type u_1} [] [] {σ : } {τ : } (h : ) :
IsConj σ τ
theorem Equiv.Perm.isConj_iff_cycleType_eq {α : Type u_1} [] [] {σ : } {τ : } :
@[simp]
theorem Equiv.Perm.cycleType_extendDomain {α : Type u_1} [] [] {β : Type u_2} [] [] {p : βProp} [] (f : α ) {g : } :
theorem Equiv.Perm.cycleType_ofSubtype {α : Type u_1} [] [] {p : αProp} [] {g : } :
Equiv.Perm.cycleType (Equiv.Perm.ofSubtype g) =
theorem Equiv.Perm.mem_cycleType_iff {α : Type u_1} [] [] {n : } {σ : } :
c τ, σ = c * τ
theorem Equiv.Perm.le_card_support_of_mem_cycleType {α : Type u_1} [] [] {n : } {σ : } (h : ) :
theorem Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two {α : Type u_1} [] [] {n : } {g : } (hn2 : < n + 2) (hng : ) :
theorem Equiv.Perm.card_compl_support_modEq {α : Type u_1} [] [] {p : } {n : } [hp : Fact ()] {σ : } (hσ : σ ^ p ^ n = 1) :
theorem Equiv.Perm.card_fixedPoints_modEq {α : Type u_1} [] [] {f : } {p : } {n : } [hp : Fact ()] (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 ()] (hα : ¬) {σ : } (hσ : σ ^ p ^ n = 1) :
a, σ a = a
theorem Equiv.Perm.exists_fixed_point_of_prime' {α : Type u_1} [] {p : } {n : } [hp : Fact ()] (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 : Nat.Prime ()) (h2 : < 2 * ) :
theorem Equiv.Perm.isCycle_of_prime_order'' {α : Type u_1} [] {σ : } (h1 : ) (h2 : ) :
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.

Instances For
theorem Equiv.Perm.VectorsProdEqOne.mem_iff (G : Type u_2) [] {n : } (v : Vector G n) :
= 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}
@[simp]
theorem Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply (G : Type u_2) [] (n : ) (v : ↑(Equiv.Perm.vectorsProdEqOne G (n + 1))) :
().symm v =
@[simp]
theorem Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe (G : Type u_2) [] (n : ) (v : Vector G n) :
↑() = ()⁻¹ ::ᵥ 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.

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.

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.

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 ()] (hdvd : ) :
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} [] [] (p : ) [hp : Fact ()] (hdvd : ) :
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} [] [] {H : } [d : DecidablePred fun x => x H] {τ : } (h0 : ) (h1 : Fintype.card { x // x H }) (h2 : τ H) (h3 : ) :
H =
def Equiv.Perm.partition {α : Type u_1} [] [] (σ : ) :

The partition corresponding to a permutation

Instances For
theorem Equiv.Perm.parts_partition {α : Type u_1} [] [] {σ : } :
().parts =
theorem Equiv.Perm.filter_parts_partition_eq_cycleType {α : Type u_1} [] [] {σ : } :
Multiset.filter (fun n => 2 n) ().parts =
theorem Equiv.Perm.partition_eq_of_isConj {α : Type u_1} [] [] {σ : } {τ : } :

### 3-cycles #

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

A three-cycle is a cycle of length 3.

Instances For
theorem Equiv.Perm.IsThreeCycle.cycleType {α : Type u_1} [] [] {σ : } (h : ) :
theorem Equiv.Perm.IsThreeCycle.card_support {α : Type u_1} [] [] {σ : } (h : ) :
theorem card_support_eq_three_iff {α : Type u_1} [] [] {σ : } :
theorem Equiv.Perm.IsThreeCycle.isCycle {α : Type u_1} [] [] {σ : } (h : ) :
theorem Equiv.Perm.IsThreeCycle.sign {α : Type u_1} [] [] {σ : } (h : ) :
Equiv.Perm.sign σ = 1
theorem Equiv.Perm.IsThreeCycle.inv {α : Type u_1} [] [] {f : } (h : ) :
@[simp]
theorem Equiv.Perm.IsThreeCycle.inv_iff {α : Type u_1} [] [] {f : } :
theorem Equiv.Perm.IsThreeCycle.orderOf {α : Type u_1} [] [] {g : } (ht : ) :
= 3
theorem Equiv.Perm.IsThreeCycle.isThreeCycle_sq {α : Type u_1} [] [] {g : } (ht : ) :
theorem Equiv.Perm.isThreeCycle_swap_mul_swap_same {α : Type u_1} [] [] {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} [] [] {a : α} {b : α} {c : α} (ab : a b) (ac : a c) :
*
theorem Equiv.Perm.IsSwap.mul_mem_closure_three_cycles {α : Type u_1} [] [] {σ : } {τ : } (hσ : ) (hτ : ) :
σ * τ