mathlib3 documentation

group_theory.perm.cycle.basic

Cyclic permutations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file develops the theory of cycles in permutations.

Main definitions #

In the following, f : equiv.perm β.

The following two definitions require that β is a fintype:

Main results #

Notes #

equiv.perm.is_cycle and equiv.perm.is_cycle_on are different in three ways:

same_cycle #

source
def equiv.perm.same_cycle {α : Type u_2} (f : equiv.perm α) (x y : α) :
Prop

The equivalence relation indicating that two points are in the same cycle of a permutation.

Equations
Instances for equiv.perm.same_cycle
source
@[refl]
theorem equiv.perm.same_cycle.refl {α : Type u_2} (f : equiv.perm α) (x : α) :
f.same_cycle x x
source
theorem equiv.perm.same_cycle.rfl {α : Type u_2} {f : equiv.perm α} {x : α} :
f.same_cycle x x
source
@[protected]
theorem eq.same_cycle {α : Type u_2} {x y : α} (h : x = y) (f : equiv.perm α) :
f.same_cycle x y
source
@[symm]
theorem equiv.perm.same_cycle.symm {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → f.same_cycle y x
source
theorem equiv.perm.same_cycle_comm {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y ↔ f.same_cycle y x
source
@[trans]
theorem equiv.perm.same_cycle.trans {α : Type u_2} {f : equiv.perm α} {x y z : α} :
f.same_cycle x y → f.same_cycle y z → f.same_cycle x z
source
@[simp]
theorem equiv.perm.same_cycle_one {α : Type u_2} {x y : α} :
1.same_cycle x y ↔ x = y
source
@[simp]
theorem equiv.perm.same_cycle_inv {α : Type u_2} {f : equiv.perm α} {x y : α} :
f⁻¹.same_cycle x y ↔ f.same_cycle x y
source
theorem equiv.perm.same_cycle.of_inv {α : Type u_2} {f : equiv.perm α} {x y : α} :
f⁻¹.same_cycle x y → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_inv.

source
theorem equiv.perm.same_cycle.inv {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → f⁻¹.same_cycle x y

Alias of the reverse direction of equiv.perm.same_cycle_inv.

source
@[simp]
theorem equiv.perm.same_cycle_conj {α : Type u_2} {f g : equiv.perm α} {x y : α} :
(g * f * g⁻¹).same_cycle x y ↔ f.same_cycle (⇑g⁻¹ x) (⇑g⁻¹ y)
source
theorem equiv.perm.same_cycle.conj {α : Type u_2} {f g : equiv.perm α} {x y : α} :
f.same_cycle x y → (g * f * g⁻¹).same_cycle (⇑g x) (⇑g y)
source
theorem equiv.perm.same_cycle.apply_eq_self_iff {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → (⇑f x = x ↔ ⇑f y = y)
source
theorem equiv.perm.same_cycle.eq_of_left {α : Type u_2} {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) (hx : function.is_fixed_pt ⇑f x) :
x = y
source
theorem equiv.perm.same_cycle.eq_of_right {α : Type u_2} {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) (hy : function.is_fixed_pt ⇑f y) :
x = y
source
@[simp]
theorem equiv.perm.same_cycle_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle (⇑f x) y ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x (⇑f y) ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_inv_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle (⇑f⁻¹ x) y ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_inv_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x (⇑f⁻¹ y) ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_zpow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
f.same_cycle (⇑(f ^ n) x) y ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_zpow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
f.same_cycle x (⇑(f ^ n) y) ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_pow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
f.same_cycle (⇑(f ^ n) x) y ↔ f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_pow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
f.same_cycle x (⇑(f ^ n) y) ↔ f.same_cycle x y
source
theorem equiv.perm.same_cycle.of_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle (⇑f x) y → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_apply_left.

source
theorem equiv.perm.same_cycle.apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → f.same_cycle (⇑f x) y

Alias of the reverse direction of equiv.perm.same_cycle_apply_left.

source
theorem equiv.perm.same_cycle.of_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x (⇑f y) → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_apply_right.

source
theorem equiv.perm.same_cycle.apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → f.same_cycle x (⇑f y)

Alias of the reverse direction of equiv.perm.same_cycle_apply_right.

source
theorem equiv.perm.same_cycle.inv_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → f.same_cycle (⇑f⁻¹ x) y

Alias of the reverse direction of equiv.perm.same_cycle_inv_apply_left.

source
theorem equiv.perm.same_cycle.of_inv_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle (⇑f⁻¹ x) y → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_inv_apply_left.

source
theorem equiv.perm.same_cycle.inv_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y → f.same_cycle x (⇑f⁻¹ y)

Alias of the reverse direction of equiv.perm.same_cycle_inv_apply_right.

source
theorem equiv.perm.same_cycle.of_inv_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x (⇑f⁻¹ y) → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_inv_apply_right.

source
theorem equiv.perm.same_cycle.of_pow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
f.same_cycle (⇑(f ^ n) x) y → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_pow_left.

source
theorem equiv.perm.same_cycle.pow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
f.same_cycle x y → f.same_cycle (⇑(f ^ n) x) y

Alias of the reverse direction of equiv.perm.same_cycle_pow_left.

source
theorem equiv.perm.same_cycle.pow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
f.same_cycle x y → f.same_cycle x (⇑(f ^ n) y)

Alias of the reverse direction of equiv.perm.same_cycle_pow_right.

source
theorem equiv.perm.same_cycle.of_pow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
f.same_cycle x (⇑(f ^ n) y) → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_pow_right.

source
theorem equiv.perm.same_cycle.zpow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
f.same_cycle x y → f.same_cycle (⇑(f ^ n) x) y

Alias of the reverse direction of equiv.perm.same_cycle_zpow_left.

source
theorem equiv.perm.same_cycle.of_zpow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
f.same_cycle (⇑(f ^ n) x) y → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_zpow_left.

source
theorem equiv.perm.same_cycle.zpow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
f.same_cycle x y → f.same_cycle x (⇑(f ^ n) y)

Alias of the reverse direction of equiv.perm.same_cycle_zpow_right.

source
theorem equiv.perm.same_cycle.of_zpow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
f.same_cycle x (⇑(f ^ n) y) → f.same_cycle x y

Alias of the forward direction of equiv.perm.same_cycle_zpow_right.

source
theorem equiv.perm.same_cycle.of_pow {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℕ} :
(f ^ n).same_cycle x y → f.same_cycle x y
source
theorem equiv.perm.same_cycle.of_zpow {α : Type u_2} {f : equiv.perm α} {x y : α} {n : ℤ} :
(f ^ n).same_cycle x y → f.same_cycle x y
source
@[simp]
theorem equiv.perm.same_cycle_subtype_perm {α : Type u_2} {f : equiv.perm α} {p : α → Prop} {h : ∀ (x : α), p x ↔ p (⇑f x)} {x y : {x // p x}} :
(f.subtype_perm h).same_cycle x y ↔ f.same_cycle ↑x ↑y
source
theorem equiv.perm.same_cycle.subtype_perm {α : Type u_2} {f : equiv.perm α} {p : α → Prop} {h : ∀ (x : α), p x ↔ p (⇑f x)} {x y : {x // p x}} :
f.same_cycle ↑x ↑y → (f.subtype_perm h).same_cycle x y

Alias of the reverse direction of equiv.perm.same_cycle_subtype_perm.

source
@[simp]
theorem equiv.perm.same_cycle_extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {x y : α} {p : β → Prop} [decidable_pred p] {f : α ≃ subtype p} :
(g.extend_domain f).same_cycle ↑(⇑f x) ↑(⇑f y) ↔ g.same_cycle x y
source
theorem equiv.perm.same_cycle.extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {x y : α} {p : β → Prop} [decidable_pred p] {f : α ≃ subtype p} :
g.same_cycle x y → (g.extend_domain f).same_cycle ↑(⇑f x) ↑(⇑f y)

Alias of the reverse direction of equiv.perm.same_cycle_extend_domain.

source
theorem equiv.perm.same_cycle.exists_pow_eq' {α : Type u_2} {f : equiv.perm α} {x y : α} [finite α] :
f.same_cycle x y → (∃ (i : ℕ) (H : i < order_of f), ⇑(f ^ i) x = y)
source
theorem equiv.perm.same_cycle.exists_pow_eq'' {α : Type u_2} {f : equiv.perm α} {x y : α} [finite α] (h : f.same_cycle x y) :
∃ (i : ℕ) (hpos : 0 < i) (h : i ≤ order_of f), ⇑(f ^ i) x = y
source
@[protected, instance]
def equiv.perm.same_cycle.decidable_rel {α : Type u_2} [fintype α] [decidable_eq α] (f : equiv.perm α) :
decidable_rel f.same_cycle
Equations

is_cycle #

source
def equiv.perm.is_cycle {α : Type u_2} (f : equiv.perm α) :
Prop

A cycle is a non identity permutation where any two nonfixed points of the permutation are related by repeated application of the permutation.

Equations
source
theorem equiv.perm.is_cycle.ne_one {α : Type u_2} {f : equiv.perm α} (h : f.is_cycle) :
f ≠ 1
source
@[simp]
theorem equiv.perm.not_is_cycle_one {α : Type u_2} :
¬1.is_cycle
source
@[protected]
theorem equiv.perm.is_cycle.same_cycle {α : Type u_2} {f : equiv.perm α} {x y : α} (hf : f.is_cycle) (hx : ⇑f x ≠ x) (hy : ⇑f y ≠ y) :
f.same_cycle x y
source
theorem equiv.perm.is_cycle.exists_zpow_eq {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.is_cycle → ⇑f x ≠ x → ⇑f y ≠ y → (∃ (i : ℤ), ⇑(f ^ i) x = y)
source
theorem equiv.perm.is_cycle.inv {α : Type u_2} {f : equiv.perm α} (hf : f.is_cycle) :
f⁻¹.is_cycle
source
@[simp]
theorem equiv.perm.is_cycle_inv {α : Type u_2} {f : equiv.perm α} :
f⁻¹.is_cycle ↔ f.is_cycle
source
theorem equiv.perm.is_cycle.conj {α : Type u_2} {f g : equiv.perm α} :
f.is_cycle → (g * f * g⁻¹).is_cycle
source
@[protected]
theorem equiv.perm.is_cycle.extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) :
g.is_cycle → (g.extend_domain f).is_cycle
source
theorem equiv.perm.is_cycle_iff_same_cycle {α : Type u_2} {f : equiv.perm α} {x : α} (hx : ⇑f x ≠ x) :
f.is_cycle ↔ ∀ {y : α}, f.same_cycle x y ↔ ⇑f y ≠ y
source
theorem equiv.perm.is_cycle.exists_pow_eq {α : Type u_2} {f : equiv.perm α} {x y : α} [finite α] (hf : f.is_cycle) (hx : ⇑f x ≠ x) (hy : ⇑f y ≠ y) :
∃ (i : ℕ), ⇑(f ^ i) x = y
source
theorem equiv.perm.is_cycle_swap {α : Type u_2} {x y : α} [decidable_eq α] (hxy : x ≠ y) :
(equiv.swap x y).is_cycle
source
@[protected]
theorem equiv.perm.is_swap.is_cycle {α : Type u_2} {f : equiv.perm α} [decidable_eq α] :
f.is_swap → f.is_cycle
source
theorem equiv.perm.is_cycle.two_le_card_support {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (h : f.is_cycle) :
2 ≤ f.support.card
source
theorem equiv.perm.is_cycle.exists_pow_eq_one {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) :
∃ (k : ℕ) (hk : 1 < k), f ^ k = 1
source
noncomputable def equiv.perm.is_cycle.zpowers_equiv_support {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) :
↥↑(subgroup.zpowers σ) ≃ ↥↑(σ.support)

The subgroup generated by a cycle is in bijection with its support

Equations
source
@[simp]
theorem equiv.perm.is_cycle.zpowers_equiv_support_apply {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) {n : ℕ} :
⇑(hσ.zpowers_equiv_support) ⟨σ ^ n, _⟩ = ⟨⇑(σ ^ n) (classical.some hσ), _⟩
source
@[simp]
theorem equiv.perm.is_cycle.zpowers_equiv_support_symm_apply {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) (n : ℕ) :
⇑(hσ.zpowers_equiv_support.symm) ⟨⇑(σ ^ n) (classical.some hσ), _⟩ = ⟨σ ^ n, _⟩
source
@[protected]
theorem equiv.perm.is_cycle.order_of {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) :
order_of f = f.support.card
source
theorem equiv.perm.is_cycle_swap_mul_aux₁ {α : Type u_1} [decidable_eq α] (n : ℕ) {b x : α} {f : equiv.perm α} (hb : ⇑(equiv.swap x (⇑f x) * f) b ≠ b) (h : ⇑(f ^ n) (⇑f x) = b) :
∃ (i : ℤ), ⇑((equiv.swap x (⇑f x) * f) ^ i) (⇑f x) = b
source
theorem equiv.perm.is_cycle_swap_mul_aux₂ {α : Type u_1} [decidable_eq α] (n : ℤ) {b x : α} {f : equiv.perm α} (hb : ⇑(equiv.swap x (⇑f x) * f) b ≠ b) (h : ⇑(f ^ n) (⇑f x) = b) :
∃ (i : ℤ), ⇑((equiv.swap x (⇑f x) * f) ^ i) (⇑f x) = b
source
theorem equiv.perm.is_cycle.eq_swap_of_apply_apply_eq_self {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hfx : ⇑f x ≠ x) (hffx : ⇑f (⇑f x) = x) :
f = equiv.swap x (⇑f x)
source
theorem equiv.perm.is_cycle.swap_mul {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hx : ⇑f x ≠ x) (hffx : ⇑f (⇑f x) ≠ x) :
(equiv.swap x (⇑f x) * f).is_cycle
source
theorem equiv.perm.is_cycle.sign {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) :
⇑equiv.perm.sign f = -(-1) ^ f.support.card
source
theorem equiv.perm.is_cycle.of_pow {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] {n : ℕ} (h1 : (f ^ n).is_cycle) (h2 : f.support ⊆ (f ^ n).support) :
f.is_cycle
source
theorem equiv.perm.is_cycle.of_zpow {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] {n : ℤ} (h1 : (f ^ n).is_cycle) (h2 : f.support ⊆ (f ^ n).support) :
f.is_cycle
source
theorem equiv.perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : list (equiv.perm β)} (h1 : ∀ (f : equiv.perm β), f ∈ l → f.is_cycle) (h2 : list.pairwise equiv.perm.disjoint l) :
l.nodup
source
theorem equiv.perm.is_cycle.support_congr {α : Type u_2} {f g : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) (hg : g.is_cycle) (h : f.support ⊆ g.support) (h' : ∀ (x : α), x ∈ f.support → ⇑f x = ⇑g x) :
f = g

Unlike support_congr, which assumes that ∀ (x ∈ g.support), f x = g x), here we have the weaker assumption that ∀ (x ∈ f.support), f x = g x.

source
theorem equiv.perm.is_cycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f g : equiv.perm α} {x : α} [decidable_eq α] [fintype α] (hf : f.is_cycle) (hg : g.is_cycle) (h : ∀ (x : α), x ∈ f.support ∩ g.support → ⇑f x = ⇑g x) (hx : ⇑f x = ⇑g x) (hx' : x ∈ f.support) :
f = g

If two cyclic permutations agree on all terms in their intersection, and that intersection is not empty, then the two cyclic permutations must be equal.

source
theorem equiv.perm.is_cycle.support_pow_eq_iff {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) {n : ℕ} :
(f ^ n).support = f.support ↔ ¬order_of f ∣ n
source
theorem equiv.perm.is_cycle.support_pow_of_pos_of_lt_order_of {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) {n : ℕ} (npos : 0 < n) (hn : n < order_of f) :
(f ^ n).support = f.support
source
theorem equiv.perm.is_cycle.pow_iff {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : ℕ} :
(f ^ n).is_cycle ↔ n.coprime (order_of f)
source
theorem equiv.perm.is_cycle.pow_eq_one_iff {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : ℕ} :
f ^ n = 1 ↔ ∃ (x : β), ⇑f x ≠ x ∧ ⇑(f ^ n) x = x
source
theorem equiv.perm.is_cycle.pow_eq_one_iff' {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : ℕ} {x : β} (hx : ⇑f x ≠ x) :
f ^ n = 1 ↔ ⇑(f ^ n) x = x
source
theorem equiv.perm.is_cycle.pow_eq_one_iff'' {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : ℕ} :
f ^ n = 1 ↔ ∀ (x : β), ⇑f x ≠ x → ⇑(f ^ n) x = x
source
theorem equiv.perm.is_cycle.pow_eq_pow_iff {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {a b : ℕ} :
f ^ a = f ^ b ↔ ∃ (x : β), ⇑f x ≠ x ∧ ⇑(f ^ a) x = ⇑(f ^ b) x
source
theorem equiv.perm.is_cycle.is_cycle_pow_pos_of_lt_prime_order {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) (hf' : nat.prime (order_of f)) (n : ℕ) (hn : 0 < n) (hn' : n < order_of f) :
(f ^ n).is_cycle

is_cycle_on #

source
def equiv.perm.is_cycle_on {α : Type u_2} (f : equiv.perm α) (s : set α) :
Prop

A permutation is a cycle on s when any two points of s are related by repeated application of the permutation. Note that this means the identity is a cycle of subsingleton sets.

Equations
source
@[simp]
theorem equiv.perm.is_cycle_on_empty {α : Type u_2} {f : equiv.perm α} :
f.is_cycle_on ∅
source
@[simp]
theorem equiv.perm.is_cycle_on_one {α : Type u_2} {s : set α} :
1.is_cycle_on s ↔ s.subsingleton
source
theorem set.subsingleton.is_cycle_on_one {α : Type u_2} {s : set α} :
s.subsingleton → 1.is_cycle_on s

Alias of the reverse direction of equiv.perm.is_cycle_on_one.

source
theorem equiv.perm.is_cycle_on.subsingleton {α : Type u_2} {s : set α} :
1.is_cycle_on s → s.subsingleton

Alias of the forward direction of equiv.perm.is_cycle_on_one.

source
@[simp]
theorem equiv.perm.is_cycle_on_singleton {α : Type u_2} {f : equiv.perm α} {a : α} :
f.is_cycle_on {a} ↔ ⇑f a = a
source
theorem equiv.perm.is_cycle_on_of_subsingleton {α : Type u_2} [subsingleton α] (f : equiv.perm α) (s : set α) :
f.is_cycle_on s
source
@[simp]
theorem equiv.perm.is_cycle_on_inv {α : Type u_2} {f : equiv.perm α} {s : set α} :
f⁻¹.is_cycle_on s ↔ f.is_cycle_on s
source
theorem equiv.perm.is_cycle_on.of_inv {α : Type u_2} {f : equiv.perm α} {s : set α} :
f⁻¹.is_cycle_on s → f.is_cycle_on s

Alias of the forward direction of equiv.perm.is_cycle_on_inv.

source
theorem equiv.perm.is_cycle_on.inv {α : Type u_2} {f : equiv.perm α} {s : set α} :
f.is_cycle_on s → f⁻¹.is_cycle_on s

Alias of the reverse direction of equiv.perm.is_cycle_on_inv.

source
theorem equiv.perm.is_cycle_on.conj {α : Type u_2} {f g : equiv.perm α} {s : set α} (h : f.is_cycle_on s) :
(g * f * g⁻¹).is_cycle_on (⇑g '' s)
source
theorem equiv.perm.is_cycle_on_swap {α : Type u_2} {a b : α} [decidable_eq α] (hab : a ≠ b) :
(equiv.swap a b).is_cycle_on {a, b}
source
@[protected]
theorem equiv.perm.is_cycle_on.apply_ne {α : Type u_2} {f : equiv.perm α} {s : set α} {a : α} (hf : f.is_cycle_on s) (hs : s.nontrivial) (ha : a ∈ s) :
⇑f a ≠ a
source
@[protected]
theorem equiv.perm.is_cycle.is_cycle_on {α : Type u_2} {f : equiv.perm α} (hf : f.is_cycle) :
f.is_cycle_on {x : α | ⇑f x ≠ x}
source
theorem equiv.perm.is_cycle_iff_exists_is_cycle_on {α : Type u_2} {f : equiv.perm α} :
f.is_cycle ↔ ∃ (s : set α), s.nontrivial ∧ f.is_cycle_on s ∧ ∀ ⦃x : α⦄, ¬function.is_fixed_pt ⇑f x → x ∈ s

This lemma demonstrates the relation between equiv.perm.is_cycle and equiv.perm.is_cycle_on in non-degenerate cases.

source
theorem equiv.perm.is_cycle_on.apply_mem_iff {α : Type u_2} {f : equiv.perm α} {s : set α} {x : α} (hf : f.is_cycle_on s) :
⇑f x ∈ s ↔ x ∈ s
source
theorem equiv.perm.is_cycle_on.is_cycle_subtype_perm {α : Type u_2} {f : equiv.perm α} {s : set α} (hf : f.is_cycle_on s) (hs : s.nontrivial) :
(f.subtype_perm _).is_cycle

Note that the identity satisfies is_cycle_on for any subsingleton set, but not is_cycle.

source
@[protected]
theorem equiv.perm.is_cycle_on.subtype_perm {α : Type u_2} {f : equiv.perm α} {s : set α} (hf : f.is_cycle_on s) :
(f.subtype_perm _).is_cycle_on set.univ

Note that the identity is a cycle on any subsingleton set, but not a cycle.

source
theorem equiv.perm.is_cycle_on.pow_apply_eq {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on ↑s) (ha : a ∈ s) {n : ℕ} :
⇑(f ^ n) a = a ↔ s.card ∣ n
source
theorem equiv.perm.is_cycle_on.zpow_apply_eq {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on ↑s) (ha : a ∈ s) {n : ℤ} :
⇑(f ^ n) a = a ↔ ↑(s.card) ∣ n
source
theorem equiv.perm.is_cycle_on.pow_apply_eq_pow_apply {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on ↑s) (ha : a ∈ s) {m n : ℕ} :
⇑(f ^ m) a = ⇑(f ^ n) a ↔ m ≡ n [MOD s.card]
source
theorem equiv.perm.is_cycle_on.zpow_apply_eq_zpow_apply {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on ↑s) (ha : a ∈ s) {m n : ℤ} :
⇑(f ^ m) a = ⇑(f ^ n) a ↔ m ≡ n [ZMOD ↑(s.card)]
source
theorem equiv.perm.is_cycle_on.pow_card_apply {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on ↑s) (ha : a ∈ s) :
⇑(f ^ s.card) a = a
source
theorem equiv.perm.is_cycle_on.exists_pow_eq {α : Type u_2} {f : equiv.perm α} {a b : α} {s : finset α} (hf : f.is_cycle_on ↑s) (ha : a ∈ s) (hb : b ∈ s) :
∃ (n : ℕ) (H : n < s.card), ⇑(f ^ n) a = b
source
theorem equiv.perm.is_cycle_on.exists_pow_eq' {α : Type u_2} {f : equiv.perm α} {s : set α} {a b : α} (hs : s.finite) (hf : f.is_cycle_on s) (ha : a ∈ s) (hb : b ∈ s) :
∃ (n : ℕ), ⇑(f ^ n) a = b
source
theorem equiv.perm.is_cycle_on.range_pow {α : Type u_2} {f : equiv.perm α} {s : set α} {a : α} (hs : s.finite) (h : f.is_cycle_on s) (ha : a ∈ s) :
set.range (λ (n : ℕ), ⇑(f ^ n) a) = s
source
theorem equiv.perm.is_cycle_on.range_zpow {α : Type u_2} {f : equiv.perm α} {s : set α} {a : α} (h : f.is_cycle_on s) (ha : a ∈ s) :
set.range (λ (n : ℤ), ⇑(f ^ n) a) = s
source
theorem equiv.perm.is_cycle_on.of_pow {α : Type u_2} {f : equiv.perm α} {s : set α} {n : ℕ} (hf : (f ^ n).is_cycle_on s) (h : set.bij_on ⇑f s s) :
f.is_cycle_on s
source
theorem equiv.perm.is_cycle_on.of_zpow {α : Type u_2} {f : equiv.perm α} {s : set α} {n : ℤ} (hf : (f ^ n).is_cycle_on s) (h : set.bij_on ⇑f s s) :
f.is_cycle_on s
source
theorem equiv.perm.is_cycle_on.extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {s : set α} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) (h : g.is_cycle_on s) :
(g.extend_domain f).is_cycle_on (coe ∘ ⇑f '' s)
source
@[protected]
theorem equiv.perm.is_cycle_on.countable {α : Type u_2} {f : equiv.perm α} {s : set α} (hs : f.is_cycle_on s) :
s.countable

cycle_of #

source
def equiv.perm.cycle_of {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
equiv.perm α

f.cycle_of x is the cycle of the permutation f to which x belongs.

Equations
source
theorem equiv.perm.cycle_of_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x y : α) :
⇑(f.cycle_of x) y = ite (f.same_cycle x y) (⇑f y) y
source
theorem equiv.perm.cycle_of_inv {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
(f.cycle_of x)⁻¹ = f⁻¹.cycle_of x
source
@[simp]
theorem equiv.perm.cycle_of_pow_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (n : ℕ) :
⇑(f.cycle_of x ^ n) x = ⇑(f ^ n) x
source
@[simp]
theorem equiv.perm.cycle_of_zpow_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (n : ℤ) :
⇑(f.cycle_of x ^ n) x = ⇑(f ^ n) x
source
theorem equiv.perm.same_cycle.cycle_of_apply {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
f.same_cycle x y → ⇑(f.cycle_of x) y = ⇑f y
source
theorem equiv.perm.cycle_of_apply_of_not_same_cycle {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
¬f.same_cycle x y → ⇑(f.cycle_of x) y = y
source
theorem equiv.perm.same_cycle.cycle_of_eq {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :
f.cycle_of x = f.cycle_of y
source
@[simp]
theorem equiv.perm.cycle_of_apply_apply_zpow_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (k : ℤ) :
⇑(f.cycle_of x) (⇑(f ^ k) x) = ⇑(f ^ (k + 1)) x
source
@[simp]
theorem equiv.perm.cycle_of_apply_apply_pow_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (k : ℕ) :
⇑(f.cycle_of x) (⇑(f ^ k) x) = ⇑(f ^ (k + 1)) x
source
@[simp]
theorem equiv.perm.cycle_of_apply_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
⇑(f.cycle_of x) (⇑f x) = ⇑f (⇑f x)
source
@[simp]
theorem equiv.perm.cycle_of_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
⇑(f.cycle_of x) x = ⇑f x
source
theorem equiv.perm.is_cycle.cycle_of_eq {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hf : f.is_cycle) (hx : ⇑f x ≠ x) :
f.cycle_of x = f
source
@[simp]
theorem equiv.perm.cycle_of_eq_one_iff {α : Type u_2} [decidable_eq α] [fintype α] {x : α} (f : equiv.perm α) :
f.cycle_of x = 1 ↔ ⇑f x = x
source
@[simp]
theorem equiv.perm.cycle_of_self_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
f.cycle_of (⇑f x) = f.cycle_of x
source
@[simp]
theorem equiv.perm.cycle_of_self_apply_pow {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ℕ) (x : α) :
f.cycle_of (⇑(f ^ n) x) = f.cycle_of x
source
@[simp]
theorem equiv.perm.cycle_of_self_apply_zpow {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ℤ) (x : α) :
f.cycle_of (⇑(f ^ n) x) = f.cycle_of x
source
@[protected]
theorem equiv.perm.is_cycle.cycle_of {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hf : f.is_cycle) :
f.cycle_of x = ite (⇑f x = x) 1 f
source
theorem equiv.perm.cycle_of_one {α : Type u_2} [decidable_eq α] [fintype α] (x : α) :
1.cycle_of x = 1
source
theorem equiv.perm.is_cycle_cycle_of {α : Type u_2} [decidable_eq α] [fintype α] {x : α} (f : equiv.perm α) (hx : ⇑f x ≠ x) :
(f.cycle_of x).is_cycle
source
@[simp]
theorem equiv.perm.two_le_card_support_cycle_of_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
2 ≤ (f.cycle_of x).support.card ↔ ⇑f x ≠ x
source
@[simp]
theorem equiv.perm.card_support_cycle_of_pos_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
0 < (f.cycle_of x).support.card ↔ ⇑f x ≠ x
source
theorem equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ℕ) (x : α) :
⇑(f ^ n) x = ⇑(f ^ (n % order_of (f.cycle_of x))) x
source
theorem equiv.perm.cycle_of_mul_of_apply_right_eq_self {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : commute f g) (x : α) (hx : ⇑g x = x) :
(f * g).cycle_of x = f.cycle_of x
source
theorem equiv.perm.disjoint.cycle_of_mul_distrib {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) (x : α) :
(f * g).cycle_of x = f.cycle_of x * g.cycle_of x
source
theorem equiv.perm.support_cycle_of_eq_nil_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
(f.cycle_of x).support = ∅ ↔ x ∉ f.support
source
theorem equiv.perm.support_cycle_of_le {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
(f.cycle_of x).support ≤ f.support
source
theorem equiv.perm.mem_support_cycle_of_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
y ∈ (f.cycle_of x).support ↔ f.same_cycle x y ∧ x ∈ f.support
source
theorem equiv.perm.mem_support_cycle_of_iff' {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (hx : ⇑f x ≠ x) :
y ∈ (f.cycle_of x).support ↔ f.same_cycle x y
source
theorem equiv.perm.same_cycle.mem_support_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :
x ∈ f.support ↔ y ∈ f.support
source
theorem equiv.perm.pow_mod_card_support_cycle_of_self_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ℕ) (x : α) :
⇑(f ^ (n % (f.cycle_of x).support.card)) x = ⇑(f ^ n) x
source
theorem equiv.perm.is_cycle_cycle_of_iff {α : Type u_2} [decidable_eq α] [fintype α] {x : α} (f : equiv.perm α) :
(f.cycle_of x).is_cycle ↔ ⇑f x ≠ x

x is in the support of f iff equiv.perm.cycle_of f x is a cycle.

source
theorem equiv.perm.is_cycle_on_support_cycle_of {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
f.is_cycle_on ↑((f.cycle_of x).support)
source
theorem equiv.perm.same_cycle.exists_pow_eq_of_mem_support {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) (hx : x ∈ f.support) :
∃ (i : ℕ) (hi' : i < (f.cycle_of x).support.card), ⇑(f ^ i) x = y
source
theorem equiv.perm.same_cycle.exists_pow_eq {α : Type u_2} [decidable_eq α] [fintype α] {x y : α} (f : equiv.perm α) (h : f.same_cycle x y) :
∃ (i : ℕ) (hi : 0 < i) (hi' : i ≤ (f.cycle_of x).support.card + 1), ⇑(f ^ i) x = y

cycle_factors #

source
def equiv.perm.cycle_factors_aux {α : Type u_2} [decidable_eq α] [fintype α] (l : list α) (f : equiv.perm α) :
(∀ {x : α}, ⇑f x ≠ x → x ∈ l) → {l // l.prod = f ∧ (∀ (g : equiv.perm α), g ∈ l → g.is_cycle) ∧ list.pairwise equiv.perm.disjoint l}

Given a list l : list α and a permutation f : perm α whose nonfixed points are all in l, recursively factors f into cycles.

Equations
source
theorem equiv.perm.mem_list_cycles_iff {α : Type u_1} [finite α] {l : list (equiv.perm α)} (h1 : ∀ (σ : equiv.perm α), σ ∈ l → σ.is_cycle) (h2 : list.pairwise equiv.perm.disjoint l) {σ : equiv.perm α} :
σ ∈ l ↔ σ.is_cycle ∧ ∀ (a : α), ⇑σ a ≠ a → ⇑σ a = ⇑(l.prod) a
source
theorem equiv.perm.list_cycles_perm_list_cycles {α : Type u_1} [finite α] {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_factors {α : Type u_2} [decidable_eq α] [fintype α] [linear_order α] (f : equiv.perm α) :
{l // l.prod = f ∧ (∀ (g : equiv.perm α), g ∈ l → g.is_cycle) ∧ list.pairwise equiv.perm.disjoint l}

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f.

Equations
source
def equiv.perm.trunc_cycle_factors {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) :
trunc {l // l.prod = f ∧ (∀ (g : equiv.perm α), g ∈ l → g.is_cycle) ∧ list.pairwise equiv.perm.disjoint l}

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f, without a linear order.

Equations
source
def equiv.perm.cycle_factors_finset {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) :
finset (equiv.perm α)

Factors a permutation f into a finset of disjoint cyclic permutations that multiply to f.

Equations
source
theorem equiv.perm.cycle_factors_finset_eq_list_to_finset {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} {l : list (equiv.perm α)} (hn : l.nodup) :
σ.cycle_factors_finset = l.to_finset ↔ (∀ (f : equiv.perm α), f ∈ l → f.is_cycle) ∧ list.pairwise equiv.perm.disjoint l ∧ l.prod = σ
source
theorem equiv.perm.cycle_factors_finset_eq_finset {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} {s : finset (equiv.perm α)} :
σ.cycle_factors_finset = s ↔ (∀ (f : equiv.perm α), f ∈ s → f.is_cycle) ∧ ∃ (h : ↑s.pairwise equiv.perm.disjoint), s.noncomm_prod id _ = σ
source
theorem equiv.perm.cycle_factors_finset_pairwise_disjoint {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) :
↑(f.cycle_factors_finset).pairwise equiv.perm.disjoint
source
theorem equiv.perm.cycle_factors_finset_mem_commute {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) :
↑(f.cycle_factors_finset).pairwise commute
source
theorem equiv.perm.cycle_factors_finset_noncomm_prod {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (comm : ↑(f.cycle_factors_finset).pairwise commute := _) :
f.cycle_factors_finset.noncomm_prod id comm = f

The product of cycle factors is equal to the original f : perm α.

source
theorem equiv.perm.mem_cycle_factors_finset_iff {α : Type u_2} [decidable_eq α] [fintype α] {f p : equiv.perm α} :
p ∈ f.cycle_factors_finset ↔ p.is_cycle ∧ ∀ (a : α), a ∈ p.support → ⇑p a = ⇑f a
source
theorem equiv.perm.cycle_of_mem_cycle_factors_finset_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
f.cycle_of x ∈ f.cycle_factors_finset ↔ x ∈ f.support
source
theorem equiv.perm.mem_cycle_factors_finset_support_le {α : Type u_2} [decidable_eq α] [fintype α] {p f : equiv.perm α} (h : p ∈ f.cycle_factors_finset) :
p.support ≤ f.support
source
theorem equiv.perm.cycle_factors_finset_eq_empty_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.cycle_factors_finset = ∅ ↔ f = 1
source
@[simp]
theorem equiv.perm.cycle_factors_finset_one {α : Type u_2} [decidable_eq α] [fintype α] :
1.cycle_factors_finset = ∅
source
@[simp]
theorem equiv.perm.cycle_factors_finset_eq_singleton_self_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.cycle_factors_finset = {f} ↔ f.is_cycle
source
theorem equiv.perm.is_cycle.cycle_factors_finset_eq_singleton {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) :
f.cycle_factors_finset = {f}
source
theorem equiv.perm.cycle_factors_finset_eq_singleton_iff {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} :
f.cycle_factors_finset = {g} ↔ f.is_cycle ∧ f = g
source
theorem equiv.perm.cycle_factors_finset_injective {α : Type u_2} [decidable_eq α] [fintype α] :
function.injective equiv.perm.cycle_factors_finset

Two permutations f g : perm α have the same cycle factors iff they are the same.

source
theorem equiv.perm.disjoint.disjoint_cycle_factors_finset {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
disjoint f.cycle_factors_finset g.cycle_factors_finset
source
theorem equiv.perm.disjoint.cycle_factors_finset_mul_eq_union {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
(f * g).cycle_factors_finset = f.cycle_factors_finset ∪ g.cycle_factors_finset
source
theorem equiv.perm.disjoint_mul_inv_of_mem_cycle_factors_finset {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f ∈ g.cycle_factors_finset) :
(g * f⁻¹).disjoint f
source
theorem equiv.perm.cycle_is_cycle_of {α : Type u_2} [decidable_eq α] [fintype α] {f c : equiv.perm α} {a : α} (ha : a ∈ c.support) (hc : c ∈ f.cycle_factors_finset) :
c = f.cycle_of a

If c is a cycle, a ∈ c.support and c is a cycle of f, then c = f.cycle_of a

source
theorem equiv.perm.cycle_induction_on {β : Type u_3} [finite β] (P : equiv.perm β → Prop) (σ : equiv.perm β) (base_one : P 1) (base_cycles : ∀ (σ : equiv.perm β), σ.is_cycle → P σ) (induction_disjoint : ∀ (σ τ : equiv.perm β), σ.disjoint τ → σ.is_cycle → P σ → P τ → P (σ * τ)) :
P σ
source
theorem equiv.perm.cycle_factors_finset_mul_inv_mem_eq_sdiff {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f ∈ g.cycle_factors_finset) :
(g * f⁻¹).cycle_factors_finset = g.cycle_factors_finset \ {f}
source
theorem equiv.perm.closure_is_cycle {β : Type u_3} [finite β] :
subgroup.closure {σ : equiv.perm β | σ.is_cycle} = ⊤
source
theorem equiv.perm.closure_cycle_adjacent_swap {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h1 : σ.is_cycle) (h2 : σ.support = ⊤) (x : α) :
subgroup.closure {σ, equiv.swap x (⇑σ x)} = ⊤
source
theorem equiv.perm.closure_cycle_coprime_swap {α : Type u_2} [decidable_eq α] [fintype α] {n : ℕ} {σ : equiv.perm α} (h0 : n.coprime (fintype.card α)) (h1 : σ.is_cycle) (h2 : σ.support = finset.univ) (x : α) :
subgroup.closure {σ, equiv.swap x (⇑(σ ^ n) x)} = ⊤
source
theorem equiv.perm.closure_prime_cycle_swap {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (h0 : nat.prime (fintype.card α)) (h1 : σ.is_cycle) (h2 : σ.support = finset.univ) (h3 : τ.is_swap) :
subgroup.closure {σ, τ} = ⊤
source
theorem equiv.perm.is_conj_of_support_equiv {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (f : {x // x ∈ ↑(σ.support)} ≃ {x // x ∈ ↑(τ.support)}) (hf : ∀ (x : α) (hx : x ∈ ↑(σ.support)), ↑(⇑f ⟨⇑σ x, _⟩) = ⇑τ ↑(⇑f ⟨x, hx⟩)) :
is_conj σ τ
source
theorem equiv.perm.is_cycle.is_conj {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) (h : σ.support.card = τ.support.card) :
is_conj σ τ
source
theorem equiv.perm.is_cycle.is_conj_iff {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) :
is_conj σ τ ↔ σ.support.card = τ.support.card
source
@[simp]
theorem equiv.perm.support_conj {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
(σ * τ * σ⁻¹).support = finset.map (equiv.to_embedding σ) τ.support
source
theorem equiv.perm.card_support_conj {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
(σ * τ * σ⁻¹).support.card = τ.support.card
source
theorem equiv.perm.disjoint.is_conj_mul {α : Type u_1} [finite α] {σ τ π ρ : equiv.perm α} (hc1 : is_conj σ π) (hc2 : is_conj τ ρ) (hd1 : σ.disjoint τ) (hd2 : π.disjoint ρ) :
is_conj (σ * τ) (π * ρ)

Fixed points #

source
theorem equiv.perm.fixed_point_card_lt_of_ne_one {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h : σ ≠ 1) :
(finset.filter (λ (x : α), ⇑σ x = x) finset.univ).card < fintype.card α - 1
source
theorem list.nodup.is_cycle_on_form_perm {α : Type u_2} [decidable_eq α] {l : list α} (h : l.nodup) :
l.form_perm.is_cycle_on {a : α | a ∈ l}
source
theorem int.add_left_one_is_cycle  :
(equiv.add_left 1).is_cycle
source
theorem int.add_right_one_is_cycle  :
(equiv.add_right 1).is_cycle
source
theorem finset.exists_cycle_on {α : Type u_2} [decidable_eq α] [fintype α] (s : finset α) :
∃ (f : equiv.perm α), f.is_cycle_on ↑s ∧ f.support ⊆ s
source
theorem set.countable.exists_cycle_on {α : Type u_2} {s : set α} (hs : s.countable) :
∃ (f : equiv.perm α), f.is_cycle_on s ∧ {x : α | ⇑f x ≠ x} ⊆ s
source
theorem set.prod_self_eq_Union_perm {α : Type u_2} {f : equiv.perm α} {s : set α} (hf : f.is_cycle_on s) :
s ×ˢ s = ⋃ (n : ℤ), (λ (a : α), (a, ⇑(f ^ n) a)) '' s
source
theorem finset.product_self_eq_disj_Union_perm_aux {α : Type u_2} {f : equiv.perm α} {s : finset α} (hf : f.is_cycle_on ↑s) :
↑(finset.range s.card).pairwise_disjoint (λ (k : ℕ), finset.map {to_fun := λ (i : α), (i, ⇑(f ^ k) i), inj' := _} s)
source
theorem finset.product_self_eq_disj_Union_perm {α : Type u_2} {f : equiv.perm α} {s : finset α} (hf : f.is_cycle_on ↑s) :
s ×ˢ s = (finset.range s.card).disj_Union (λ (k : ℕ), finset.map {to_fun := λ (i : α), (i, ⇑(f ^ k) i), inj' := _} s) _

We can partition the square s ×ˢ s into shifted diagonals as such:

01234
40123
34012
23401
12340

The diagonals are given by the cycle f.

source
theorem finset.sum_smul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [semiring α] [add_comm_monoid β] [module α β] {s : finset ι} {σ : equiv.perm ι} (hσ : σ.is_cycle_on ↑s) (f : ι → α) (g : ι → β) :
s.sum (λ (i : ι), f i) • s.sum (λ (i : ι), g i) = (finset.range s.card).sum (λ (k : ℕ), s.sum (λ (i : ι), f i • g (⇑(σ ^ k) i)))
source
theorem finset.sum_mul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} [semiring α] {s : finset ι} {σ : equiv.perm ι} (hσ : σ.is_cycle_on ↑s) (f g : ι → α) :
s.sum (λ (i : ι), f i) * s.sum (λ (i : ι), g i) = (finset.range s.card).sum (λ (k : ℕ), s.sum (λ (i : ι), f i * g (⇑(σ ^ k) i)))