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

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

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 ∈ s, Equiv.Perm.IsCycle f) (h2 : Set.Pairwise (↑s) Equiv.Perm.Disjoint) (h0 : Finset.noncommProd s id ⋯ = σ) : 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 α} : 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 σ = ↑[(Equiv.Perm.support σ).card]

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 σ) = (Equiv.Perm.support σ).card

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 ∣ (Equiv.Perm.support σ).card

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 : (Equiv.Perm.support σ).card < 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 : Equiv.Perm α) (τ : Equiv.Perm α), σ = c * τ ∧ Equiv.Perm.Disjoint c τ ∧ Equiv.Perm.IsCycle c ∧ (Equiv.Perm.support c).card = n

theorem Equiv.Perm.le_card_support_of_mem_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {σ : Equiv.Perm α} (h : n ∈ Equiv.Perm.cycleType σ) : n ≤ (Equiv.Perm.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 ∈ 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) : (Equiv.Perm.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 σ) : 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.

Equations

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

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)

Equations

• Equiv.Perm.VectorsProdEqOne.zeroUnique G = Eq.mpr ⋯ (Set.uniqueSingleton 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 = Eq.mpr ⋯ (Set.uniqueSingleton (1 ::ᵥ Vector.nil))

@[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.

Equations

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

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.

Equations

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

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 (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 = { val := { val := List.rotate (↑↑v) k, property := ⋯ }, property := ⋯ }

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 : ℕ) [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 = ⊤

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

The partition corresponding to a permutation

Equations

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

theorem Equiv.Perm.parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : (Equiv.Perm.partition σ).parts = Equiv.Perm.cycleType σ + Multiset.replicate (Fintype.card α - (Equiv.Perm.support σ).card) 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.

Equations

• Equiv.Perm.IsThreeCycle σ = (Equiv.Perm.cycleType σ = {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 σ) : (Equiv.Perm.support σ).card = 3

theorem card_support_eq_three_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : (Equiv.Perm.support σ).card = 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 α | 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 α | Equiv.Perm.IsThreeCycle σ}