Cycles of a permutation

This file starts 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.

Notes

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

• IsCycle is about the entire type while IsCycleOn is restricted to a set.
• IsCycle forbids the identity while IsCycleOn allows it (if s is a subsingleton).
• IsCycleOn forbids fixed points on s (if s is nontrivial), while IsCycle 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 := ⋯ }

@[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 < 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 : ℕ), 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y

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

Equations

• Equiv.Perm.instDecidableRelSameCycle f x y = decidable_of_iff (∃ n ∈ List.range (Fintype.card (Equiv.Perm α)), (f ^ n) x = y) ⋯

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 ≤ (Equiv.Perm.support f).card

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

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

Equations

• Equiv.Perm.IsCycle.zpowersEquivSupport hσ = Equiv.ofBijective (fun (τ : ↑↑(Subgroup.zpowers σ)) => { val := ↑τ (Classical.choose hσ), property := ⋯ }) ⋯

@[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 := ⋯ } = { val := (σ ^ n) (Classical.choose hσ), property := ⋯ }

@[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 := ⋯ } = { val := σ ^ n, property := ⋯ }

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

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) ^ (Equiv.Perm.support f).card

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 ∈ 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 ∈ 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 ∈ 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)

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

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

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

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

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.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.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.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 α), 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 ⋯)

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 ⋯) 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 ↔ s.card ∣ 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 ↔ ↑s.card ∣ 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 s.card]

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 ↑s.card]

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 ^ s.card) 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 < s.card, (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

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 Finset.exists_cycleOn {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) : ∃ (f : Equiv.Perm α), Equiv.Perm.IsCycleOn f ↑s ∧ Equiv.Perm.support f ⊆ s

theorem Set.Countable.exists_cycleOn {α : Type u_2} {s : Set α} (hs : Set.Countable s) : ∃ (f : Equiv.Perm α), 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_disjiUnion_perm_aux {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) : Set.PairwiseDisjoint ↑(Finset.range s.card) fun (k : ℕ) => Finset.map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := ⋯ } s

theorem Finset.product_self_eq_disjiUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f ↑s) : s ×ˢ s = Finset.disjiUnion (Finset.range s.card) (fun (k : ℕ) => Finset.map { toFun := 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.

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 s.card) 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 s.card) fun (k : ℕ) => Finset.sum s fun (i : ι) => f i * g ((σ ^ k) i)