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

Equations

• σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) σ.cycleFactorsFinset.val

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 : ∀ f ∈ s, 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)

theorem Equiv.Perm.CycleType.count_def {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (n : ℕ) : Multiset.count n σ.cycleType = Fintype.card { c : { x : Equiv.Perm α // x ∈ σ.cycleFactorsFinset } // (↑c).support.card = n }

@[simp]

theorem Equiv.Perm.cycleType_eq_zero {α : Type u_1} [Fintype α] [DecidableEq α] {σ : 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 σ.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 α} (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 α} : (τ * σ * τ⁻¹).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) : n ∣ orderOf σ

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 g : Equiv.Perm α} (hf : f ∈ g.cycleFactorsFinset) : f.cycleType ≤ g.cycleType

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

theorem Equiv.Perm.Disjoint.cycleType_noncommProd {α : Type u_1} [Fintype α] [DecidableEq α] {ι : Type u_2} {k : ι → Equiv.Perm α} {s : Finset ι} (hs : (↑s).Pairwise fun (i j : ι) => (k i).Disjoint (k j)) (hs' : (↑s).Pairwise fun (i j : ι) => Commute (k i) (k j) := ⋯) : (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

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

theorem Equiv.Perm.isConj_iff_cycleType_eq {α : Type u_1} [Fintype α] [DecidableEq α] {σ τ : 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) : 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 σ) : σ.IsCycle

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

def Equiv.Perm.vectorsProdEqOne (G : Type u_2) [Group G] (n : ℕ) : Set (Mathlib.Vector G n)

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

Equations

• Equiv.Perm.vectorsProdEqOne G n = {v : Mathlib.Vector G n | v.toList.prod = 1}

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}

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

Equations

• Equiv.Perm.VectorsProdEqOne.zeroUnique G = ⋯.mpr (Set.uniqueSingleton Mathlib.Vector.nil)

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

Equations

• Equiv.Perm.VectorsProdEqOne.oneUnique G = ⋯.mpr (Set.uniqueSingleton (1 ::ᵥ Mathlib.Vector.nil))

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

Equations

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

@[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 = (↑v).tail

@[simp]

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

def Equiv.Perm.VectorsProdEqOne.equivVector (G : Type u_2) [Group G] (n : ℕ) : ↑(Equiv.Perm.vectorsProdEqOne G n) ≃ Mathlib.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.
• Equiv.Perm.VectorsProdEqOne.equivVector G n.succ = (Equiv.Perm.VectorsProdEqOne.vectorEquiv G n).symm

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

Equations

• Equiv.Perm.VectorsProdEqOne.instFintypeElemVectorVectorsProdEqOne G n = Fintype.ofEquiv (Mathlib.Vector G (n - 1)) (Equiv.Perm.VectorsProdEqOne.equivVector G n).symm

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.

Equations

• Equiv.Perm.VectorsProdEqOne.rotate v k = ⟨⟨(↑↑v).rotate k, ⋯⟩, ⋯⟩

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 : 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_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 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 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

• σ.partition = { parts := σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1, parts_pos := ⋯, parts_sum := ⋯ }

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 α} : IsConj σ τ ↔ σ.partition = τ.partition

3-cycles

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

A three-cycle is a cycle of length 3.

Equations

• σ.IsThreeCycle = (σ.cycleType = {3})

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) : orderOf g = 3

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