Cyclic permutations

This file develops the theory of cycles in permutations.

Main definitions

In the following, f : Equiv.Perm β.

• Equiv.Perm.SameCycle: f.SameCycle x y when x and y are in the same cycle of f.
• Equiv.Perm.IsCycle: f is a cycle if any two nonfixed points of f are related by repeated applications of f, and f is not the identity.
• Equiv.Perm.IsCycleOn: f is a cycle on a set s when any two points of s are related by repeated applications of f.

The following two definitions require that β is a Fintype:

• Equiv.Perm.cycleOf: f.cycleOf x is the cycle of f that x belongs to.
• Equiv.Perm.cycleFactors: f.cycleFactors is a list of disjoint cyclic permutations that multiply to f.

Main results

• This file contains several closure results:
  • closure_is_cycle : The symmetric group is generated by cycles
  • closure_cycle_adjacent_swap : The symmetric group is generated by a cycle and an adjacent transposition
  • closure_cycle_coprime_swap : The symmetric group is generated by a cycle and a coprime transposition
  • closure_prime_cycle_swap : The symmetric group is generated by a prime cycle and a transposition

Notes

Equiv.Perm.is_cycle and Equiv.Perm.IsCycleOn are different in three ways:

• is_cycle is about the entire type while IsCycleOn is restricted to a set.
• is_cycle forbids the identity while IsCycleOn allows it (if s is a subsingleton).
• IsCycleOn forbids fixed points on s (if s is nontrivial), while is_cycle allows them.

SameCycle

def Equiv.Perm.SameCycle {α : 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

• Equiv.Perm.SameCycle f x y = ∃ i, ↑(f ^ i) x = y

theorem Equiv.Perm.SameCycle.refl {α : Type u_2} (f : Equiv.Perm α) (x : α) : Equiv.Perm.SameCycle f x x

theorem Equiv.Perm.SameCycle.rfl {α : Type u_2} {f : Equiv.Perm α} {x : α} : Equiv.Perm.SameCycle f x x

theorem Eq.sameCycle {α : Type u_2} {x : α} {y : α} (h : x = y) (f : Equiv.Perm α) : Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.SameCycle.symm {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f y x

theorem Equiv.Perm.sameCycle_comm {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y ↔ Equiv.Perm.SameCycle f y x

theorem Equiv.Perm.SameCycle.trans {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {z : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f y z → Equiv.Perm.SameCycle f x z

theorem Equiv.Perm.SameCycle.equivalence {α : Type u_2} (f : Equiv.Perm α) : Equivalence (Equiv.Perm.SameCycle f)

def Equiv.Perm.SameCycle.setoid {α : Type u_2} (f : Equiv.Perm α) : Setoid α

The setoid defined by the SameCycle relation.

Equations

• Equiv.Perm.SameCycle.setoid f = { r := Equiv.Perm.SameCycle f, iseqv := (_ : Equivalence (Equiv.Perm.SameCycle f)) }

@[simp]

theorem Equiv.Perm.sameCycle_one {α : Type u_2} {x : α} {y : α} : Equiv.Perm.SameCycle 1 x y ↔ x = y

@[simp]

theorem Equiv.Perm.sameCycle_inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f⁻¹ x y ↔ Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.SameCycle.inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f⁻¹ x y

Alias of the reverse direction of Equiv.Perm.sameCycle_inv.

theorem Equiv.Perm.SameCycle.of_inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f⁻¹ x y → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_inv.

@[simp]

theorem Equiv.Perm.sameCycle_conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle (g * f * g⁻¹) x y ↔ Equiv.Perm.SameCycle f (↑g⁻¹ x) (↑g⁻¹ y)

theorem Equiv.Perm.SameCycle.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle (g * f * g⁻¹) (↑g x) (↑g y)

theorem Equiv.Perm.SameCycle.apply_eq_self_iff {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → (↑f x = x ↔ ↑f y = y)

theorem Equiv.Perm.SameCycle.eq_of_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hx : Function.IsFixedPt (↑f) x) : x = y

theorem Equiv.Perm.SameCycle.eq_of_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hy : Function.IsFixedPt (↑f) y) : x = y

@[simp]

theorem Equiv.Perm.sameCycle_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f (↑f x) y ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x (↑f y) ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f (↑f⁻¹ x) y ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x (↑f⁻¹ y) ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle f (↑(f ^ n) x) y ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle f x (↑(f ^ n) y) ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle f (↑(f ^ n) x) y ↔ Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle f x (↑(f ^ n) y) ↔ Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.SameCycle.of_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f (↑f x) y → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_apply_left.

theorem Equiv.Perm.SameCycle.apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f (↑f x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_apply_left.

theorem Equiv.Perm.SameCycle.apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f x (↑f y)

Alias of the reverse direction of Equiv.Perm.sameCycle_apply_right.

theorem Equiv.Perm.SameCycle.of_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x (↑f y) → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_apply_right.

theorem Equiv.Perm.SameCycle.inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f (↑f⁻¹ x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_inv_apply_left.

theorem Equiv.Perm.SameCycle.of_inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f (↑f⁻¹ x) y → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_inv_apply_left.

theorem Equiv.Perm.SameCycle.inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f x (↑f⁻¹ y)

Alias of the reverse direction of Equiv.Perm.sameCycle_inv_apply_right.

theorem Equiv.Perm.SameCycle.of_inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x (↑f⁻¹ y) → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_inv_apply_right.

theorem Equiv.Perm.SameCycle.pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f (↑(f ^ n) x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_pow_left.

theorem Equiv.Perm.SameCycle.of_pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle f (↑(f ^ n) x) y → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_pow_left.

theorem Equiv.Perm.SameCycle.of_pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle f x (↑(f ^ n) y) → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_pow_right.

theorem Equiv.Perm.SameCycle.pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f x (↑(f ^ n) y)

Alias of the reverse direction of Equiv.Perm.sameCycle_pow_right.

theorem Equiv.Perm.SameCycle.of_zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle f (↑(f ^ n) x) y → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_zpow_left.

theorem Equiv.Perm.SameCycle.zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f (↑(f ^ n) x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_zpow_left.

theorem Equiv.Perm.SameCycle.zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle f x y → Equiv.Perm.SameCycle f x (↑(f ^ n) y)

Alias of the reverse direction of Equiv.Perm.sameCycle_zpow_right.

theorem Equiv.Perm.SameCycle.of_zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle f x (↑(f ^ n) y) → Equiv.Perm.SameCycle f x y

Alias of the forward direction of Equiv.Perm.sameCycle_zpow_right.

theorem Equiv.Perm.SameCycle.of_pow {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℕ} : Equiv.Perm.SameCycle (f ^ n) x y → Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.SameCycle.of_zpow {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : ℤ} : Equiv.Perm.SameCycle (f ^ n) x y → Equiv.Perm.SameCycle f x y

@[simp]

theorem Equiv.Perm.sameCycle_subtypePerm {α : Type u_2} {f : Equiv.Perm α} {p : α → Prop} {h : ∀ (x : α), p x ↔ p (↑f x)} {x : { x // p x }} {y : { x // p x }} : Equiv.Perm.SameCycle (Equiv.Perm.subtypePerm f h) x y ↔ Equiv.Perm.SameCycle f ↑x ↑y

theorem Equiv.Perm.SameCycle.subtypePerm {α : Type u_2} {f : Equiv.Perm α} {p : α → Prop} {h : ∀ (x : α), p x ↔ p (↑f x)} {x : { x // p x }} {y : { x // p x }} : Equiv.Perm.SameCycle f ↑x ↑y → Equiv.Perm.SameCycle (Equiv.Perm.subtypePerm f h) x y

Alias of the reverse direction of Equiv.Perm.sameCycle_subtypePerm.

@[simp]

theorem Equiv.Perm.sameCycle_extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x : α} {y : α} {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} : Equiv.Perm.SameCycle (Equiv.Perm.extendDomain g f) ↑(↑f x) ↑(↑f y) ↔ Equiv.Perm.SameCycle g x y

theorem Equiv.Perm.SameCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x : α} {y : α} {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} : Equiv.Perm.SameCycle g x y → Equiv.Perm.SameCycle (Equiv.Perm.extendDomain g f) ↑(↑f x) ↑(↑f y)

Alias of the reverse direction of Equiv.Perm.sameCycle_extendDomain.

theorem Equiv.Perm.SameCycle.exists_pow_eq' {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] : Equiv.Perm.SameCycle f x y → ∃ i, i < orderOf f ∧ ↑(f ^ i) x = y

theorem Equiv.Perm.SameCycle.exists_pow_eq'' {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] (h : Equiv.Perm.SameCycle f x y) : ∃ i x x, ↑(f ^ i) x = y

instance Equiv.Perm.instDecidableRelSameCycle {α : Type u_2} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) : DecidableRel (Equiv.Perm.SameCycle f)

Equations

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

IsCycle

def Equiv.Perm.IsCycle {α : 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

• Equiv.Perm.IsCycle f = ∃ x, ↑f x ≠ x ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.IsCycle.ne_one {α : Type u_2} {f : Equiv.Perm α} (h : Equiv.Perm.IsCycle f) : f ≠ 1

@[simp]

theorem Equiv.Perm.not_isCycle_one {α : Type u_2} : ¬Equiv.Perm.IsCycle 1

theorem Equiv.Perm.IsCycle.sameCycle {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (hf : Equiv.Perm.IsCycle f) (hx : ↑f x ≠ x) (hy : ↑f y ≠ y) : Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.IsCycle.exists_zpow_eq {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.IsCycle f → ↑f x ≠ x → ↑f y ≠ y → ∃ i, ↑(f ^ i) x = y

theorem Equiv.Perm.IsCycle.inv {α : Type u_2} {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : Equiv.Perm.IsCycle f⁻¹

@[simp]

theorem Equiv.Perm.isCycle_inv {α : Type u_2} {f : Equiv.Perm α} : Equiv.Perm.IsCycle f⁻¹ ↔ Equiv.Perm.IsCycle f

theorem Equiv.Perm.IsCycle.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} : Equiv.Perm.IsCycle f → Equiv.Perm.IsCycle (g * f * g⁻¹)

theorem Equiv.Perm.IsCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : Equiv.Perm.IsCycle g → Equiv.Perm.IsCycle (Equiv.Perm.extendDomain g f)

theorem Equiv.Perm.isCycle_iff_sameCycle {α : Type u_2} {f : Equiv.Perm α} {x : α} (hx : ↑f x ≠ x) : Equiv.Perm.IsCycle f ↔ ∀ {y : α}, Equiv.Perm.SameCycle f x y ↔ ↑f y ≠ y

theorem Equiv.Perm.IsCycle.exists_pow_eq {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] (hf : Equiv.Perm.IsCycle f) (hx : ↑f x ≠ x) (hy : ↑f y ≠ y) : ∃ i, ↑(f ^ i) x = y

theorem Equiv.Perm.isCycle_swap {α : Type u_2} {x : α} {y : α} [DecidableEq α] (hxy : x ≠ y) : Equiv.Perm.IsCycle (Equiv.swap x y)

theorem Equiv.Perm.IsSwap.isCycle {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] : Equiv.Perm.IsSwap f → Equiv.Perm.IsCycle f

theorem Equiv.Perm.IsCycle.two_le_card_support {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (h : Equiv.Perm.IsCycle f) : 2 ≤ Finset.card (Equiv.Perm.support f)

theorem Equiv.Perm.IsCycle.exists_pow_eq_one {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) : ∃ k x, f ^ k = 1

noncomputable def Equiv.Perm.IsCycle.zpowersEquivSupport {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) : { x // x ∈ Subgroup.zpowers σ } ≃ { x // x ∈ Equiv.Perm.support σ }

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

Equations

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

@[simp]

theorem Equiv.Perm.IsCycle.zpowersEquivSupport_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) {n : ℕ} : ↑(Equiv.Perm.IsCycle.zpowersEquivSupport hσ) { val := σ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) } = { val := ↑(σ ^ n) (Classical.choose hσ), property := (_ : ↑(σ ^ n) (Classical.choose hσ) ∈ Equiv.Perm.support σ) }

@[simp]

theorem Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) (n : ℕ) : ↑(Equiv.Perm.IsCycle.zpowersEquivSupport hσ).symm { val := ↑(σ ^ n) (Classical.choose hσ), property := (_ : ↑(σ ^ n) (Classical.choose hσ) ∈ Equiv.Perm.support σ) } = { val := σ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) }

theorem Equiv.Perm.IsCycle.orderOf {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) : orderOf f = Finset.card (Equiv.Perm.support f)

theorem Equiv.Perm.isCycle_swap_mul_aux₁ {α : Type u_4} [DecidableEq α] (n : ℕ) {b : α} {x : α} {f : Equiv.Perm α} : ↑(Equiv.swap x (↑f x) * f) b ≠ b → ↑(f ^ n) (↑f x) = b → ∃ i, ↑((Equiv.swap x (↑f x) * f) ^ i) (↑f x) = b

theorem Equiv.Perm.isCycle_swap_mul_aux₂ {α : Type u_4} [DecidableEq α] (n : ℤ) {b : α} {x : α} {f : Equiv.Perm α} : ↑(Equiv.swap x (↑f x) * f) b ≠ b → ↑(f ^ n) (↑f x) = b → ∃ i, ↑((Equiv.swap x (↑f x) * f) ^ i) (↑f x) = b

theorem Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self {α : Type u_4} [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) {x : α} (hfx : ↑f x ≠ x) (hffx : ↑f (↑f x) = x) : f = Equiv.swap x (↑f x)

theorem Equiv.Perm.IsCycle.swap_mul {α : Type u_4} [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) {x : α} (hx : ↑f x ≠ x) (hffx : ↑f (↑f x) ≠ x) : Equiv.Perm.IsCycle (Equiv.swap x (↑f x) * f)

theorem Equiv.Perm.IsCycle.sign {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : ↑Equiv.Perm.sign f = -(-1) ^ Finset.card (Equiv.Perm.support f)

theorem Equiv.Perm.IsCycle.of_pow {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] {n : ℕ} (h1 : Equiv.Perm.IsCycle (f ^ n)) (h2 : Equiv.Perm.support f ⊆ Equiv.Perm.support (f ^ n)) : Equiv.Perm.IsCycle f

theorem Equiv.Perm.IsCycle.of_zpow {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] {n : ℤ} (h1 : Equiv.Perm.IsCycle (f ^ n)) (h2 : Equiv.Perm.support f ⊆ Equiv.Perm.support (f ^ n)) : Equiv.Perm.IsCycle f

theorem Equiv.Perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : List (Equiv.Perm β)} (h1 : ∀ (f : Equiv.Perm β), f ∈ l → Equiv.Perm.IsCycle f) (h2 : List.Pairwise Equiv.Perm.Disjoint l) : List.Nodup l

theorem Equiv.Perm.IsCycle.support_congr {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) (hg : Equiv.Perm.IsCycle g) (h : Equiv.Perm.support f ⊆ Equiv.Perm.support g) (h' : ∀ (x : α), x ∈ Equiv.Perm.support f → ↑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.

theorem Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) (hg : Equiv.Perm.IsCycle g) (h : ∀ (x : α), x ∈ Equiv.Perm.support f ∩ Equiv.Perm.support g → ↑f x = ↑g x) (hx : ↑f x = ↑g x) (hx' : x ∈ Equiv.Perm.support f) : 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.

theorem Equiv.Perm.IsCycle.support_pow_eq_iff {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) {n : ℕ} : Equiv.Perm.support (f ^ n) = Equiv.Perm.support f ↔ ¬orderOf f ∣ n

theorem Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) {n : ℕ} (npos : 0 < n) (hn : n < orderOf f) : Equiv.Perm.support (f ^ n) = Equiv.Perm.support f

theorem Equiv.Perm.IsCycle.pow_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : ℕ} : Equiv.Perm.IsCycle (f ^ n) ↔ Nat.Coprime n (orderOf f)

theorem Equiv.Perm.IsCycle.pow_eq_one_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : ℕ} : f ^ n = 1 ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ n) x = x

theorem Equiv.Perm.IsCycle.pow_eq_one_iff' {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : ℕ} {x : β} (hx : ↑f x ≠ x) : f ^ n = 1 ↔ ↑(f ^ n) x = x

theorem Equiv.Perm.IsCycle.pow_eq_one_iff'' {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : ℕ} : f ^ n = 1 ↔ ∀ (x : β), ↑f x ≠ x → ↑(f ^ n) x = x

theorem Equiv.Perm.IsCycle.pow_eq_pow_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {a : ℕ} {b : ℕ} : f ^ a = f ^ b ↔ ∃ x, ↑f x ≠ x ∧ ↑(f ^ a) x = ↑(f ^ b) x

theorem Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) (hf' : Nat.Prime (orderOf f)) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) : Equiv.Perm.IsCycle (f ^ n)

IsCycleOn

def Equiv.Perm.IsCycleOn {α : 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

• Equiv.Perm.IsCycleOn f s = (Set.BijOn (↑f) s s ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Equiv.Perm.SameCycle f x y)

@[simp]

theorem Equiv.Perm.isCycleOn_empty {α : Type u_2} {f : Equiv.Perm α} : Equiv.Perm.IsCycleOn f ∅

@[simp]

theorem Equiv.Perm.isCycleOn_one {α : Type u_2} {s : Set α} : Equiv.Perm.IsCycleOn 1 s ↔ Set.Subsingleton s

theorem Set.Subsingleton.isCycleOn_one {α : Type u_2} {s : Set α} : Set.Subsingleton s → Equiv.Perm.IsCycleOn 1 s

Alias of the reverse direction of Equiv.Perm.isCycleOn_one.

theorem Equiv.Perm.IsCycleOn.subsingleton {α : Type u_2} {s : Set α} : Equiv.Perm.IsCycleOn 1 s → Set.Subsingleton s

Alias of the forward direction of Equiv.Perm.isCycleOn_one.

@[simp]

theorem Equiv.Perm.isCycleOn_singleton {α : Type u_2} {f : Equiv.Perm α} {a : α} : Equiv.Perm.IsCycleOn f {a} ↔ ↑f a = a

theorem Equiv.Perm.isCycleOn_of_subsingleton {α : Type u_2} [Subsingleton α] (f : Equiv.Perm α) (s : Set α) : Equiv.Perm.IsCycleOn f s

@[simp]

theorem Equiv.Perm.isCycleOn_inv {α : Type u_2} {f : Equiv.Perm α} {s : Set α} : Equiv.Perm.IsCycleOn f⁻¹ s ↔ Equiv.Perm.IsCycleOn f s

theorem Equiv.Perm.IsCycleOn.inv {α : Type u_2} {f : Equiv.Perm α} {s : Set α} : Equiv.Perm.IsCycleOn f s → Equiv.Perm.IsCycleOn f⁻¹ s

Alias of the reverse direction of Equiv.Perm.isCycleOn_inv.

theorem Equiv.Perm.IsCycleOn.of_inv {α : Type u_2} {f : Equiv.Perm α} {s : Set α} : Equiv.Perm.IsCycleOn f⁻¹ s → Equiv.Perm.IsCycleOn f s

Alias of the forward direction of Equiv.Perm.isCycleOn_inv.

theorem Equiv.Perm.IsCycleOn.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {s : Set α} (h : Equiv.Perm.IsCycleOn f s) : Equiv.Perm.IsCycleOn (g * f * g⁻¹) (↑g '' s)

theorem Equiv.Perm.isCycleOn_swap {α : Type u_2} {a : α} {b : α} [DecidableEq α] (hab : a ≠ b) : Equiv.Perm.IsCycleOn (Equiv.swap a b) {a, b}

theorem Equiv.Perm.IsCycleOn.apply_ne {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (hf : Equiv.Perm.IsCycleOn f s) (hs : Set.Nontrivial s) (ha : a ∈ s) : ↑f a ≠ a

theorem Equiv.Perm.IsCycle.isCycleOn {α : Type u_2} {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : Equiv.Perm.IsCycleOn f {x | ↑f x ≠ x}

theorem Equiv.Perm.isCycle_iff_exists_isCycleOn {α : Type u_2} {f : Equiv.Perm α} : Equiv.Perm.IsCycle f ↔ ∃ s, Set.Nontrivial s ∧ Equiv.Perm.IsCycleOn f s ∧ ∀ ⦃x : α⦄, ¬Function.IsFixedPt (↑f) x → x ∈ s

This lemma demonstrates the relation between Equiv.Perm.IsCycle and Equiv.Perm.IsCycleOn in non-degenerate cases.

theorem Equiv.Perm.IsCycleOn.apply_mem_iff {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {x : α} (hf : Equiv.Perm.IsCycleOn f s) : ↑f x ∈ s ↔ x ∈ s

theorem Equiv.Perm.IsCycleOn.isCycle_subtypePerm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : Equiv.Perm.IsCycleOn f s) (hs : Set.Nontrivial s) : Equiv.Perm.IsCycle (Equiv.Perm.subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s))

Note that the identity satisfies IsCycleOn for any subsingleton set, but not IsCycle.

theorem Equiv.Perm.IsCycleOn.subtypePerm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : Equiv.Perm.IsCycleOn f s) : Equiv.Perm.IsCycleOn (Equiv.Perm.subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) Set.univ

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

theorem Equiv.Perm.IsCycleOn.pow_apply_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) (ha : a ∈ s) {n : ℕ} : ↑(f ^ n) a = a ↔ Finset.card s ∣ n

theorem Equiv.Perm.IsCycleOn.zpow_apply_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) (ha : a ∈ s) {n : ℤ} : ↑(f ^ n) a = a ↔ ↑(Finset.card s) ∣ n

theorem Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) (ha : a ∈ s) {m : ℕ} {n : ℕ} : ↑(f ^ m) a = ↑(f ^ n) a ↔ m ≡ n [MOD Finset.card s]

theorem Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) (ha : a ∈ s) {m : ℤ} {n : ℤ} : ↑(f ^ m) a = ↑(f ^ n) a ↔ m ≡ n [ZMOD ↑(Finset.card s)]

theorem Equiv.Perm.IsCycleOn.pow_card_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) (ha : a ∈ s) : ↑(f ^ Finset.card s) a = a

theorem Equiv.Perm.IsCycleOn.exists_pow_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {b : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) (ha : a ∈ s) (hb : b ∈ s) : ∃ n, n < Finset.card s ∧ ↑(f ^ n) a = b

theorem Equiv.Perm.IsCycleOn.exists_pow_eq' {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} {b : α} (hs : Set.Finite s) (hf : Equiv.Perm.IsCycleOn f s) (ha : a ∈ s) (hb : b ∈ s) : ∃ n, ↑(f ^ n) a = b

theorem Equiv.Perm.IsCycleOn.range_pow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (hs : Set.Finite s) (h : Equiv.Perm.IsCycleOn f s) (ha : a ∈ s) : (Set.range fun n => ↑(f ^ n) a) = s

theorem Equiv.Perm.IsCycleOn.range_zpow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (h : Equiv.Perm.IsCycleOn f s) (ha : a ∈ s) : (Set.range fun n => ↑(f ^ n) a) = s

theorem Equiv.Perm.IsCycleOn.of_pow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : ℕ} (hf : Equiv.Perm.IsCycleOn (f ^ n) s) (h : Set.BijOn (↑f) s s) : Equiv.Perm.IsCycleOn f s

theorem Equiv.Perm.IsCycleOn.of_zpow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : ℤ} (hf : Equiv.Perm.IsCycleOn (f ^ n) s) (h : Set.BijOn (↑f) s s) : Equiv.Perm.IsCycleOn f s

theorem Equiv.Perm.IsCycleOn.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {s : Set α} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (h : Equiv.Perm.IsCycleOn g s) : Equiv.Perm.IsCycleOn (Equiv.Perm.extendDomain g f) (Subtype.val ∘ ↑f '' s)

theorem Equiv.Perm.IsCycleOn.countable {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hs : Equiv.Perm.IsCycleOn f s) : Set.Countable s

cycleOf

def Equiv.Perm.cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm α

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

Equations

• Equiv.Perm.cycleOf f x = ↑Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm f (_ : ∀ (x : α), Equiv.Perm.SameCycle f x x ↔ Equiv.Perm.SameCycle f x (↑f x)))

theorem Equiv.Perm.cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (y : α) : ↑(Equiv.Perm.cycleOf f x) y = if Equiv.Perm.SameCycle f x y then ↑f y else y

theorem Equiv.Perm.cycleOf_inv {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : (Equiv.Perm.cycleOf f x)⁻¹ = Equiv.Perm.cycleOf f⁻¹ x

@[simp]

theorem Equiv.Perm.cycleOf_pow_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (n : ℕ) : ↑(Equiv.Perm.cycleOf f x ^ n) x = ↑(f ^ n) x

@[simp]

theorem Equiv.Perm.cycleOf_zpow_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (n : ℤ) : ↑(Equiv.Perm.cycleOf f x ^ n) x = ↑(f ^ n) x

theorem Equiv.Perm.SameCycle.cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → ↑(Equiv.Perm.cycleOf f x) y = ↑f y

theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} : ¬Equiv.Perm.SameCycle f x y → ↑(Equiv.Perm.cycleOf f x) y = y

theorem Equiv.Perm.SameCycle.cycleOf_eq {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) : Equiv.Perm.cycleOf f x = Equiv.Perm.cycleOf f y

@[simp]

theorem Equiv.Perm.cycleOf_apply_apply_zpow_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (k : ℤ) : ↑(Equiv.Perm.cycleOf f x) (↑(f ^ k) x) = ↑(f ^ (k + 1)) x

@[simp]

theorem Equiv.Perm.cycleOf_apply_apply_pow_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (k : ℕ) : ↑(Equiv.Perm.cycleOf f x) (↑(f ^ k) x) = ↑(f ^ (k + 1)) x

@[simp]

theorem Equiv.Perm.cycleOf_apply_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : ↑(Equiv.Perm.cycleOf f x) (↑f x) = ↑f (↑f x)

@[simp]

theorem Equiv.Perm.cycleOf_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : ↑(Equiv.Perm.cycleOf f x) x = ↑f x

theorem Equiv.Perm.IsCycle.cycleOf_eq {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hf : Equiv.Perm.IsCycle f) (hx : ↑f x ≠ x) : Equiv.Perm.cycleOf f x = f

@[simp]

theorem Equiv.Perm.cycleOf_eq_one_iff {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) : Equiv.Perm.cycleOf f x = 1 ↔ ↑f x = x

@[simp]

theorem Equiv.Perm.cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm.cycleOf f (↑f x) = Equiv.Perm.cycleOf f x

@[simp]

theorem Equiv.Perm.cycleOf_self_apply_pow {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α) : Equiv.Perm.cycleOf f (↑(f ^ n) x) = Equiv.Perm.cycleOf f x

@[simp]

theorem Equiv.Perm.cycleOf_self_apply_zpow {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℤ) (x : α) : Equiv.Perm.cycleOf f (↑(f ^ n) x) = Equiv.Perm.cycleOf f x

theorem Equiv.Perm.IsCycle.cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hf : Equiv.Perm.IsCycle f) : Equiv.Perm.cycleOf f x = if ↑f x = x then 1 else f

theorem Equiv.Perm.cycleOf_one {α : Type u_2} [DecidableEq α] [Fintype α] (x : α) : Equiv.Perm.cycleOf 1 x = 1

theorem Equiv.Perm.isCycle_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) (hx : ↑f x ≠ x) : Equiv.Perm.IsCycle (Equiv.Perm.cycleOf f x)

@[simp]

theorem Equiv.Perm.two_le_card_support_cycleOf_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : 2 ≤ Finset.card (Equiv.Perm.support (Equiv.Perm.cycleOf f x)) ↔ ↑f x ≠ x

@[simp]

theorem Equiv.Perm.card_support_cycleOf_pos_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : 0 < Finset.card (Equiv.Perm.support (Equiv.Perm.cycleOf f x)) ↔ ↑f x ≠ x

theorem Equiv.Perm.pow_apply_eq_pow_mod_orderOf_cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α) : ↑(f ^ n) x = ↑(f ^ (n % orderOf (Equiv.Perm.cycleOf f x))) x

theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Commute f g) (x : α) (hx : ↑g x = x) : Equiv.Perm.cycleOf (f * g) x = Equiv.Perm.cycleOf f x

theorem Equiv.Perm.Disjoint.cycleOf_mul_distrib {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) (x : α) : Equiv.Perm.cycleOf (f * g) x = Equiv.Perm.cycleOf f x * Equiv.Perm.cycleOf g x

theorem Equiv.Perm.support_cycleOf_eq_nil_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : Equiv.Perm.support (Equiv.Perm.cycleOf f x) = ∅ ↔ ¬x ∈ Equiv.Perm.support f

theorem Equiv.Perm.support_cycleOf_le {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm.support (Equiv.Perm.cycleOf f x) ≤ Equiv.Perm.support f

theorem Equiv.Perm.mem_support_cycleOf_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} : y ∈ Equiv.Perm.support (Equiv.Perm.cycleOf f x) ↔ Equiv.Perm.SameCycle f x y ∧ x ∈ Equiv.Perm.support f

theorem Equiv.Perm.mem_support_cycleOf_iff' {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (hx : ↑f x ≠ x) : y ∈ Equiv.Perm.support (Equiv.Perm.cycleOf f x) ↔ Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.SameCycle.mem_support_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) : x ∈ Equiv.Perm.support f ↔ y ∈ Equiv.Perm.support f

theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α) : ↑(f ^ (n % Finset.card (Equiv.Perm.support (Equiv.Perm.cycleOf f x)))) x = ↑(f ^ n) x

theorem Equiv.Perm.isCycle_cycleOf_iff {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) : Equiv.Perm.IsCycle (Equiv.Perm.cycleOf f x) ↔ ↑f x ≠ x

x is in the support of f iff Equiv.Perm.cycle_of f x is a cycle.

theorem Equiv.Perm.isCycleOn_support_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm.IsCycleOn f ↑(Equiv.Perm.support (Equiv.Perm.cycleOf f x))

theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hx : x ∈ Equiv.Perm.support f) : ∃ i x, ↑(f ^ i) x = y

theorem Equiv.Perm.SameCycle.exists_pow_eq {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} {y : α} (f : Equiv.Perm α) (h : Equiv.Perm.SameCycle f x y) : ∃ i x x, ↑(f ^ i) x = y

cycleFactors

def Equiv.Perm.cycleFactorsAux {α : Type u_2} [DecidableEq α] [Fintype α] (l : List α) (f : Equiv.Perm α) : (∀ {x : α}, ↑f x ≠ x → x ∈ l) → { l // List.prod l = f ∧ (∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsCycle g) ∧ 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

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

theorem Equiv.Perm.mem_list_cycles_iff {α : Type u_4} [Finite α] {l : List (Equiv.Perm α)} (h1 : ∀ (σ : Equiv.Perm α), σ ∈ l → Equiv.Perm.IsCycle σ) (h2 : List.Pairwise Equiv.Perm.Disjoint l) {σ : Equiv.Perm α} : σ ∈ l ↔ Equiv.Perm.IsCycle σ ∧ ∀ (a : α), ↑σ a ≠ a → ↑σ a = ↑(List.prod l) a

theorem Equiv.Perm.list_cycles_perm_list_cycles {α : Type u_4} [Finite α] {l₁ : List (Equiv.Perm α)} {l₂ : List (Equiv.Perm α)} (h₀ : List.prod l₁ = List.prod l₂) (h₁l₁ : ∀ (σ : Equiv.Perm α), σ ∈ l₁ → Equiv.Perm.IsCycle σ) (h₁l₂ : ∀ (σ : Equiv.Perm α), σ ∈ l₂ → Equiv.Perm.IsCycle σ) (h₂l₁ : List.Pairwise Equiv.Perm.Disjoint l₁) (h₂l₂ : List.Pairwise Equiv.Perm.Disjoint l₂) : l₁ ~ l₂

def Equiv.Perm.cycleFactors {α : Type u_2} [DecidableEq α] [Fintype α] [LinearOrder α] (f : Equiv.Perm α) : { l // List.prod l = f ∧ (∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsCycle g) ∧ List.Pairwise Equiv.Perm.Disjoint l }

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

Equations

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

def Equiv.Perm.truncCycleFactors {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Trunc { l // List.prod l = f ∧ (∀ (g : Equiv.Perm α), g ∈ l → Equiv.Perm.IsCycle g) ∧ 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

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

def Equiv.Perm.cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Finset (Equiv.Perm α)

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

Equations

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

theorem Equiv.Perm.cycleFactorsFinset_eq_list_toFinset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {l : List (Equiv.Perm α)} (hn : List.Nodup l) : Equiv.Perm.cycleFactorsFinset σ = List.toFinset l ↔ (∀ (f : Equiv.Perm α), f ∈ l → Equiv.Perm.IsCycle f) ∧ List.Pairwise Equiv.Perm.Disjoint l ∧ List.prod l = σ

theorem Equiv.Perm.cycleFactorsFinset_eq_finset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {s : Finset (Equiv.Perm α)} : Equiv.Perm.cycleFactorsFinset σ = s ↔ (∀ (f : Equiv.Perm α), f ∈ s → Equiv.Perm.IsCycle f) ∧ ∃ h, Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ

theorem Equiv.Perm.cycleFactorsFinset_pairwise_disjoint {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Equiv.Perm.Disjoint

theorem Equiv.Perm.cycleFactorsFinset_mem_commute {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Commute

theorem Equiv.Perm.cycleFactorsFinset_noncommProd {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (comm : optParam (Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Commute) (_ : Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Commute)) : Finset.noncommProd (Equiv.Perm.cycleFactorsFinset f) id comm = f

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

theorem Equiv.Perm.mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {p : Equiv.Perm α} : p ∈ Equiv.Perm.cycleFactorsFinset f ↔ Equiv.Perm.IsCycle p ∧ ∀ (a : α), a ∈ Equiv.Perm.support p → ↑p a = ↑f a

theorem Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : Equiv.Perm.cycleOf f x ∈ Equiv.Perm.cycleFactorsFinset f ↔ x ∈ Equiv.Perm.support f

theorem Equiv.Perm.mem_cycleFactorsFinset_support_le {α : Type u_2} [DecidableEq α] [Fintype α] {p : Equiv.Perm α} {f : Equiv.Perm α} (h : p ∈ Equiv.Perm.cycleFactorsFinset f) : Equiv.Perm.support p ≤ Equiv.Perm.support f

theorem Equiv.Perm.cycleFactorsFinset_eq_empty_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} : Equiv.Perm.cycleFactorsFinset f = ∅ ↔ f = 1

@[simp]

theorem Equiv.Perm.cycleFactorsFinset_one {α : Type u_2} [DecidableEq α] [Fintype α] : Equiv.Perm.cycleFactorsFinset 1 = ∅

@[simp]

theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} : Equiv.Perm.cycleFactorsFinset f = {f} ↔ Equiv.Perm.IsCycle f

theorem Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : Equiv.Perm.cycleFactorsFinset f = {f}

theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} : Equiv.Perm.cycleFactorsFinset f = {g} ↔ Equiv.Perm.IsCycle f ∧ f = g

theorem Equiv.Perm.cycleFactorsFinset_injective {α : Type u_2} [DecidableEq α] [Fintype α] : Function.Injective Equiv.Perm.cycleFactorsFinset

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

theorem Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) : Disjoint (Equiv.Perm.cycleFactorsFinset f) (Equiv.Perm.cycleFactorsFinset g)

theorem Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) : Equiv.Perm.cycleFactorsFinset (f * g) = Equiv.Perm.cycleFactorsFinset f ∪ Equiv.Perm.cycleFactorsFinset g

theorem Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f ∈ Equiv.Perm.cycleFactorsFinset g) : Equiv.Perm.Disjoint (g * f⁻¹) f

theorem Equiv.Perm.cycle_is_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {c : Equiv.Perm α} {a : α} (ha : a ∈ Equiv.Perm.support c) (hc : c ∈ Equiv.Perm.cycleFactorsFinset f) : c = Equiv.Perm.cycleOf f a

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

theorem Equiv.Perm.cycle_induction_on {β : Type u_3} [Finite β] (P : Equiv.Perm β → Prop) (σ : Equiv.Perm β) (base_one : P 1) (base_cycles : (σ : Equiv.Perm β) → Equiv.Perm.IsCycle σ → P σ) (induction_disjoint : (σ τ : Equiv.Perm β) → Equiv.Perm.Disjoint σ τ → Equiv.Perm.IsCycle σ → P σ → P τ → P (σ * τ)) : P σ

theorem Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f ∈ Equiv.Perm.cycleFactorsFinset g) : Equiv.Perm.cycleFactorsFinset (g * f⁻¹) = Equiv.Perm.cycleFactorsFinset g \ {f}

theorem Equiv.Perm.closure_isCycle {β : Type u_3} [Finite β] : Subgroup.closure {σ | Equiv.Perm.IsCycle σ} = ⊤

theorem Equiv.Perm.closure_cycle_adjacent_swap {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = ⊤) (x : α) : Subgroup.closure {σ, Equiv.swap x (↑σ x)} = ⊤

theorem Equiv.Perm.closure_cycle_coprime_swap {α : Type u_2} [DecidableEq α] [Fintype α] {n : ℕ} {σ : Equiv.Perm α} (h0 : Nat.Coprime n (Fintype.card α)) (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = Finset.univ) (x : α) : Subgroup.closure {σ, Equiv.swap x (↑(σ ^ n) x)} = ⊤

theorem Equiv.Perm.closure_prime_cycle_swap {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h0 : Nat.Prime (Fintype.card α)) (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = Finset.univ) (h3 : Equiv.Perm.IsSwap τ) : Subgroup.closure {σ, τ} = ⊤

theorem Equiv.Perm.isConj_of_support_equiv {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (f : { x // x ∈ ↑(Equiv.Perm.support σ) } ≃ { x // x ∈ ↑(Equiv.Perm.support τ) }) (hf : ∀ (x : α) (hx : x ∈ ↑(Equiv.Perm.support σ)), ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ Equiv.Perm.support σ) }) = ↑τ ↑(↑f { val := x, property := hx })) : IsConj σ τ

theorem Equiv.Perm.IsCycle.isConj {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) (hτ : Equiv.Perm.IsCycle τ) (h : Finset.card (Equiv.Perm.support σ) = Finset.card (Equiv.Perm.support τ)) : IsConj σ τ

theorem Equiv.Perm.IsCycle.isConj_iff {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) (hτ : Equiv.Perm.IsCycle τ) : IsConj σ τ ↔ Finset.card (Equiv.Perm.support σ) = Finset.card (Equiv.Perm.support τ)

@[simp]

theorem Equiv.Perm.support_conj {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} : Equiv.Perm.support (σ * τ * σ⁻¹) = Finset.map (Equiv.toEmbedding σ) (Equiv.Perm.support τ)

theorem Equiv.Perm.card_support_conj {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} : Finset.card (Equiv.Perm.support (σ * τ * σ⁻¹)) = Finset.card (Equiv.Perm.support τ)

theorem Equiv.Perm.Disjoint.isConj_mul {α : Type u_4} [Finite α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} {π : Equiv.Perm α} {ρ : Equiv.Perm α} (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : Equiv.Perm.Disjoint σ τ) (hd2 : Equiv.Perm.Disjoint π ρ) : IsConj (σ * τ) (π * ρ)

Fixed points

theorem Equiv.Perm.fixed_point_card_lt_of_ne_one {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (h : σ ≠ 1) : Finset.card (Finset.filter (fun x => ↑σ x = x) Finset.univ) < Fintype.card α - 1

theorem List.Nodup.isCycleOn_formPerm {α : Type u_2} [DecidableEq α] {l : List α} (h : List.Nodup l) : Equiv.Perm.IsCycleOn (List.formPerm l) {a | a ∈ l}

theorem Int.addLeft_one_isCycle : Equiv.Perm.IsCycle (Equiv.addLeft 1)

theorem Int.addRight_one_isCycle : Equiv.Perm.IsCycle (Equiv.addRight 1)

theorem Finset.exists_cycleOn {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) : ∃ f, Equiv.Perm.IsCycleOn f ↑s ∧ Equiv.Perm.support f ⊆ s

theorem Set.Countable.exists_cycleOn {α : Type u_2} [DecidableEq α] {s : Set α} (hs : Set.Countable s) : ∃ f, Equiv.Perm.IsCycleOn f s ∧ {x | ↑f x ≠ x} ⊆ s

theorem Set.prod_self_eq_iUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : Equiv.Perm.IsCycleOn f s) : s ×ˢ s = ⋃ (n : ℤ), (fun a => (a, ↑(f ^ n) a)) '' s

theorem Finset.product_self_eq_disj_Union_perm_aux {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) : Set.PairwiseDisjoint ↑(Finset.range (Finset.card s)) fun k => Finset.map { toFun := fun i => (i, ↑(f ^ k) i), inj' := (_ : ∀ (i j : α), (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j → ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) } s

theorem Finset.product_self_eq_disjUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) : s ×ˢ s = Finset.disjiUnion (Finset.range (Finset.card s)) (fun k => Finset.map { toFun := fun i => (i, ↑(f ^ k) i), inj' := (_ : ∀ (i j : α), (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j → ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) } s) (_ : Set.PairwiseDisjoint ↑(Finset.range (Finset.card s)) fun k => Finset.map { toFun := fun i => (i, ↑(f ^ k) i), inj' := (_ : ∀ (i j : α), (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j → ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) } 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.

theorem Finset.sum_smul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [AddCommMonoid β] [Module α β] {s : Finset ι} {σ : Equiv.Perm ι} (hσ : Equiv.Perm.IsCycleOn σ ↑s) (f : ι → α) (g : ι → β) : ((Finset.sum s fun i => f i) • Finset.sum s fun i => g i) = Finset.sum (Finset.range (Finset.card s)) fun k => Finset.sum s fun i => f i • g (↑(σ ^ k) i)

theorem Finset.sum_mul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} [Semiring α] {s : Finset ι} {σ : Equiv.Perm ι} (hσ : Equiv.Perm.IsCycleOn σ ↑s) (f : ι → α) (g : ι → α) : ((Finset.sum s fun i => f i) * Finset.sum s fun i => g i) = Finset.sum (Finset.range (Finset.card s)) fun k => Finset.sum s fun i => f i * g (↑(σ ^ k) i)