Cycle Types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define the cycle type of a permutation.
Main definitions #
σ.cycle_typewhereσis a permutation of afintypeσ.partitionwhereσis a permutation of afintype
Main results #
sum_cycle_type: The sum ofσ.cycle_typeequalsσ.support.cardlcm_cycle_type: The lcm ofσ.cycle_typeequalsorder_of σis_conj_iff_cycle_type_eq: Two permutations are conjugate if and only if they have the same cycle type.exists_prime_order_of_dvd_card: For every primepdividing the order of a finite groupGthere exists an element of orderpinG. This is known as Cauchy's theorem.
The cycle type of a permutation
Equations
theorem
equiv.perm.cycle_type_eq'
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(s : finset (equiv.perm α))
(h1 : ∀ (f : equiv.perm α), f ∈ s → f.is_cycle)
(h2 : ↑s.pairwise equiv.perm.disjoint)
(h0 : s.noncomm_prod id _ = σ) :
theorem
equiv.perm.cycle_type_eq
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(l : list (equiv.perm α))
(h0 : l.prod = σ)
(h1 : ∀ (σ : equiv.perm α), σ ∈ l → σ.is_cycle)
(h2 : list.pairwise equiv.perm.disjoint l) :
σ.cycle_type = ↑(list.map (finset.card ∘ equiv.perm.support) l)
theorem
equiv.perm.cycle_type_eq_zero
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α} :
σ.cycle_type = 0 ↔ σ = 1
theorem
equiv.perm.card_cycle_type_eq_zero
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α} :
⇑multiset.card σ.cycle_type = 0 ↔ σ = 1
theorem
equiv.perm.two_le_of_mem_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
{n : ℕ}
(h : n ∈ σ.cycle_type) :
2 ≤ n
theorem
equiv.perm.one_lt_of_mem_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
{n : ℕ}
(h : n ∈ σ.cycle_type) :
1 < n
theorem
equiv.perm.is_cycle.cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(hσ : σ.is_cycle) :
theorem
equiv.perm.card_cycle_type_eq_one
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α} :
⇑multiset.card σ.cycle_type = 1 ↔ σ.is_cycle
theorem
equiv.perm.disjoint.cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ τ : equiv.perm α}
(h : σ.disjoint τ) :
(σ * τ).cycle_type = σ.cycle_type + τ.cycle_type
theorem
equiv.perm.cycle_type_inv
{α : Type u_1}
[fintype α]
[decidable_eq α]
(σ : equiv.perm α) :
σ⁻¹.cycle_type = σ.cycle_type
theorem
equiv.perm.cycle_type_conj
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ τ : equiv.perm α} :
(τ * σ * τ⁻¹).cycle_type = σ.cycle_type
theorem
equiv.perm.sum_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
(σ : equiv.perm α) :
σ.cycle_type.sum = σ.support.card
theorem
equiv.perm.sign_of_cycle_type'
{α : Type u_1}
[fintype α]
[decidable_eq α]
(σ : equiv.perm α) :
⇑equiv.perm.sign σ = (multiset.map (λ (n : ℕ), -(-1) ^ n) σ.cycle_type).prod
theorem
equiv.perm.sign_of_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
(f : equiv.perm α) :
⇑equiv.perm.sign f = (-1) ^ (f.cycle_type.sum + ⇑multiset.card f.cycle_type)
theorem
equiv.perm.lcm_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
(σ : equiv.perm α) :
σ.cycle_type.lcm = order_of σ
theorem
equiv.perm.dvd_of_mem_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
{n : ℕ}
(h : n ∈ σ.cycle_type) :
theorem
equiv.perm.order_of_cycle_of_dvd_order_of
{α : Type u_1}
[fintype α]
[decidable_eq α]
(f : equiv.perm α)
(x : α) :
theorem
equiv.perm.two_dvd_card_support
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(hσ : σ ^ 2 = 1) :
theorem
equiv.perm.cycle_type_prime_order
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(hσ : nat.prime (order_of σ)) :
∃ (n : ℕ), σ.cycle_type = multiset.replicate (n + 1) (order_of σ)
theorem
equiv.perm.is_cycle_of_prime_order
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(h1 : nat.prime (order_of σ))
(h2 : σ.support.card < 2 * order_of σ) :
σ.is_cycle
theorem
equiv.perm.cycle_type_le_of_mem_cycle_factors_finset
{α : Type u_1}
[fintype α]
[decidable_eq α]
{f g : equiv.perm α}
(hf : f ∈ g.cycle_factors_finset) :
f.cycle_type ≤ g.cycle_type
theorem
equiv.perm.cycle_type_mul_mem_cycle_factors_finset_eq_sub
{α : Type u_1}
[fintype α]
[decidable_eq α]
{f g : equiv.perm α}
(hf : f ∈ g.cycle_factors_finset) :
(g * f⁻¹).cycle_type = g.cycle_type - f.cycle_type
theorem
equiv.perm.is_conj_of_cycle_type_eq
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ τ : equiv.perm α}
(h : σ.cycle_type = τ.cycle_type) :
is_conj σ τ
theorem
equiv.perm.is_conj_iff_cycle_type_eq
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ τ : equiv.perm α} :
is_conj σ τ ↔ σ.cycle_type = τ.cycle_type
@[simp]
theorem
equiv.perm.cycle_type_extend_domain
{α : Type u_1}
[fintype α]
[decidable_eq α]
{β : Type u_2}
[fintype β]
[decidable_eq β]
{p : β → Prop}
[decidable_pred p]
(f : α ≃ subtype p)
{g : equiv.perm α} :
(g.extend_domain f).cycle_type = g.cycle_type
theorem
equiv.perm.cycle_type_of_subtype
{α : Type u_1}
[fintype α]
[decidable_eq α]
{p : α → Prop}
[decidable_pred p]
{g : equiv.perm (subtype p)} :
theorem
equiv.perm.mem_cycle_type_iff
{α : Type u_1}
[fintype α]
[decidable_eq α]
{n : ℕ}
{σ : equiv.perm α} :
theorem
equiv.perm.le_card_support_of_mem_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{n : ℕ}
{σ : equiv.perm α}
(h : n ∈ σ.cycle_type) :
theorem
equiv.perm.cycle_type_of_card_le_mem_cycle_type_add_two
{α : Type u_1}
[fintype α]
[decidable_eq α]
{n : ℕ}
{g : equiv.perm α}
(hn2 : fintype.card α < n + 2)
(hng : n ∈ g.cycle_type) :
g.cycle_type = {n}
theorem
equiv.perm.card_compl_support_modeq
{α : Type u_1}
[fintype α]
[decidable_eq α]
{p n : ℕ}
[hp : fact (nat.prime p)]
{σ : equiv.perm α}
(hσ : σ ^ p ^ n = 1) :
theorem
equiv.perm.is_cycle_of_prime_order'
{α : Type u_1}
[fintype α]
{σ : equiv.perm α}
(h1 : nat.prime (order_of σ))
(h2 : fintype.card α < 2 * order_of σ) :
σ.is_cycle
theorem
equiv.perm.is_cycle_of_prime_order''
{α : Type u_1}
[fintype α]
{σ : equiv.perm α}
(h1 : nat.prime (fintype.card α))
(h2 : order_of σ = fintype.card α) :
σ.is_cycle
The type of vectors with terms from G, length n, and product equal to 1:G.
Instances for ↥equiv.perm.vectors_prod_eq_one
theorem
equiv.perm.vectors_prod_eq_one.one_eq
(G : Type u_2)
[group G] :
equiv.perm.vectors_prod_eq_one G 1 = {1 ::ᵥ vector.nil}
@[protected, instance]
Equations
@[protected, instance]
Equations
def
equiv.perm.vectors_prod_eq_one.vector_equiv
(G : Type u_2)
[group G]
(n : ℕ) :
vector G n ≃ ↥(equiv.perm.vectors_prod_eq_one 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.
@[simp]
theorem
equiv.perm.vectors_prod_eq_one.vector_equiv_symm_apply
(G : Type u_2)
[group G]
(n : ℕ)
(v : ↥(equiv.perm.vectors_prod_eq_one G (n + 1))) :
def
equiv.perm.vectors_prod_eq_one.equiv_vector
(G : Type u_2)
[group G]
(n : ℕ) :
↥(equiv.perm.vectors_prod_eq_one 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
- equiv.perm.vectors_prod_eq_one.equiv_vector G n = ((equiv.perm.vectors_prod_eq_one.vector_equiv G (n - 1)).trans (dite (n = 0) (λ (hn : n = 0), show ↥(equiv.perm.vectors_prod_eq_one G (n - 1 + 1)) ≃ ↥(equiv.perm.vectors_prod_eq_one G n), from _.mpr (equiv.equiv_of_unique ↥(equiv.perm.vectors_prod_eq_one G (0 - 1 + 1)) ↥(equiv.perm.vectors_prod_eq_one G 0))) (λ (hn : ¬n = 0), _.mpr (equiv.refl ↥(equiv.perm.vectors_prod_eq_one G n))))).symm
@[protected, instance]
Equations
theorem
equiv.perm.vectors_prod_eq_one.card
(G : Type u_2)
[group G]
(n : ℕ)
[fintype G] :
fintype.card ↥(equiv.perm.vectors_prod_eq_one G n) = fintype.card G ^ (n - 1)
def
equiv.perm.vectors_prod_eq_one.rotate
{G : Type u_2}
[group G]
{n : ℕ}
(v : ↥(equiv.perm.vectors_prod_eq_one G n))
(k : ℕ) :
Rotate a vector whose product is 1.
theorem
equiv.perm.vectors_prod_eq_one.rotate_zero
{G : Type u_2}
[group G]
{n : ℕ}
(v : ↥(equiv.perm.vectors_prod_eq_one G n)) :
theorem
equiv.perm.vectors_prod_eq_one.rotate_rotate
{G : Type u_2}
[group G]
{n : ℕ}
(v : ↥(equiv.perm.vectors_prod_eq_one G n))
(j k : ℕ) :
theorem
equiv.perm.vectors_prod_eq_one.rotate_length
{G : Type u_2}
[group G]
{n : ℕ}
(v : ↥(equiv.perm.vectors_prod_eq_one G n)) :
theorem
exists_prime_order_of_dvd_card
{G : Type u_1}
[group G]
[fintype G]
(p : ℕ)
[hp : fact (nat.prime p)]
(hdvd : p ∣ fintype.card G) :
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_add_order_of_dvd_card
{G : Type u_1}
[add_group G]
[fintype G]
(p : ℕ)
[hp : fact (nat.prime p)]
(hdvd : p ∣ fintype.card G) :
∃ (x : G), add_order_of 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 α]
[decidable_eq α]
{H : subgroup (equiv.perm α)}
[d : decidable_pred (λ (_x : equiv.perm α), _x ∈ H)]
{τ : equiv.perm α}
(h0 : nat.prime (fintype.card α))
(h1 : fintype.card α ∣ fintype.card ↥H)
(h2 : τ ∈ H)
(h3 : τ.is_swap) :
The partition corresponding to a permutation
Equations
- σ.partition = {parts := σ.cycle_type + multiset.replicate (fintype.card α - σ.support.card) 1, parts_pos := _, parts_sum := _}
theorem
equiv.perm.parts_partition
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α} :
σ.partition.parts = σ.cycle_type + multiset.replicate (fintype.card α - σ.support.card) 1
theorem
equiv.perm.filter_parts_partition_eq_cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α} :
multiset.filter (λ (n : ℕ), 2 ≤ n) σ.partition.parts = σ.cycle_type
theorem
equiv.perm.partition_eq_of_is_conj
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ τ : equiv.perm α} :
3-cycles #
A three-cycle is a cycle of length 3.
Equations
- σ.is_three_cycle = (σ.cycle_type = {3})
theorem
equiv.perm.is_three_cycle.cycle_type
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(h : σ.is_three_cycle) :
σ.cycle_type = {3}
theorem
equiv.perm.is_three_cycle.card_support
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(h : σ.is_three_cycle) :
theorem
card_support_eq_three_iff
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α} :
σ.support.card = 3 ↔ σ.is_three_cycle
theorem
equiv.perm.is_three_cycle.is_cycle
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(h : σ.is_three_cycle) :
σ.is_cycle
theorem
equiv.perm.is_three_cycle.sign
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ : equiv.perm α}
(h : σ.is_three_cycle) :
⇑equiv.perm.sign σ = 1
theorem
equiv.perm.is_three_cycle.inv
{α : Type u_1}
[fintype α]
[decidable_eq α]
{f : equiv.perm α}
(h : f.is_three_cycle) :
@[simp]
theorem
equiv.perm.is_three_cycle.inv_iff
{α : Type u_1}
[fintype α]
[decidable_eq α]
{f : equiv.perm α} :
theorem
equiv.perm.is_three_cycle.order_of
{α : Type u_1}
[fintype α]
[decidable_eq α]
{g : equiv.perm α}
(ht : g.is_three_cycle) :
theorem
equiv.perm.is_three_cycle.is_three_cycle_sq
{α : Type u_1}
[fintype α]
[decidable_eq α]
{g : equiv.perm α}
(ht : g.is_three_cycle) :
(g * g).is_three_cycle
theorem
equiv.perm.is_three_cycle_swap_mul_swap_same
{α : Type u_1}
[fintype α]
[decidable_eq α]
{a b c : α}
(ab : a ≠ b)
(ac : a ≠ c)
(bc : b ≠ c) :
(equiv.swap a b * equiv.swap a c).is_three_cycle
theorem
equiv.perm.swap_mul_swap_same_mem_closure_three_cycles
{α : Type u_1}
[fintype α]
[decidable_eq α]
{a b c : α}
(ab : a ≠ b)
(ac : a ≠ c) :
equiv.swap a b * equiv.swap a c ∈ subgroup.closure {σ : equiv.perm α | σ.is_three_cycle}
theorem
equiv.perm.is_swap.mul_mem_closure_three_cycles
{α : Type u_1}
[fintype α]
[decidable_eq α]
{σ τ : equiv.perm α}
(hσ : σ.is_swap)
(hτ : τ.is_swap) :
σ * τ ∈ subgroup.closure {σ : equiv.perm α | σ.is_three_cycle}