mathlib documentation

group_theory.perm.cycle_type

Cycle Types #

In this file we define the cycle type of a partition.

Main definitions #

Main results #

source
theorem equiv.perm.mem_list_cycles_iff {α : Type u_1} [fintype α] {l : list (equiv.perm α)} (h1 : ∀ (σ : equiv.perm α), σ ∈ l → σ.is_cycle) (h2 : list.pairwise equiv.perm.disjoint l) {σ : equiv.perm α} (h3 : σ.is_cycle) {a : α} (h4 : ⇑σ a ≠ a) :
σ ∈ l ↔ ∀ (k : ℕ), ⇑(σ ^ k) a = ⇑(l.prod ^ k) a
source
theorem equiv.perm.list_cycles_perm_list_cycles {α : Type u_1} [fintype α] {l₁ l₂ : list (equiv.perm α)} (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ (σ : equiv.perm α), σ ∈ l₁ → σ.is_cycle) (h₁l₂ : ∀ (σ : equiv.perm α), σ ∈ l₂ → σ.is_cycle) (h₂l₁ : list.pairwise equiv.perm.disjoint l₁) (h₂l₂ : list.pairwise equiv.perm.disjoint l₂) :
l₁ ~ l₂
source
def equiv.perm.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
multiset ℕ

The cycle type of a permutation

Equations
source
theorem equiv.perm.two_le_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} {n : ℕ} (h : n ∈ σ.cycle_type) :
2 ≤ n
source
theorem equiv.perm.one_lt_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} {n : ℕ} (h : n ∈ σ.cycle_type) :
1 < n
source
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)
source
theorem equiv.perm.cycle_type_one {α : Type u_1} [fintype α] [decidable_eq α] :
1.cycle_type = 0
source
theorem equiv.perm.cycle_type_eq_zero {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
σ.cycle_type = 0 ↔ σ = 1
source
theorem equiv.perm.card_cycle_type_eq_zero {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
⇑multiset.card σ.cycle_type = 0 ↔ σ = 1
source
theorem equiv.perm.is_cycle.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (hσ : σ.is_cycle) :
σ.cycle_type = ↑[σ.support.card]
source
theorem equiv.perm.card_cycle_type_eq_one {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
⇑multiset.card σ.cycle_type = 1 ↔ σ.is_cycle
source
theorem equiv.perm.disjoint.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} (h : σ.disjoint τ) :
(σ * τ).cycle_type = σ.cycle_type + τ.cycle_type
source
theorem equiv.perm.cycle_type_inv {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
σ⁻¹.cycle_type = σ.cycle_type
source
theorem equiv.perm.cycle_type_conj {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} :
((τ * σ) * τ⁻¹).cycle_type = σ.cycle_type
source
theorem equiv.perm.sum_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
σ.cycle_type.sum = σ.support.card
source
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
source
theorem equiv.perm.lcm_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
σ.cycle_type.lcm = order_of σ
source
theorem equiv.perm.dvd_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} {n : ℕ} (h : n ∈ σ.cycle_type) :
n ∣ order_of σ
source
theorem equiv.perm.two_dvd_card_support {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (hσ : σ ^ 2 = 1) :
2 ∣ σ.support.card
source
theorem equiv.perm.cycle_type_prime_order {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (hσ : nat.prime (order_of σ)) :
∃ (n : ℕ), σ.cycle_type = multiset.repeat (order_of σ) (n + 1)
source
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
source
theorem equiv.perm.is_conj_of_cycle_type_eq {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} (h : σ.cycle_type = τ.cycle_type) :
is_conj σ τ
source
theorem equiv.perm.is_conj_iff_cycle_type_eq {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} :
is_conj σ τ ↔ σ.cycle_type = τ.cycle_type
source
@[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
source
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
source
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
source
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) :
H = ⊤
source
def equiv.perm.partition {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
partition (fintype.card α)

The partition corresponding to a permutation

Equations
source
theorem equiv.perm.parts_partition {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
σ.partition.parts = σ.cycle_type + multiset.repeat 1 (fintype.card α - σ.support.card)
source
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
source
theorem equiv.perm.partition_eq_of_is_conj {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} :
is_conj σ τ ↔ σ.partition = τ.partition

3-cycles #

source
def equiv.perm.is_three_cycle {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
Prop

A three-cycle is a cycle of length 3.

Equations
source
theorem equiv.perm.is_three_cycle.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h : σ.is_three_cycle) :
σ.cycle_type = {3}
source
theorem equiv.perm.is_three_cycle.card_support {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h : σ.is_three_cycle) :
σ.support.card = 3
source
theorem card_support_eq_three_iff {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
σ.support.card = 3 ↔ σ.is_three_cycle
source
theorem equiv.perm.is_three_cycle.is_cycle {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h : σ.is_three_cycle) :
σ.is_cycle
source
theorem equiv.perm.is_three_cycle.sign {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h : σ.is_three_cycle) :
⇑equiv.perm.sign σ = 1
source
theorem equiv.perm.is_three_cycle.inv {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} (h : f.is_three_cycle) :
f⁻¹.is_three_cycle
source
@[simp]
theorem equiv.perm.is_three_cycle.inv_iff {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} :
f⁻¹.is_three_cycle ↔ f.is_three_cycle
source
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
source
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}
source
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}