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} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Multiset ℕ

The cycle type of a permutation

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 : ∀ (f : Equiv.Perm α), f ∈ s → Equiv.Perm.IsCycle f) (h2 : Set.Pairwise (↑s) Equiv.Perm.Disjoint) (h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => 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 : ∀ (σ : Equiv.Perm α), σ ∈ 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 α} : Equiv.Perm.cycleType σ = 0 ↔ σ = 1

@[simp]

theorem Equiv.Perm.cycleType_one {α : Type u_1} [Fintype α] [DecidableEq α] : Equiv.Perm.cycleType 1 = 0

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

theorem Equiv.Perm.IsCycle.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) : Equiv.Perm.cycleType σ = ↑[Finset.card (Equiv.Perm.support σ)]

theorem Equiv.Perm.card_cycleType_eq_one {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : ↑Multiset.card (Equiv.Perm.cycleType σ) = 1 ↔ Equiv.Perm.IsCycle σ

theorem Equiv.Perm.Disjoint.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h : Equiv.Perm.Disjoint σ τ) : Equiv.Perm.cycleType (σ * τ) = Equiv.Perm.cycleType σ + Equiv.Perm.cycleType τ

@[simp]

theorem Equiv.Perm.cycleType_inv {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Equiv.Perm.cycleType σ⁻¹ = Equiv.Perm.cycleType σ

@[simp]

theorem Equiv.Perm.cycleType_conj {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} : Equiv.Perm.cycleType (τ * σ * τ⁻¹) = Equiv.Perm.cycleType σ

theorem Equiv.Perm.sum_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Multiset.sum (Equiv.Perm.cycleType σ) = Finset.card (Equiv.Perm.support σ)

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))

@[simp]

theorem Equiv.Perm.lcm_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Multiset.lcm (Equiv.Perm.cycleType σ) = orderOf σ

theorem Equiv.Perm.dvd_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {n : ℕ} (h : n ∈ Equiv.Perm.cycleType σ) : n ∣ orderOf σ

theorem Equiv.Perm.orderOf_cycleOf_dvd_orderOf {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (x : α) : orderOf (Equiv.Perm.cycleOf f x) ∣ orderOf f

theorem Equiv.Perm.two_dvd_card_support {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : σ ^ 2 = 1) : 2 ∣ Finset.card (Equiv.Perm.support σ)

theorem Equiv.Perm.cycleType_prime_order {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (hσ : Nat.Prime (orderOf σ)) : ∃ n, Equiv.Perm.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 : Finset.card (Equiv.Perm.support σ) < 2 * orderOf σ) : Equiv.Perm.IsCycle σ

theorem Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {g : Equiv.Perm α} (hf : f ∈ Equiv.Perm.cycleFactorsFinset g) : Equiv.Perm.cycleType f ≤ Equiv.Perm.cycleType g

theorem Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {g : Equiv.Perm α} (hf : f ∈ Equiv.Perm.cycleFactorsFinset g) : Equiv.Perm.cycleType (g * f⁻¹) = Equiv.Perm.cycleType g - Equiv.Perm.cycleType f

theorem Equiv.Perm.isConj_of_cycleType_eq {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h : Equiv.Perm.cycleType σ = Equiv.Perm.cycleType τ) : IsConj σ τ

theorem Equiv.Perm.isConj_iff_cycleType_eq {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} : IsConj σ τ ↔ Equiv.Perm.cycleType σ = Equiv.Perm.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 α} : Equiv.Perm.cycleType (Equiv.Perm.extendDomain g f) = Equiv.Perm.cycleType g

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.mem_cycleType_iff {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {σ : Equiv.Perm α} : n ∈ Equiv.Perm.cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Equiv.Perm.Disjoint c τ ∧ Equiv.Perm.IsCycle c ∧ Finset.card (Equiv.Perm.support c) = n

theorem Equiv.Perm.le_card_support_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {σ : Equiv.Perm α} (h : n ∈ Equiv.Perm.cycleType σ) : n ≤ Finset.card (Equiv.Perm.support σ)

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 ∈ Equiv.Perm.cycleType g) : Equiv.Perm.cycleType g = {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) : Finset.card (Equiv.Perm.support σ)ᶜ ≡ 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) : Fintype.card α ≡ Fintype.card ↑(Function.fixedPoints f) [MOD p]

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 σ) : Equiv.Perm.IsCycle σ

theorem Equiv.Perm.isCycle_of_prime_order'' {α : Type u_1} [Fintype α] {σ : Equiv.Perm α} (h1 : Nat.Prime (Fintype.card α)) (h2 : orderOf σ = Fintype.card α) : Equiv.Perm.IsCycle σ

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.

theorem Equiv.Perm.VectorsProdEqOne.mem_iff (G : Type u_2) [Group G] {n : ℕ} (v : Vector G n) : v ∈ Equiv.Perm.vectorsProdEqOne G n ↔ List.prod (Vector.toList v) = 1

theorem Equiv.Perm.VectorsProdEqOne.zero_eq (G : Type u_2) [Group G] : Equiv.Perm.vectorsProdEqOne G 0 = {Vector.nil}

theorem Equiv.Perm.VectorsProdEqOne.one_eq (G : Type u_2) [Group G] : Equiv.Perm.vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}

instance Equiv.Perm.VectorsProdEqOne.zeroUnique (G : Type u_2) [Group G] : Unique ↑(Equiv.Perm.vectorsProdEqOne G 0)

instance Equiv.Perm.VectorsProdEqOne.oneUnique (G : Type u_2) [Group G] : Unique ↑(Equiv.Perm.vectorsProdEqOne G 1)

@[simp]

theorem Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply (G : Type u_2) [Group G] (n : ℕ) (v : ↑(Equiv.Perm.vectorsProdEqOne G (n + 1))) : ↑(Equiv.Perm.VectorsProdEqOne.vectorEquiv G n).symm v = Vector.tail ↑v

@[simp]

theorem Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe (G : Type u_2) [Group G] (n : ℕ) (v : Vector G n) : ↑(↑(Equiv.Perm.VectorsProdEqOne.vectorEquiv G n) v) = (List.prod (Vector.toList v))⁻¹ ::ᵥ v

def Equiv.Perm.VectorsProdEqOne.vectorEquiv (G : Type u_2) [Group G] (n : ℕ) : Vector G n ≃ ↑(Equiv.Perm.vectorsProdEqOne G (n + 1))

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.

def Equiv.Perm.VectorsProdEqOne.equivVector (G : Type u_2) [Group G] (n : ℕ) : ↑(Equiv.Perm.vectorsProdEqOne G 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.

instance Equiv.Perm.VectorsProdEqOne.instFintypeElemVectorVectorsProdEqOne (G : Type u_2) [Group G] (n : ℕ) [Fintype G] : Fintype ↑(Equiv.Perm.vectorsProdEqOne G n)

theorem Equiv.Perm.VectorsProdEqOne.card (G : Type u_2) [Group G] (n : ℕ) [Fintype G] : Fintype.card ↑(Equiv.Perm.vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)

def Equiv.Perm.VectorsProdEqOne.rotate {G : Type u_2} [Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)) (k : ℕ) : ↑(Equiv.Perm.vectorsProdEqOne G n)

Rotate a vector whose product is 1.

theorem Equiv.Perm.VectorsProdEqOne.rotate_zero {G : Type u_2} [Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)) : Equiv.Perm.VectorsProdEqOne.rotate v 0 = v

theorem Equiv.Perm.VectorsProdEqOne.rotate_rotate {G : Type u_2} [Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)) (j : ℕ) (k : ℕ) : Equiv.Perm.VectorsProdEqOne.rotate (Equiv.Perm.VectorsProdEqOne.rotate v j) k = Equiv.Perm.VectorsProdEqOne.rotate v (j + k)

theorem Equiv.Perm.VectorsProdEqOne.rotate_length {G : Type u_2} [Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)) : Equiv.Perm.VectorsProdEqOne.rotate v n = v

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, 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, 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 => x ∈ H] {τ : Equiv.Perm α} (h0 : Nat.Prime (Fintype.card α)) (h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }) (h2 : τ ∈ H) (h3 : Equiv.Perm.IsSwap τ) : H = ⊤

def Equiv.Perm.partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Nat.Partition (Fintype.card α)

The partition corresponding to a permutation

theorem Equiv.Perm.parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : (Equiv.Perm.partition σ).parts = Equiv.Perm.cycleType σ + Multiset.replicate (Fintype.card α - Finset.card (Equiv.Perm.support σ)) 1

theorem Equiv.Perm.filter_parts_partition_eq_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : Multiset.filter (fun n => 2 ≤ n) (Equiv.Perm.partition σ).parts = Equiv.Perm.cycleType σ

theorem Equiv.Perm.partition_eq_of_isConj {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} : IsConj σ τ ↔ Equiv.Perm.partition σ = Equiv.Perm.partition τ

3-cycles

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

A three-cycle is a cycle of length 3.

theorem Equiv.Perm.IsThreeCycle.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle σ) : Equiv.Perm.cycleType σ = {3}

theorem Equiv.Perm.IsThreeCycle.card_support {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle σ) : Finset.card (Equiv.Perm.support σ) = 3

theorem card_support_eq_three_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : Finset.card (Equiv.Perm.support σ) = 3 ↔ Equiv.Perm.IsThreeCycle σ

theorem Equiv.Perm.IsThreeCycle.isCycle {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle σ) : Equiv.Perm.IsCycle σ

theorem Equiv.Perm.IsThreeCycle.sign {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle σ) : ↑Equiv.Perm.sign σ = 1

theorem Equiv.Perm.IsThreeCycle.inv {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle f) : Equiv.Perm.IsThreeCycle f⁻¹

@[simp]

theorem Equiv.Perm.IsThreeCycle.inv_iff {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} : Equiv.Perm.IsThreeCycle f⁻¹ ↔ Equiv.Perm.IsThreeCycle f

theorem Equiv.Perm.IsThreeCycle.orderOf {α : Type u_1} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (ht : Equiv.Perm.IsThreeCycle g) : orderOf g = 3

theorem Equiv.Perm.IsThreeCycle.isThreeCycle_sq {α : Type u_1} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (ht : Equiv.Perm.IsThreeCycle g) : Equiv.Perm.IsThreeCycle (g * g)

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.Perm.IsThreeCycle (Equiv.swap a b * Equiv.swap a 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) : 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σ : Equiv.Perm.IsSwap σ) (hτ : Equiv.Perm.IsSwap τ) : σ * τ ∈ Subgroup.closure {σ | Equiv.Perm.IsThreeCycle σ}