Mathlib.GroupTheory.Perm.Cycle.Basic

Equiv.Perm.SameCycle definition

(f : Perm α) (x y : α) : Prop

Full source

/-- The equivalence relation indicating that two points are in the same cycle of a permutation. -/
def SameCycle (f : Perm α) (x y : α) : Prop :=
  ∃ i : ℤ, (f ^ i) x = y

Same cycle relation for permutations

Informal description

For a permutation $ f $ of a type $ \alpha $, the relation $ \text{SameCycle } f $ on $ \alpha $ is defined such that two elements $ x $ and $ y $ are related if there exists an integer $ i $ such that $ f^i(x) = y $. This relation captures when two elements are in the same cycle of the permutation $ f $.

Equiv.Perm.SameCycle.refl theorem

(f : Perm α) (x : α) : SameCycle f x x

Full source

@[refl]
theorem SameCycle.refl (f : Perm α) (x : α) : SameCycle f x x :=
  ⟨0, rfl⟩

Reflexivity of SameCycle Relation for Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any element $x \in \alpha$, the relation $\text{SameCycle } f$ is reflexive, i.e., $x$ is in the same cycle as itself under $f$.

Equiv.Perm.SameCycle.rfl theorem

: SameCycle f x x

Full source

theorem SameCycle.rfl : SameCycle f x x :=
  SameCycle.refl _ _

Reflexivity of Same Cycle Relation in Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any element $x \in \alpha$, the relation $\text{SameCycle } f$ is reflexive, i.e., $x$ is in the same cycle as itself under $f$.

Eq.sameCycle theorem

(h : x = y) (f : Perm α) : f.SameCycle x y

Full source

protected theorem _root_.Eq.sameCycle (h : x = y) (f : Perm α) : f.SameCycle x y := by rw [h]

Equality Implies Same Cycle in Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any elements $x, y \in \alpha$, if $x = y$, then $x$ and $y$ are in the same cycle of $f$.

Equiv.Perm.SameCycle.symm theorem

: SameCycle f x y → SameCycle f y x

Full source

@[symm]
theorem SameCycle.symm : SameCycle f x y → SameCycle f y x := fun ⟨i, hi⟩ =>
  ⟨-i, by rw [zpow_neg, ← hi, inv_apply_self]⟩

Symmetry of Same Cycle Relation in Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any elements $x, y \in \alpha$, if $x$ and $y$ are in the same cycle of $f$ (i.e., there exists an integer $i$ such that $f^i(x) = y$), then $y$ and $x$ are also in the same cycle of $f$ (i.e., there exists an integer $j$ such that $f^j(y) = x$).

Equiv.Perm.sameCycle_comm theorem

: SameCycle f x y ↔ SameCycle f y x

Full source

theorem sameCycle_comm : SameCycleSameCycle f x y ↔ SameCycle f y x :=
  ⟨SameCycle.symm, SameCycle.symm⟩

Symmetry of the Same Cycle Relation for Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any elements $x, y \in \alpha$, the elements $x$ and $y$ are in the same cycle of $f$ if and only if $y$ and $x$ are in the same cycle of $f$. In other words, the relation $\text{SameCycle } f$ is symmetric.

Equiv.Perm.SameCycle.trans theorem

: SameCycle f x y → SameCycle f y z → SameCycle f x z

Full source

@[trans]
theorem SameCycle.trans : SameCycle f x y → SameCycle f y z → SameCycle f x z :=
  fun ⟨i, hi⟩ ⟨j, hj⟩ => ⟨j + i, by rw [zpow_add, mul_apply, hi, hj]⟩

Transitivity of Same Cycle Relation in Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any elements $x, y, z \in \alpha$, if $x$ and $y$ are in the same cycle of $f$ and $y$ and $z$ are in the same cycle of $f$, then $x$ and $z$ are also in the same cycle of $f$. In other words, the relation $\text{SameCycle } f$ is transitive.

Equiv.Perm.SameCycle.equivalence theorem

: Equivalence (SameCycle f)

Full source

theorem SameCycle.equivalence : Equivalence (SameCycle f) :=
  ⟨SameCycle.refl f, SameCycle.symm, SameCycle.trans⟩

Equivalence Relation Properties of SameCycle for Permutations

Informal description

For any permutation $f$ of a type $\alpha$, the relation $\text{SameCycle } f$ is an equivalence relation on $\alpha$. That is: 1. (Reflexivity) For every $x \in \alpha$, $x$ is in the same cycle as itself. 2. (Symmetry) For any $x, y \in \alpha$, if $x$ is in the same cycle as $y$, then $y$ is in the same cycle as $x$. 3. (Transitivity) For any $x, y, z \in \alpha$, if $x$ is in the same cycle as $y$ and $y$ is in the same cycle as $z$, then $x$ is in the same cycle as $z$.

Equiv.Perm.SameCycle.setoid definition

(f : Perm α) : Setoid α

Full source

/-- The setoid defined by the `SameCycle` relation. -/
def SameCycle.setoid (f : Perm α) : Setoid α where
  r := f.SameCycle
  iseqv := SameCycle.equivalence f

Equivalence relation of being in the same cycle under a permutation

Informal description

For a permutation $ f $ of a type $ \alpha $, the setoid (equivalence relation) defined by the relation $ \text{SameCycle } f $, where two elements $ x $ and $ y $ are equivalent if they are in the same cycle of $ f $. This means there exists an integer $ i $ such that $ f^i(x) = y $. The relation is reflexive, symmetric, and transitive, making it an equivalence relation on $ \alpha $.

Equiv.Perm.sameCycle_one theorem

: SameCycle 1 x y ↔ x = y

Full source

@[simp]
theorem sameCycle_one : SameCycleSameCycle 1 x y ↔ x = y := by simp [SameCycle]

Identity Permutation Has Singleton Cycles: $\text{SameCycle } 1\, x\, y \leftrightarrow x = y$

Informal description

For any elements $x$ and $y$ in the domain of a permutation, $x$ and $y$ are in the same cycle of the identity permutation if and only if $x = y$.

Equiv.Perm.sameCycle_inv theorem

: SameCycle f⁻¹ x y ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_inv : SameCycleSameCycle f⁻¹ x y ↔ SameCycle f x y :=
  (Equiv.neg _).exists_congr_left.trans <| by simp [SameCycle]

Inverse Permutation Preserves Cycle Membership: $\text{SameCycle}(f^{-1}, x, y) \leftrightarrow \text{SameCycle}(f, x, y)$

Informal description

For any permutation $f$ of a type $\alpha$ and any elements $x, y \in \alpha$, the elements $x$ and $y$ are in the same cycle of the inverse permutation $f^{-1}$ if and only if they are in the same cycle of $f$.

Equiv.Perm.sameCycle_conj theorem

: SameCycle (g * f * g⁻¹) x y ↔ SameCycle f (g⁻¹ x) (g⁻¹ y)

Full source

@[simp]
theorem sameCycle_conj : SameCycleSameCycle (g * f * g⁻¹) x y ↔ SameCycle f (g⁻¹ x) (g⁻¹ y) :=
  exists_congr fun i => by simp [conj_zpow, eq_inv_iff_eq]

Conjugation Preserves Cycle Structure: $\text{SameCycle}(gfg^{-1}, x, y) \leftrightarrow \text{SameCycle}(f, g^{-1}x, g^{-1}y)$

Informal description

For any permutation $f$ and elements $x, y$ in its domain, $x$ and $y$ are in the same cycle of the conjugate permutation $gfg^{-1}$ if and only if $g^{-1}x$ and $g^{-1}y$ are in the same cycle of $f$.

Equiv.Perm.SameCycle.conj theorem

: SameCycle f x y → SameCycle (g * f * g⁻¹) (g x) (g y)

Full source

theorem SameCycle.conj : SameCycle f x y → SameCycle (g * f * g⁻¹) (g x) (g y) := by
  simp [sameCycle_conj]

Conjugation Preserves Cycle Membership: $x \sim_f y \Rightarrow g(x) \sim_{gfg^{-1}} g(y)$

Informal description

For any permutations $f$ and $g$ on a type $\alpha$, and any elements $x, y \in \alpha$, if $x$ and $y$ are in the same cycle of $f$, then $g(x)$ and $g(y)$ are in the same cycle of the conjugate permutation $gfg^{-1}$.

Equiv.Perm.SameCycle.apply_eq_self_iff theorem

: SameCycle f x y → (f x = x ↔ f y = y)

Full source

theorem SameCycle.apply_eq_self_iff : SameCycle f x y → (f x = x ↔ f y = y) := fun ⟨i, hi⟩ => by
  rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]

Fixed Point Equivalence in Same Cycle: $x \sim_f y \Rightarrow (f(x) = x \leftrightarrow f(y) = y)$

Informal description

For a permutation $f$ of a type $\alpha$ and elements $x, y \in \alpha$ that are in the same cycle of $f$, the permutation $f$ fixes $x$ if and only if it fixes $y$, i.e., $f(x) = x \leftrightarrow f(y) = y$.

Equiv.Perm.sameCycle_apply_left theorem

: SameCycle f (f x) y ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_apply_left : SameCycleSameCycle f (f x) y ↔ SameCycle f x y :=
  (Equiv.addRight 1).exists_congr_left.trans <| by
    simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]

Same Cycle Relation is Preserved Under Permutation Application on Left

Informal description

For a permutation $f$ of a type $\alpha$ and elements $x, y \in \alpha$, the elements $f(x)$ and $y$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$. In other words, $f(x) \sim_f y \leftrightarrow x \sim_f y$, where $\sim_f$ denotes the "same cycle" relation for $f$.

Equiv.Perm.sameCycle_apply_right theorem

: SameCycle f x (f y) ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_apply_right : SameCycleSameCycle f x (f y) ↔ SameCycle f x y := by
  rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]

Same Cycle Relation is Preserved Under Permutation Application on Right

Informal description

For a permutation $f$ of a type $\alpha$ and elements $x, y \in \alpha$, the elements $x$ and $f(y)$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$. In other words, $x \sim_f f(y) \leftrightarrow x \sim_f y$, where $\sim_f$ denotes the "same cycle" relation for $f$.

Equiv.Perm.sameCycle_inv_apply_left theorem

: SameCycle f (f⁻¹ x) y ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_inv_apply_left : SameCycleSameCycle f (f⁻¹ x) y ↔ SameCycle f x y := by
  rw [← sameCycle_apply_left, apply_inv_self]

Same Cycle Relation is Preserved Under Inverse Permutation Application on Left: $f^{-1}(x) \sim_f y \leftrightarrow x \sim_f y$

Informal description

For a permutation $f$ of a type $\alpha$ and elements $x, y \in \alpha$, the elements $f^{-1}(x)$ and $y$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$. In other words, $f^{-1}(x) \sim_f y \leftrightarrow x \sim_f y$, where $\sim_f$ denotes the "same cycle" relation for $f$.

Equiv.Perm.sameCycle_inv_apply_right theorem

: SameCycle f x (f⁻¹ y) ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_inv_apply_right : SameCycleSameCycle f x (f⁻¹ y) ↔ SameCycle f x y := by
  rw [← sameCycle_apply_right, apply_inv_self]

Same Cycle Relation is Preserved Under Inverse Permutation Application on Right: $x \sim_f f^{-1}(y) \leftrightarrow x \sim_f y$

Informal description

For a permutation $f$ of a type $\alpha$ and elements $x, y \in \alpha$, the elements $x$ and $f^{-1}(y)$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$. In other words, $x \sim_f f^{-1}(y) \leftrightarrow x \sim_f y$, where $\sim_f$ denotes the "same cycle" relation for $f$.

Equiv.Perm.sameCycle_zpow_left theorem

{n : ℤ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_zpow_left {n : ℤ} : SameCycleSameCycle f ((f ^ n) x) y ↔ SameCycle f x y :=
  (Equiv.addRight (n : ℤ)).exists_congr_left.trans <| by simp [SameCycle, zpow_add]

Same Cycle Relation is Invariant under Integer Powers: $\text{SameCycle } f (f^n x) y \leftrightarrow \text{SameCycle } f x y$

Informal description

For any permutation $f$ of a type $\alpha$, any elements $x, y \in \alpha$, and any integer $n$, the elements $(f^n)(x)$ and $y$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$.

Equiv.Perm.sameCycle_zpow_right theorem

{n : ℤ} : SameCycle f x ((f ^ n) y) ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_zpow_right {n : ℤ} : SameCycleSameCycle f x ((f ^ n) y) ↔ SameCycle f x y := by
  rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]

Same Cycle Relation is Invariant under Integer Powers of Permutation Applied to Second Element: $\text{SameCycle } f x (f^n y) \leftrightarrow \text{SameCycle } f x y$

Informal description

For any permutation $f$ of a type $\alpha$, any elements $x, y \in \alpha$, and any integer $n$, the elements $x$ and $(f^n)(y)$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$.

Equiv.Perm.sameCycle_pow_left theorem

{n : ℕ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_pow_left {n : ℕ} : SameCycleSameCycle f ((f ^ n) x) y ↔ SameCycle f x y := by
  rw [← zpow_natCast, sameCycle_zpow_left]

Same Cycle Relation is Invariant under Natural Powers: $\text{SameCycle } f (f^n x) y \leftrightarrow \text{SameCycle } f x y$

Informal description

For any permutation $f$ of a type $\alpha$, any elements $x, y \in \alpha$, and any natural number $n$, the elements $(f^n)(x)$ and $y$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$.

Equiv.Perm.sameCycle_pow_right theorem

{n : ℕ} : SameCycle f x ((f ^ n) y) ↔ SameCycle f x y

Full source

@[simp]
theorem sameCycle_pow_right {n : ℕ} : SameCycleSameCycle f x ((f ^ n) y) ↔ SameCycle f x y := by
  rw [← zpow_natCast, sameCycle_zpow_right]

Same Cycle Relation is Invariant under Natural Powers of Permutation Applied to Second Element: $\text{SameCycle } f x (f^n y) \leftrightarrow \text{SameCycle } f x y$

Informal description

For any permutation $f$ of a type $\alpha$, any elements $x, y \in \alpha$, and any natural number $n$, the elements $x$ and $f^n(y)$ are in the same cycle of $f$ if and only if $x$ and $y$ are in the same cycle of $f$.

Equiv.Perm.SameCycle.of_pow theorem

{n : ℕ} : SameCycle (f ^ n) x y → SameCycle f x y

Full source

theorem SameCycle.of_pow {n : ℕ} : SameCycle (f ^ n) x y → SameCycle f x y := fun ⟨m, h⟩ =>
  ⟨n * m, by simp [zpow_mul, h]⟩

Same Cycle Relation Preserved Under Powers: $\text{SameCycle}(f^n, x, y) \to \text{SameCycle}(f, x, y)$

Informal description

For any permutation $f$ of a type $\alpha$, any natural number $n$, and any elements $x, y \in \alpha$, if $x$ and $y$ are in the same cycle of the permutation $f^n$, then they are also in the same cycle of $f$.

Equiv.Perm.SameCycle.of_zpow theorem

{n : ℤ} : SameCycle (f ^ n) x y → SameCycle f x y

Full source

theorem SameCycle.of_zpow {n : ℤ} : SameCycle (f ^ n) x y → SameCycle f x y := fun ⟨m, h⟩ =>
  ⟨n * m, by simp [zpow_mul, h]⟩

Same Cycle Relation Preserved Under Integer Powers: $\text{SameCycle}(f^n, x, y) \to \text{SameCycle}(f, x, y)$

Informal description

For any permutation $f$ of a type $\alpha$, any integer $n$, and any elements $x, y \in \alpha$, if $x$ and $y$ are in the same cycle of the permutation $f^n$, then they are also in the same cycle of $f$.

Equiv.Perm.sameCycle_subtypePerm theorem

{h} {x y : { x // p x }} : (f.subtypePerm h).SameCycle x y ↔ f.SameCycle x y

Full source

@[simp]
theorem sameCycle_subtypePerm {h} {x y : { x // p x }} :
    (f.subtypePerm h).SameCycle x y ↔ f.SameCycle x y :=
  exists_congr fun n => by simp [Subtype.ext_iff]

Same Cycle Relation for Subtype Permutation

Informal description

For a permutation $ f $ of a type $ \alpha $ and a predicate $ p $ on $ \alpha $, let $ h $ be a proof that $ f $ preserves $ p $. Then for any two elements $ x $ and $ y $ in the subtype $ \{x \mid p x\} $, the following are equivalent: 1. $ x $ and $ y $ are in the same cycle of the restricted permutation $ f.\text{subtypePerm } h $. 2. $ x $ and $ y $ are in the same cycle of the original permutation $ f $.

Equiv.Perm.sameCycle_extendDomain theorem

 {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} : SameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y

Full source

@[simp]
theorem sameCycle_extendDomain {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} :
    SameCycleSameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y :=
  exists_congr fun n => by
    rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]

Same Cycle Relation Preserved Under Domain Extension

Informal description

Let $p$ be a decidable predicate on a type $\beta$, and let $f : \alpha \simeq \{x \in \beta \mid p x\}$ be an equivalence between $\alpha$ and the subtype of $\beta$ satisfying $p$. For any permutation $g$ of $\alpha$ and elements $x, y \in \alpha$, the following are equivalent: 1. The elements $f(x)$ and $f(y)$ are in the same cycle of the extended permutation $g.\text{extendDomain } f$. 2. The elements $x$ and $y$ are in the same cycle of the original permutation $g$.

Equiv.Perm.SameCycle.exists_pow_eq' theorem

[Finite α] : SameCycle f x y → ∃ i < orderOf f, (f ^ i) x = y

Full source

theorem SameCycle.exists_pow_eq' [Finite α] : SameCycle f x y → ∃ i < orderOf f, (f ^ i) x = y := by
  rintro ⟨k, rfl⟩
  use (k % orderOf f).natAbs
  have h₀ := Int.natCast_pos.mpr (orderOf_pos f)
  have h₁ := Int.emod_nonneg k h₀.ne'
  rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf]
  refine ⟨?_, by rfl⟩
  rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]
  exact Int.emod_lt_of_pos _ h₀

Existence of Power Mapping Elements in Same Cycle

Informal description

Let $\alpha$ be a finite type and $f$ a permutation of $\alpha$. If $x$ and $y$ are in the same cycle of $f$, then there exists an integer $i$ with $0 \leq i < \text{orderOf } f$ such that $f^i(x) = y$.

Equiv.Perm.SameCycle.exists_pow_eq'' theorem

[Finite α] (h : SameCycle f x y) : ∃ i : ℕ, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y

Full source

theorem SameCycle.exists_pow_eq'' [Finite α] (h : SameCycle f x y) :
    ∃ i : ℕ, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y := by
  obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
  · refine ⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩
    rw [pow_orderOf_eq_one, pow_zero]
  · exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩

Existence of Positive Power Mapping Elements in Same Cycle with Bounded Exponent

Informal description

Let $\alpha$ be a finite type and $f$ a permutation of $\alpha$. If $x$ and $y$ are in the same cycle of $f$ (i.e., $f.\text{SameCycle } x y$ holds), then there exists a positive integer $i$ such that $0 < i \leq \text{orderOf } f$ and $f^i(x) = y$.

Equiv.Perm.SameCycle.exists_fin_pow_eq theorem

[Finite α] (h : SameCycle f x y) : ∃ i : Fin (orderOf f), (f ^ (i : ℕ)) x = y

Full source

theorem SameCycle.exists_fin_pow_eq [Finite α] (h : SameCycle f x y) :
    ∃ i : Fin (orderOf f), (f ^ (i : ℕ)) x = y := by
  obtain ⟨i, hi, hx⟩ := SameCycle.exists_pow_eq' h
  exact ⟨⟨i, hi⟩, hx⟩

Existence of Finite Exponent Mapping Elements in Same Cycle

Informal description

Let $\alpha$ be a finite type and $f$ a permutation of $\alpha$. If $x$ and $y$ are in the same cycle of $f$ (i.e., $\text{SameCycle } f\ x\ y$ holds), then there exists an integer $i$ in the finite set $\{0, \dots, \text{orderOf } f - 1\}$ such that $f^i(x) = y$.

Equiv.Perm.SameCycle.exists_nat_pow_eq theorem

[Finite α] (h : SameCycle f x y) : ∃ i : ℕ, (f ^ i) x = y

Full source

theorem SameCycle.exists_nat_pow_eq [Finite α] (h : SameCycle f x y) :
    ∃ i : ℕ, (f ^ i) x = y := by
  obtain ⟨i, _, hi⟩ := h.exists_pow_eq'
  exact ⟨i, hi⟩

Existence of Natural Power Mapping Elements in Same Cycle

Informal description

Let $\alpha$ be a finite type and $f$ a permutation of $\alpha$. If $x$ and $y$ are in the same cycle of $f$, then there exists a natural number $i$ such that $f^i(x) = y$.

Equiv.Perm.instDecidableRelSameCycleInv instance

(f : Perm α) [DecidableRel (SameCycle f)] : DecidableRel (SameCycle f⁻¹)

Full source

instance (f : Perm α) [DecidableRel (SameCycle f)] :
    DecidableRel (SameCycle f⁻¹) := fun x y =>
  decidable_of_iff (f.SameCycle x y) (sameCycle_inv).symm

Decidability of Same Cycle Relation for Inverse Permutation

Informal description

For any permutation $ f $ of a type $ \alpha $, if the relation $ \text{SameCycle } f $ is decidable, then the relation $ \text{SameCycle } f^{-1} $ is also decidable.

Equiv.Perm.instDecidableRelSameCycleOfNatOfDecidableEq instance

[DecidableEq α] : DecidableRel (SameCycle (1 : Perm α))

Full source

instance (priority := 100) [DecidableEq α] : DecidableRel (SameCycle (1 : Perm α)) := fun x y =>
  decidable_of_iff (x = y) sameCycle_one.symm

Decidability of Same Cycle Relation for the Identity Permutation

Informal description

For any type $\alpha$ with decidable equality, the relation $\text{SameCycle } 1$ on $\alpha$ is decidable, where $1$ denotes the identity permutation.

Equiv.Perm.IsCycle definition

(f : Perm α) : Prop

Full source

/-- A cycle is a non identity permutation where any two nonfixed points of the permutation are
related by repeated application of the permutation. -/
def IsCycle (f : Perm α) : Prop :=
  ∃ x, f x ≠ x ∧ ∀ ⦃y⦄, f y ≠ y → SameCycle f x y

Cycle permutation

Informal description

A permutation $ f $ of a type $ \alpha $ is called a cycle if there exists an element $ x $ such that $ f(x) \neq x $ and for any other element $ y $ with $ f(y) \neq y $, the elements $ x $ and $ y $ are in the same cycle of $ f $. In other words, all non-fixed points of $ f $ lie in a single cycle.

Equiv.Perm.IsCycle.ne_one theorem

(h : IsCycle f) : f ≠ 1

Full source

theorem IsCycle.ne_one (h : IsCycle f) : f ≠ 1 := fun hf => by simp [hf, IsCycle] at h

Cycle Permutation is Not Identity

Informal description

If $f$ is a cycle permutation of a type $\alpha$, then $f$ is not the identity permutation.

Equiv.Perm.not_isCycle_one theorem

: ¬(1 : Perm α).IsCycle

Full source

@[simp]
theorem not_isCycle_one : ¬(1 : Perm α).IsCycle := fun H => H.ne_one rfl

Identity Permutation is Not a Cycle

Informal description

The identity permutation $1$ on a type $\alpha$ is not a cycle permutation.

Equiv.Perm.IsCycle.sameCycle theorem

(hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) : SameCycle f x y

Full source

protected theorem IsCycle.sameCycle (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) :
    SameCycle f x y :=
  let ⟨g, hg⟩ := hf
  let ⟨a, ha⟩ := hg.2 hx
  let ⟨b, hb⟩ := hg.2 hy
  ⟨b - a, by rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]⟩

Non-fixed Points of a Cycle Permutation Belong to the Same Cycle

Informal description

For a cycle permutation $f$ of a type $\alpha$, if $x$ and $y$ are non-fixed points of $f$ (i.e., $f(x) \neq x$ and $f(y) \neq y$), then $x$ and $y$ are in the same cycle of $f$.

Equiv.Perm.IsCycle.exists_zpow_eq theorem

: IsCycle f → f x ≠ x → f y ≠ y → ∃ i : ℤ, (f ^ i) x = y

Full source

theorem IsCycle.exists_zpow_eq : IsCycle f → f x ≠ x → f y ≠ y → ∃ i : ℤ, (f ^ i) x = y :=
  IsCycle.sameCycle

Existence of Integer Power Mapping Non-Fixed Points in a Cycle Permutation

Informal description

For any cycle permutation $f$ of a type $\alpha$ and any elements $x, y \in \alpha$ such that $f(x) \neq x$ and $f(y) \neq y$, there exists an integer $i$ such that $f^i(x) = y$.

Equiv.Perm.IsCycle.inv theorem

(hf : IsCycle f) : IsCycle f⁻¹

Full source

theorem IsCycle.inv (hf : IsCycle f) : IsCycle f⁻¹ :=
  hf.imp fun _ ⟨hx, h⟩ =>
    ⟨inv_eq_iff_eq.not.2 hx.symm, fun _ hy => (h <| inv_eq_iff_eq.not.2 hy.symm).inv⟩

Inverse of a Cycle is a Cycle

Informal description

If $f$ is a cycle permutation on a type $\alpha$, then its inverse $f^{-1}$ is also a cycle.

Equiv.Perm.isCycle_inv theorem

: IsCycle f⁻¹ ↔ IsCycle f

Full source

@[simp]
theorem isCycle_inv : IsCycleIsCycle f⁻¹ ↔ IsCycle f :=
  ⟨fun h => h.inv, IsCycle.inv⟩

Cycle Property of Permutation and Its Inverse

Informal description

A permutation $f$ of a type $\alpha$ is a cycle if and only if its inverse $f^{-1}$ is a cycle.

Equiv.Perm.IsCycle.conj theorem

: IsCycle f → IsCycle (g * f * g⁻¹)

Full source

theorem IsCycle.conj : IsCycle f → IsCycle (g * f * g⁻¹) := by
  rintro ⟨x, hx, h⟩
  refine ⟨g x, by simp [coe_mul, inv_apply_self, hx], fun y hy => ?_⟩
  rw [← apply_inv_self g y]
  exact (h <| eq_inv_iff_eq.not.2 hy).conj

Conjugation Preserves Cycle Property

Informal description

If $f$ is a cycle permutation on a type $\alpha$, then for any permutation $g$ on $\alpha$, the conjugate permutation $gfg^{-1}$ is also a cycle.

Equiv.Perm.IsCycle.extendDomain theorem

{p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : IsCycle g → IsCycle (g.extendDomain f)

Full source

protected theorem IsCycle.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
    IsCycle g → IsCycle (g.extendDomain f) := by
  rintro ⟨a, ha, ha'⟩
  refine ⟨f a, ?_, fun b hb => ?_⟩
  · rw [extendDomain_apply_image]
    exact Subtype.coe_injective.ne (f.injective.ne ha)
  have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
    rw [apply_symm_apply, Subtype.coe_mk]
  rw [h] at hb ⊢
  simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb
  exact (ha' hb).extendDomain

Cycle Property Preserved Under Permutation Extension

Informal description

Let $p$ be a decidable predicate on a type $\beta$, and let $f$ be an equivalence between $\alpha$ and the subtype of $\beta$ satisfying $p$. For any permutation $g$ of $\alpha$, if $g$ is a cycle, then its extension via $f$ to a permutation of $\beta$ is also a cycle.

Equiv.Perm.isCycle_iff_sameCycle theorem

(hx : f x ≠ x) : IsCycle f ↔ ∀ {y}, SameCycle f x y ↔ f y ≠ y

Full source

theorem isCycle_iff_sameCycle (hx : f x ≠ x) : IsCycleIsCycle f ↔ ∀ {y}, SameCycle f x y ↔ f y ≠ y :=
  ⟨fun hf y =>
    ⟨fun ⟨i, hi⟩ hy =>
      hx <| by
        rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi
        rw [hi, hy],
      hf.exists_zpow_eq hx⟩,
    fun h => ⟨x, hx, fun _ hy => h.2 hy⟩⟩

Characterization of Cycle Permutations via Non-Fixed Points and SameCycle Relation

Informal description

Let $f$ be a permutation of a type $\alpha$, and let $x \in \alpha$ be such that $f(x) \neq x$. Then $f$ is a cycle if and only if for every $y \in \alpha$, the elements $x$ and $y$ are in the same cycle of $f$ (i.e., $\text{SameCycle } f\, x\, y$) if and only if $f(y) \neq y$.

Equiv.Perm.IsCycle.exists_pow_eq theorem

(hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℕ, (f ^ i) x = y

Full source

theorem IsCycle.exists_pow_eq (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) :
    ∃ i : ℕ, (f ^ i) x = y := by
  let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy
  classical exact
      ⟨(n % orderOf f).toNat, by
        {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}⟩

Existence of Iteration Mapping Non-Fixed Points in a Cycle Permutation

Informal description

Let $f$ be a cycle permutation of a type $\alpha$, and let $x, y \in \alpha$ be two elements such that $f(x) \neq x$ and $f(y) \neq y$. Then there exists a natural number $i$ such that $f^i(x) = y$, where $f^i$ denotes the $i$-th iterate of $f$.

Equiv.Perm.isCycle_swap theorem

(hxy : x ≠ y) : IsCycle (swap x y)

Full source

theorem isCycle_swap (hxy : x ≠ y) : IsCycle (swap x y) :=
  ⟨y, by rwa [swap_apply_right], fun a (ha : ite (a = x) y (ite (a = y) x a) ≠ a) =>
    if hya : y = a then ⟨0, hya⟩
    else
      ⟨1, by
        rw [zpow_one, swap_apply_def]
        split_ifs at * <;> tauto⟩⟩

Transposition is a Cycle

Informal description

For any two distinct elements $x$ and $y$ of a type $\alpha$, the permutation that swaps $x$ and $y$ (denoted as $\text{swap } x y$) is a cycle.

Equiv.Perm.IsSwap.isCycle theorem

: IsSwap f → IsCycle f

Full source

protected theorem IsSwap.isCycle : IsSwap f → IsCycle f := by
  rintro ⟨x, y, hxy, rfl⟩
  exact isCycle_swap hxy

Transpositions are Cycles

Informal description

If a permutation $f$ is a transposition (i.e., it swaps two distinct elements), then $f$ is a cycle permutation.

Equiv.Perm.IsCycle.two_le_card_support theorem

(h : IsCycle f) : 2 ≤ #f.support

Full source

theorem IsCycle.two_le_card_support (h : IsCycle f) : 2 ≤ #f.support :=
  two_le_card_support_of_ne_one h.ne_one

Cycle Permutation Has Support of Size at Least Two

Informal description

For any cycle permutation $f$ of a type $\alpha$, the cardinality of its support (the set of elements not fixed by $f$) is at least 2, i.e., $2 \leq \#\text{supp}(f)$.

Equiv.Perm.IsCycle.zpowersEquivSupport definition

{σ : Perm α} (hσ : IsCycle σ) : (Subgroup.zpowers σ) ≃ σ.support

Full source

/-- The subgroup generated by a cycle is in bijection with its support -/
noncomputable def IsCycle.zpowersEquivSupport {σ : Perm α} (hσ : IsCycle σ) :
    (Subgroup.zpowers σ) ≃ σ.support :=
  Equiv.ofBijective
    (fun (τ : ↥ ((Subgroup.zpowers σ) : Set (Perm α))) =>
      ⟨(τ : Perm α) (Classical.choose hσ), by
        obtain ⟨τ, n, rfl⟩ := τ
        rw [Subtype.coe_mk, zpow_apply_mem_support, mem_support]
        exact (Classical.choose_spec hσ).1⟩)
    (by
      constructor
      · rintro ⟨a, m, rfl⟩ ⟨b, n, rfl⟩ h
        ext y
        by_cases hy : σ y = y
        · simp_rw [zpow_apply_eq_self_of_apply_eq_self hy]
        · obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy
          rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]
          exact congr_arg _ (Subtype.ext_iff.mp h)
      · rintro ⟨y, hy⟩
        rw [mem_support] at hy
        obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy
        exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩)

Bijection between powers of a cycle and its support

Informal description

For a cycle permutation $\sigma$ of a type $\alpha$, there is a bijection between the subgroup generated by $\sigma$ (i.e., the powers of $\sigma$) and the support of $\sigma$ (the set of elements not fixed by $\sigma$). More precisely, the bijection maps each element $\tau$ in the subgroup generated by $\sigma$ to the element $\tau(x)$ in the support of $\sigma$, where $x$ is a chosen non-fixed point of $\sigma$. Conversely, for any element $y$ in the support of $\sigma$, there exists an integer $n$ such that $\sigma^n(x) = y$, and this $n$ determines the corresponding element $\sigma^n$ in the subgroup.

Equiv.Perm.IsCycle.zpowersEquivSupport_apply theorem

 {σ : Perm α} (hσ : IsCycle σ) {n : ℕ} :
  hσ.zpowersEquivSupport ⟨σ ^ n, n, rfl⟩ =
    ⟨(σ ^ n) (Classical.choose hσ), pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩

Full source

@[simp]
theorem IsCycle.zpowersEquivSupport_apply {σ : Perm α} (hσ : IsCycle σ) {n : ℕ} :
    hσ.zpowersEquivSupport ⟨σ ^ n, n, rfl⟩ =
      ⟨(σ ^ n) (Classical.choose hσ),
        pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩ :=
  rfl

Application of the Bijection Between Powers of a Cycle and Its Support

Informal description

Let $\sigma$ be a cycle permutation of a type $\alpha$, and let $x$ be a chosen non-fixed point of $\sigma$ (i.e., $\sigma(x) \neq x$). For any natural number $n$, the bijection $\text{zpowersEquivSupport}$ maps the element $\sigma^n$ in the subgroup generated by $\sigma$ to the element $\sigma^n(x)$ in the support of $\sigma$, where $\sigma^n(x)$ is guaranteed to be in the support of $\sigma$.

Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply theorem

 {σ : Perm α} (hσ : IsCycle σ) (n : ℕ) :
  hσ.zpowersEquivSupport.symm
      ⟨(σ ^ n) (Classical.choose hσ), pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩ =
    ⟨σ ^ n, n, rfl⟩

Full source

@[simp]
theorem IsCycle.zpowersEquivSupport_symm_apply {σ : Perm α} (hσ : IsCycle σ) (n : ℕ) :
    hσ.zpowersEquivSupport.symm
        ⟨(σ ^ n) (Classical.choose hσ),
          pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩ =
      ⟨σ ^ n, n, rfl⟩ :=
  (Equiv.symm_apply_eq _).2 hσ.zpowersEquivSupport_apply

Inverse Bijection Between Support and Powers of a Cycle Permutation

Informal description

Let $\sigma$ be a cycle permutation of a type $\alpha$, and let $x$ be a chosen non-fixed point of $\sigma$ (i.e., $\sigma(x) \neq x$). For any natural number $n$, the inverse of the bijection $\text{zpowersEquivSupport}$ maps the element $\sigma^n(x)$ in the support of $\sigma$ back to the element $\sigma^n$ in the subgroup generated by $\sigma$.

Equiv.Perm.IsCycle.orderOf theorem

(hf : IsCycle f) : orderOf f = #f.support

Full source

protected theorem IsCycle.orderOf (hf : IsCycle f) : orderOf f = #f.support := by
  rw [← Fintype.card_zpowers, ← Fintype.card_coe]
  convert Fintype.card_congr (IsCycle.zpowersEquivSupport hf)

Order of a Cycle Permutation Equals Cardinality of Its Support

Informal description

For any cycle permutation $f$ of a type $\alpha$, the order of $f$ is equal to the cardinality of its support (the set of elements not fixed by $f$), i.e., $\text{orderOf}(f) = \#\text{support}(f)$.

Equiv.Perm.isCycle_swap_mul_aux₁ theorem

 {α : Type*} [DecidableEq α] :
  ∀ (n : ℕ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
    ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b

Full source

theorem isCycle_swap_mul_aux₁ {α : Type*} [DecidableEq α] :
    ∀ (n : ℕ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
      ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b := by
  intro n
  induction n with
  | zero => exact fun _ h => ⟨0, h⟩
  | succ n hn =>
    intro b x f hb h
    exact if hfbx : f x = b then ⟨0, hfbx⟩
      else
        have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
        have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b := by
          rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne, ←
            f.injective.eq_iff, apply_inv_self]
          exact this.1
        let ⟨i, hi⟩ := hn hb' (f.injective <| by
          rw [apply_inv_self]; rwa [pow_succ', mul_apply] at h)
        ⟨i + 1, by
          rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
            swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]⟩

Existence of Integer Power for Non-Fixed Point in Permutation Composition with Swap

Informal description

Let $\alpha$ be a type with decidable equality, and let $f$ be a permutation of $\alpha$. For any natural number $n$, element $b \in \alpha$, and element $x \in \alpha$, if the permutation $\text{swap}(x, f(x)) \circ f$ does not fix $b$ and $f^n(f(x)) = b$, then there exists an integer $i$ such that $(\text{swap}(x, f(x)) \circ f)^i(f(x)) = b$.

Equiv.Perm.isCycle_swap_mul_aux₂ theorem

 {α : Type*} [DecidableEq α] :
  ∀ (n : ℤ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
    ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b

Full source

theorem isCycle_swap_mul_aux₂ {α : Type*} [DecidableEq α] :
    ∀ (n : ℤ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
      ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b := by
  intro n
  cases n with
  | ofNat n => exact isCycle_swap_mul_aux₁ n
  | negSucc n =>
    intro b x f hb h
    exact if hfbx' : f x = b then ⟨0, hfbx'⟩
      else
        have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
        have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b := by
          rw [mul_apply, swap_apply_def]
          split_ifs <;>
            simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc, Ne, Perm.apply_inv_self] at *
              <;> tauto
        let ⟨i, hi⟩ :=
          isCycle_swap_mul_aux₁ n hb
            (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b by
              rw [← zpow_natCast, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc,
                ← inv_pow, pow_succ, mul_assoc, mul_assoc, inv_mul_cancel, mul_one, zpow_natCast,
                ← pow_succ', ← pow_succ])
        have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x := by
          rw [mul_apply, inv_apply_self, swap_apply_left]
        ⟨-i, by
          rw [← add_sub_cancel_right i 1, neg_sub, sub_eq_add_neg, zpow_add, zpow_one, zpow_neg,
            ← inv_zpow, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x,
            zpow_add, zpow_one, mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self,
            swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx')]⟩

Existence of Integer Power for Non-Fixed Point in Permutation Composition with Swap (Integer Version)

Informal description

Let $\alpha$ be a type with decidable equality, and let $f$ be a permutation of $\alpha$. For any integer $n$, elements $b, x \in \alpha$, if the permutation $\text{swap}(x, f(x)) \circ f$ does not fix $b$ and $f^n(f(x)) = b$, then there exists an integer $i$ such that $(\text{swap}(x, f(x)) \circ f)^i(f(x)) = b$.

Equiv.Perm.IsCycle.swap_mul theorem

 {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α} (hx : f x ≠ x) (hffx : f (f x) ≠ x) :
  IsCycle (swap x (f x) * f)

Full source

theorem IsCycle.swap_mul {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α}
    (hx : f x ≠ x) (hffx : f (f x) ≠ x) : IsCycle (swap x (f x) * f) :=
  ⟨f x, by simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, if_neg hx, hx],
    fun y hy =>
    let ⟨i, hi⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
    have hi : (f ^ (i - 1)) (f x) = y :=
      calc
        (f ^ (i - 1) : Perm α) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ) : Perm α) x := by simp
        _ = y := by rwa [← zpow_add, sub_add_cancel]

    isCycle_swap_mul_aux₂ (i - 1) hy hi⟩

Composition of a Cycle Permutation with a Transposition is a Cycle

Informal description

Let $\alpha$ be a type with decidable equality, $f$ be a cycle permutation of $\alpha$, and $x \in \alpha$ such that $f(x) \neq x$ and $f(f(x)) \neq x$. Then the composition of the transposition $\text{swap}(x, f(x))$ with $f$ is also a cycle permutation.

Equiv.Perm.IsCycle.sign theorem

{f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ #f.support

Full source

theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ #f.support :=
  let ⟨x, hx⟩ := hf
  calc
    Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by
      {rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]}
    _ = -(-1) ^ #f.support :=
      if h1 : f (f x) = x then by
        have h : swap x (f x) * f = 1 := by
          simp only [mul_def, one_def]
          rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
        rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
          hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]
        rfl
      else by
        have h : #(swap x (f x) * f).support + 1 = #f.support := by
          rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase]
        have : #(swap x (f x) * f).support < #f.support := card_support_swap_mul hx.1
        rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
        simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
termination_by #f.support

Sign of a Cycle Permutation: $\text{sign}(f) = -(-1)^{|\text{supp}(f)|}$

Informal description

For any cycle permutation $f$ of a type $\alpha$, the sign of $f$ is equal to $-(-1)^{|f.\text{support}|}$, where $f.\text{support}$ denotes the support of $f$ (the set of elements not fixed by $f$).

Equiv.Perm.IsCycle.of_pow theorem

{n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) : IsCycle f

Full source

theorem IsCycle.of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
    IsCycle f := by
  have key : ∀ x : α, (f ^ n) x ≠ x(f ^ n) x ≠ x ↔ f x ≠ x := by
    simp_rw [← mem_support, ← Finset.ext_iff]
    exact (support_pow_le _ n).antisymm h2
  obtain ⟨x, hx1, hx2⟩ := h1
  refine ⟨x, (key x).mp hx1, fun y hy => ?_⟩
  obtain ⟨i, _⟩ := hx2 ((key y).mpr hy)
  exact ⟨n * i, by rwa [zpow_mul]⟩

Cycle Property Preservation under Powers: If $f^n$ is a cycle and $\text{supp}(f) \subseteq \text{supp}(f^n)$, then $f$ is a cycle.

Informal description

Let $f$ be a permutation of a type $\alpha$, and let $n$ be a natural number. If the $n$-th power $f^n$ is a cycle and the support of $f$ is contained in the support of $f^n$, then $f$ itself is a cycle.

Equiv.Perm.IsCycle.of_zpow theorem

{n : ℤ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) : IsCycle f

Full source

theorem IsCycle.of_zpow {n : ℤ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
    IsCycle f := by
  cases n
  · exact h1.of_pow h2
  · simp only [le_eq_subset, zpow_negSucc, Perm.support_inv] at h1 h2
    exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2

Cycle Property Preservation under Integer Powers: If $f^n$ is a cycle and $\text{supp}(f) \subseteq \text{supp}(f^n)$, then $f$ is a cycle.

Informal description

Let $f$ be a permutation of a type $\alpha$, and let $n$ be an integer. If the $n$-th power $f^n$ is a cycle and the support of $f$ is contained in the support of $f^n$, then $f$ itself is a cycle.

Equiv.Perm.nodup_of_pairwise_disjoint_cycles theorem

{l : List (Perm β)} (h1 : ∀ f ∈ l, IsCycle f) (h2 : l.Pairwise Disjoint) : l.Nodup

Full source

theorem nodup_of_pairwise_disjoint_cycles {l : List (Perm β)} (h1 : ∀ f ∈ l, IsCycle f)
    (h2 : l.Pairwise Disjoint) : l.Nodup :=
  nodup_of_pairwise_disjoint (fun h => (h1 1 h).ne_one rfl) h2

List of Pairwise Disjoint Cycles Has No Duplicates

Informal description

For any list $l$ of permutations of a type $\beta$, if every permutation $f$ in $l$ is a cycle and the permutations in $l$ are pairwise disjoint (i.e., their supports are pairwise disjoint), then the list $l$ has no duplicate elements.

Equiv.Perm.IsCycle.support_congr theorem

(hf : IsCycle f) (hg : IsCycle g) (h : f.support ⊆ g.support) (h' : ∀ x ∈ f.support, f x = g x) : f = g

Full source

/-- 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 IsCycle.support_congr (hf : IsCycle f) (hg : IsCycle g) (h : f.support ⊆ g.support)
    (h' : ∀ x ∈ f.support, f x = g x) : f = g := by
  have : f.support = g.support := by
    refine le_antisymm h ?_
    intro z hz
    obtain ⟨x, hx, _⟩ := id hf
    have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
    obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
    have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
    rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
  refine Equiv.Perm.support_congr h ?_
  simpa [← this] using h'

Cycle Equality Under Support and Value Conditions

Informal description

Let $f$ and $g$ be cycle permutations of a type $\alpha$ such that: 1. The support of $f$ is contained in the support of $g$ (i.e., $\text{supp}(f) \subseteq \text{supp}(g)$), and 2. For every $x$ in the support of $f$, we have $f(x) = g(x)$. Then $f = g$.

Equiv.Perm.IsCycle.support_pow_eq_iff theorem

(hf : IsCycle f) {n : ℕ} : support (f ^ n) = support f ↔ ¬orderOf f ∣ n

Full source

theorem IsCycle.support_pow_eq_iff (hf : IsCycle f) {n : ℕ} :
    supportsupport (f ^ n) = support f ↔ ¬orderOf f ∣ n := by
  rw [orderOf_dvd_iff_pow_eq_one]
  constructor
  · intro h H
    refine hf.ne_one ?_
    rw [← support_eq_empty_iff, ← h, H, support_one]
  · intro H
    apply le_antisymm (support_pow_le _ n) _
    intro x hx
    contrapose! H
    ext z
    by_cases hz : f z = z
    · rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
    · obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
      apply (f ^ k).injective
      rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
      simpa using H

Support Equality of Cycle Powers: $\text{supp}(f^n) = \text{supp}(f) \leftrightarrow \text{ord}(f) \nmid n$

Informal description

Let $f$ be a cycle permutation of a finite type $\beta$, and let $n$ be a natural number. Then the support of $f^n$ equals the support of $f$ if and only if $n$ is not divisible by the order of $f$.

Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf theorem

(hf : IsCycle f) {n : ℕ} (npos : 0 < n) (hn : n < orderOf f) : (f ^ n).support = f.support

Full source

theorem IsCycle.support_pow_of_pos_of_lt_orderOf (hf : IsCycle f) {n : ℕ} (npos : 0 < n)
    (hn : n < orderOf f) : (f ^ n).support = f.support :=
  hf.support_pow_eq_iff.2 <| Nat.not_dvd_of_pos_of_lt npos hn

Support Equality for Powers of a Cycle Permutation When $0 < n < \text{ord}(f)$

Informal description

Let $f$ be a cycle permutation of a finite type $\beta$, and let $n$ be a positive natural number such that $n$ is less than the order of $f$. Then the support of $f^n$ equals the support of $f$.

Equiv.Perm.IsCycle.pow_iff theorem

[Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} : IsCycle (f ^ n) ↔ n.Coprime (orderOf f)

Full source

theorem IsCycle.pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    IsCycleIsCycle (f ^ n) ↔ n.Coprime (orderOf f) := by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine hf'.of_pow fun x hx => ?_
      rw [hm]
      exact support_pow_le _ n hx

Cycle Property of Powers: $f^n$ is a cycle $\leftrightarrow$ $n$ and $\text{ord}(f)$ are coprime

Informal description

Let $f$ be a cycle permutation of a finite type $\beta$, and let $n$ be a natural number. Then the $n$-th power $f^n$ is a cycle if and only if $n$ is coprime with the order of $f$.

Equiv.Perm.IsCycle.pow_eq_one_iff theorem

[Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} : f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x

Full source

theorem IsCycle.pow_eq_one_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x := by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]

Cycle Permutation Power Identity Criterion: $f^n = 1 \leftrightarrow \exists x, f(x) \neq x \land f^n(x) = x$

Informal description

Let $f$ be a cycle permutation of a finite type $\beta$. For any natural number $n$, the permutation $f^n$ is the identity if and only if there exists an element $x \in \beta$ such that $f(x) \neq x$ and $(f^n)(x) = x$.

Equiv.Perm.IsCycle.pow_eq_one_iff' theorem

[Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} {x : β} (hx : f x ≠ x) : f ^ n = 1 ↔ (f ^ n) x = x

Full source

theorem IsCycle.pow_eq_one_iff' [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} {x : β}
    (hx : f x ≠ x) : f ^ n = 1 ↔ (f ^ n) x = x :=
  ⟨fun h => DFunLike.congr_fun h x, fun h => hf.pow_eq_one_iff.2 ⟨x, hx, h⟩⟩

Cycle Permutation Power Identity Criterion at Non-Fixed Point: $f^n = 1 \leftrightarrow f^n(x) = x$ for $f(x) \neq x$

Informal description

Let $f$ be a cycle permutation of a finite type $\beta$, and let $n$ be a natural number. For any element $x \in \beta$ such that $f(x) \neq x$, the permutation $f^n$ is the identity if and only if $(f^n)(x) = x$.

Equiv.Perm.IsCycle.pow_eq_one_iff'' theorem

[Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} : f ^ n = 1 ↔ ∀ x, f x ≠ x → (f ^ n) x = x

Full source

theorem IsCycle.pow_eq_one_iff'' [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    f ^ n = 1 ↔ ∀ x, f x ≠ x → (f ^ n) x = x :=
  ⟨fun h _ hx => (hf.pow_eq_one_iff' hx).1 h, fun h =>
    let ⟨_, hx, _⟩ := id hf
    (hf.pow_eq_one_iff' hx).2 (h _ hx)⟩

Cycle Permutation Power Identity Criterion for All Non-Fixed Points: $f^n = 1 \leftrightarrow \forall x, f(x) \neq x \to f^n(x) = x$

Informal description

Let $f$ be a cycle permutation on a finite type $\beta$. For any natural number $n$, the permutation $f^n$ is the identity if and only if for every element $x \in \beta$ with $f(x) \neq x$, we have $(f^n)(x) = x$.

Equiv.Perm.IsCycle.pow_eq_pow_iff theorem

[Finite β] {f : Perm β} (hf : IsCycle f) {a b : ℕ} : f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Full source

theorem IsCycle.pow_eq_pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {a b : ℕ} :
    f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x := by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_le hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp only [pow_sub _ hab, Equiv.Perm.coe_mul, Function.comp_apply, inv_apply_self, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [not_mem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction

Cycle Permutation Powers Equality Criterion: $f^a = f^b \leftrightarrow \exists x, f(x) \neq x \land f^a(x) = f^b(x)$

Informal description

Let $f$ be a cycle permutation on a finite type $\beta$. For any natural numbers $a$ and $b$, the equality $f^a = f^b$ holds if and only if there exists an element $x \in \beta$ such that $f(x) \neq x$ and $(f^a)(x) = (f^b)(x)$.

Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order theorem

 [Finite β] {f : Perm β} (hf : IsCycle f) (hf' : (orderOf f).Prime) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) :
  IsCycle (f ^ n)

Full source

theorem IsCycle.isCycle_pow_pos_of_lt_prime_order [Finite β] {f : Perm β} (hf : IsCycle f)
    (hf' : (orderOf f).Prime) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) : IsCycle (f ^ n) := by
  classical
    cases nonempty_fintype β
    have : n.Coprime (orderOf f) := by
      refine Nat.Coprime.symm ?_
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
    obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime this
    have hf'' := hf
    rw [← hm] at hf''
    refine hf''.of_pow ?_
    rw [hm]
    exact support_pow_le f n

Powers of a Cycle Permutation with Prime Order are Cycles for $0 < n < \text{orderOf}(f)$

Informal description

Let $f$ be a cycle permutation on a finite type $\beta$ with prime order. For any positive integer $n$ such that $0 < n < \text{orderOf}(f)$, the $n$-th power of $f$ is also a cycle permutation.

Int.addLeft_one_isCycle theorem

: (Equiv.addLeft 1 : Perm ℤ).IsCycle

Full source

theorem _root_.Int.addLeft_one_isCycle : (Equiv.addLeft 1 : Perm ℤ).IsCycle :=
  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩

Left Addition by One is a Cycle Permutation on Integers

Informal description

The permutation of the integers $\mathbb{Z}$ defined by $x \mapsto x + 1$ is a cycle.

Int.addRight_one_isCycle theorem

: (Equiv.addRight 1 : Perm ℤ).IsCycle

Full source

theorem _root_.Int.addRight_one_isCycle : (Equiv.addRight 1 : Perm ℤ).IsCycle :=
  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩

Right Addition by One is a Cycle Permutation on Integers

Informal description

The permutation of the integers $\mathbb{Z}$ defined by $x \mapsto x + 1$ is a cycle.

Equiv.Perm.IsCycle.isConj theorem

(hσ : IsCycle σ) (hτ : IsCycle τ) (h : #σ.support = #τ.support) : IsConj σ τ

Full source

theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : #σ.support = #τ.support) :
    IsConj σ τ := by
  refine
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      ?_
  intro x hx
  simp only [Perm.mul_apply, Equiv.trans_apply, Equiv.sumCongr_apply]
  obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
  simp [← Perm.mul_apply, ← pow_succ']

Conjugacy of Cycle Permutations with Equal Support Size

Informal description

Let $\sigma$ and $\tau$ be cycle permutations of a type $\alpha$. If the supports of $\sigma$ and $\tau$ (the sets of elements not fixed by each permutation) have the same cardinality, then $\sigma$ and $\tau$ are conjugate in the symmetric group on $\alpha$.

Equiv.Perm.IsCycle.isConj_iff theorem

(hσ : IsCycle σ) (hτ : IsCycle τ) : IsConj σ τ ↔ #σ.support = #τ.support

Full source

theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
    IsConjIsConj σ τ ↔ #σ.support = #τ.support where
  mp h := by
    obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
    refine Finset.card_bij (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab)
        fun b hb ↦ ⟨π⁻¹ b, ?_, π.apply_inv_self b⟩
    · simp [mem_support.1 ha]
    contrapose! hb
    rw [mem_support, Classical.not_not] at hb
    rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self]
  mpr := hσ.isConj hτ

Conjugacy Criterion for Cycle Permutations: $\sigma \sim \tau \iff |\text{supp}(\sigma)| = |\text{supp}(\tau)|$

Informal description

Let $\sigma$ and $\tau$ be cycle permutations of a type $\alpha$. Then $\sigma$ and $\tau$ are conjugate in the symmetric group on $\alpha$ if and only if their supports (the sets of elements not fixed by each permutation) have the same cardinality.

Equiv.Perm.IsCycleOn definition

(f : Perm α) (s : Set α) : Prop

Full source

/-- 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. -/
def IsCycleOn (f : Perm α) (s : Set α) : Prop :=
  Set.BijOnSet.BijOn f s s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → f.SameCycle x y

Cycle of a permutation on a set

Informal description

A permutation $ f $ of a type $ \alpha $ is called a cycle on a set $ s \subseteq \alpha $ if $ f $ restricts to a bijection on $ s $ and for any two elements $ x, y \in s $, there exists an integer $ i $ such that $ f^i(x) = y $. Note that the identity permutation is considered a cycle on any subsingleton set $ s $.

Equiv.Perm.isCycleOn_empty theorem

: f.IsCycleOn ∅

Full source

@[simp]
theorem isCycleOn_empty : f.IsCycleOn ∅ := by simp [IsCycleOn, Set.bijOn_empty]

Every Permutation is a Cycle on the Empty Set

Informal description

For any permutation $f$ of a type $\alpha$, $f$ is a cycle on the empty set $\emptyset$.

Equiv.Perm.isCycleOn_one theorem

: (1 : Perm α).IsCycleOn s ↔ s.Subsingleton

Full source

@[simp]
theorem isCycleOn_one : (1 : Perm α).IsCycleOn s ↔ s.Subsingleton := by
  simp [IsCycleOn, Set.bijOn_id, Set.Subsingleton]

Identity Permutation is a Cycle on a Set if and only if the Set is a Subsingleton

Informal description

The identity permutation $1$ is a cycle on a set $s$ if and only if $s$ is a subsingleton (i.e., $s$ has at most one element).

Equiv.Perm.isCycleOn_singleton theorem

: f.IsCycleOn { a } ↔ f a = a

Full source

@[simp]
theorem isCycleOn_singleton : f.IsCycleOn {a} ↔ f a = a := by simp [IsCycleOn, SameCycle.rfl]

Cycle on Singleton Set is Equivalent to Fixing the Element

Informal description

A permutation $f$ is a cycle on the singleton set $\{a\}$ if and only if $f$ fixes $a$, i.e., $f(a) = a$.

Equiv.Perm.isCycleOn_of_subsingleton theorem

[Subsingleton α] (f : Perm α) (s : Set α) : f.IsCycleOn s

Full source

theorem isCycleOn_of_subsingleton [Subsingleton α] (f : Perm α) (s : Set α) : f.IsCycleOn s :=
  ⟨s.bijOn_of_subsingleton _, fun x _ y _ => (Subsingleton.elim x y).sameCycle _⟩

Every Permutation is a Cycle on Any Set in a Subsingleton Type

Informal description

For any type $\alpha$ that is a subsingleton (i.e., has at most one element), any permutation $f$ of $\alpha$ is a cycle on any subset $s \subseteq \alpha$.

Equiv.Perm.isCycleOn_inv theorem

: f⁻¹.IsCycleOn s ↔ f.IsCycleOn s

Full source

@[simp]
theorem isCycleOn_inv : f⁻¹f⁻¹.IsCycleOn s ↔ f.IsCycleOn s := by
  simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]
  exact fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩

Inverse Permutation Preserves Cycle Property on a Set

Informal description

For any permutation $f$ of a type $\alpha$ and any subset $s \subseteq \alpha$, the inverse permutation $f^{-1}$ is a cycle on $s$ if and only if $f$ is a cycle on $s$.

Equiv.Perm.IsCycleOn.conj theorem

(h : f.IsCycleOn s) : (g * f * g⁻¹).IsCycleOn ((g : Perm α) '' s)

Full source

theorem IsCycleOn.conj (h : f.IsCycleOn s) : (g * f * g⁻¹).IsCycleOn ((g : Perm α) '' s) :=
  ⟨(g.bijOn_image.comp h.1).comp g.bijOn_symm_image, fun x hx y hy => by
    rw [← preimage_inv] at hx hy
    convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]⟩

Conjugation Preserves Cycle Property: $gfg^{-1}$ is a cycle on $g(s)$ if $f$ is a cycle on $s$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$, and let $g$ be another permutation of $\alpha$. Then the conjugate permutation $gfg^{-1}$ is a cycle on the image of $s$ under $g$, i.e., $g(s) = \{g(x) \mid x \in s\}$.

Equiv.Perm.isCycleOn_swap theorem

[DecidableEq α] (hab : a ≠ b) : (swap a b).IsCycleOn { a, b }

Full source

theorem isCycleOn_swap [DecidableEq α] (hab : a ≠ b) : (swap a b).IsCycleOn {a, b} :=
  ⟨bijOn_swap (by simp) (by simp), fun x hx y hy => by
    rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy
    obtain rfl | rfl := hx <;> obtain rfl | rfl := hy
    · exact ⟨0, by rw [zpow_zero, coe_one, id]⟩
    · exact ⟨1, by rw [zpow_one, swap_apply_left]⟩
    · exact ⟨1, by rw [zpow_one, swap_apply_right]⟩
    · exact ⟨0, by rw [zpow_zero, coe_one, id]⟩⟩

Transposition is a Cycle on Two Elements

Informal description

For any type $\alpha$ with decidable equality and distinct elements $a, b \in \alpha$, the transposition (swap) permutation $\text{swap } a b$ is a cycle on the set $\{a, b\}$.

Equiv.Perm.IsCycleOn.apply_ne theorem

(hf : f.IsCycleOn s) (hs : s.Nontrivial) (ha : a ∈ s) : f a ≠ a

Full source

protected theorem IsCycleOn.apply_ne (hf : f.IsCycleOn s) (hs : s.Nontrivial) (ha : a ∈ s) :
    f a ≠ a := by
  obtain ⟨b, hb, hba⟩ := hs.exists_ne a
  obtain ⟨n, rfl⟩ := hf.2 ha hb
  exact fun h => hba (IsFixedPt.perm_zpow h n)

Non-fixed Points in Nontrivial Cycles

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$, and suppose $s$ is nontrivial (i.e., contains at least two distinct elements). Then for any element $a \in s$, the permutation $f$ does not fix $a$, i.e., $f(a) \neq a$.

Equiv.Perm.IsCycle.isCycleOn theorem

(hf : f.IsCycle) : f.IsCycleOn {x | f x ≠ x}

Full source

protected theorem IsCycle.isCycleOn (hf : f.IsCycle) : f.IsCycleOn { x | f x ≠ x } :=
  ⟨f.bijOn fun _ => f.apply_eq_iff_eq.not, fun _ ha _ => hf.sameCycle ha⟩

Cycle Permutation is Cycle on Non-Fixed Points

Informal description

If $f$ is a cycle permutation of a type $\alpha$, then $f$ is a cycle on the set of non-fixed points of $f$, i.e., on the set $\{x \in \alpha \mid f(x) \neq x\}$.

Equiv.Perm.isCycle_iff_exists_isCycleOn theorem

: f.IsCycle ↔ ∃ s : Set α, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x⦄, ¬IsFixedPt f x → x ∈ s

Full source

/-- This lemma demonstrates the relation between `Equiv.Perm.IsCycle` and `Equiv.Perm.IsCycleOn`
in non-degenerate cases. -/
theorem isCycle_iff_exists_isCycleOn :
    f.IsCycle ↔ ∃ s : Set α, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x⦄, ¬IsFixedPt f x → x ∈ s := by
  refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
  · obtain ⟨a, ha⟩ := hf
    exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
  · rintro ⟨s, hs, hf, hsf⟩
    obtain ⟨a, ha⟩ := hs.nonempty
    exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩

Characterization of Cycle Permutations via Cycle-on-Set Condition

Informal description

A permutation $f$ of a type $\alpha$ is a cycle if and only if there exists a nontrivial subset $s \subseteq \alpha$ such that: 1. $f$ is a cycle on $s$, 2. Every non-fixed point of $f$ (i.e., every $x$ with $f(x) \neq x$) belongs to $s$.

Equiv.Perm.IsCycleOn.apply_mem_iff theorem

(hf : f.IsCycleOn s) : f x ∈ s ↔ x ∈ s

Full source

theorem IsCycleOn.apply_mem_iff (hf : f.IsCycleOn s) : f x ∈ sf x ∈ s ↔ x ∈ s :=
  ⟨fun hx => by
    convert hf.1.perm_inv.1 hx
    rw [inv_apply_self], fun hx => hf.1.mapsTo hx⟩

Cycle-on-Set Membership Preservation under Permutation

Informal description

For a permutation $f$ of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$, an element $x \in \alpha$ satisfies $f(x) \in s$ if and only if $x \in s$.

Equiv.Perm.IsCycleOn.isCycle_subtypePerm theorem

(hf : f.IsCycleOn s) (hs : s.Nontrivial) : (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycle

Full source

/-- Note that the identity satisfies `IsCycleOn` for any subsingleton set, but not `IsCycle`. -/
theorem IsCycleOn.isCycle_subtypePerm (hf : f.IsCycleOn s) (hs : s.Nontrivial) :
    (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycle := by
  obtain ⟨a, ha⟩ := hs.nonempty
  exact
    ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩

Cycle-on-Set Induces Cycle Permutation on Nontrivial Subset

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$, and suppose $s$ is nontrivial (i.e., contains at least two distinct elements). Then the restriction of $f$ to $s$, viewed as a permutation of $s$, is a cycle.

Equiv.Perm.IsCycleOn.subtypePerm theorem

(hf : f.IsCycleOn s) : (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycleOn _root_.Set.univ

Full source

/-- Note that the identity is a cycle on any subsingleton set, but not a cycle. -/
protected theorem IsCycleOn.subtypePerm (hf : f.IsCycleOn s) :
    (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycleOn _root_.Set.univ := by
  obtain hs | hs := s.subsingleton_or_nontrivial
  · haveI := hs.coe_sort
    exact isCycleOn_of_subsingleton _ _
  convert (hf.isCycle_subtypePerm hs).isCycleOn
  rw [eq_comm, Set.eq_univ_iff_forall]
  exact fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)

Cycle-on-Set Restriction Yields Cycle on Entire Subtype

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$. Then the restriction of $f$ to $s$, viewed as a permutation of $s$, is a cycle on the entire set $s$ (i.e., on $\text{Set.univ}$ for the subtype $s$).

Equiv.Perm.IsCycleOn.pow_apply_eq theorem

{s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {n : ℕ} : (f ^ n) a = a ↔ #s ∣ n

Full source

theorem IsCycleOn.pow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {n : ℕ} :
    (f ^ n) a = a ↔ #s ∣ n := by
  obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha
  · rw [coe_singleton, isCycleOn_singleton] at hf
    simpa using IsFixedPt.iterate hf n
  classical
    have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    simp only [coe_sort_coe, support_subtype_perm, ne_eq, h, not_false_eq_true, univ_eq_attach,
      mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-coe_sort_coe]

Cycle-on-Set Power Fixing Criterion: $f^n(a) = a \leftrightarrow \#s \mid n$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a \in s$. For any natural number $n$, the $n$-th power of $f$ fixes $a$ (i.e., $f^n(a) = a$) if and only if the cardinality of $s$ divides $n$.

Equiv.Perm.IsCycleOn.zpow_apply_eq theorem

{s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) : ∀ {n : ℤ}, (f ^ n) a = a ↔ (#s : ℤ) ∣ n

Full source

theorem IsCycleOn.zpow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) :
    ∀ {n : ℤ}, (f ^ n) a = a ↔ (#s : ℤ) ∣ n
  | Int.ofNat _ => (hf.pow_apply_eq ha).trans Int.natCast_dvd_natCast.symm
  | Int.negSucc n => by
    rw [zpow_negSucc, ← inv_pow]
    exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Cycle-on-Set Integer Power Fixing Criterion: $f^n(a) = a \leftrightarrow \#s \mid n$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a \in s$. For any integer $n$, the $n$-th power of $f$ fixes $a$ (i.e., $f^n(a) = a$) if and only if the cardinality of $s$ divides $n$ (as integers).

Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply theorem

{s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {m n : ℕ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD #s]

Full source

theorem IsCycleOn.pow_apply_eq_pow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s)
    {m n : ℕ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD #s] := by
  rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]

Cycle-on-Set Power Congruence Criterion: $f^m(a) = f^n(a) \leftrightarrow m \equiv n \mod \#s$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a \in s$. For any natural numbers $m$ and $n$, the $m$-th and $n$-th powers of $f$ applied to $a$ are equal (i.e., $f^m(a) = f^n(a)$) if and only if $m$ and $n$ are congruent modulo the cardinality of $s$.

Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply theorem

{s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {m n : ℤ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD #s]

Full source

theorem IsCycleOn.zpow_apply_eq_zpow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s)
    {m n : ℤ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD #s] := by
  rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]

Cycle-on-Set Integer Power Congruence Criterion: $f^m(a) = f^n(a) \leftrightarrow m \equiv n \pmod{\#s}$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a \in s$. For any integers $m$ and $n$, the $m$-th and $n$-th powers of $f$ applied to $a$ are equal (i.e., $f^m(a) = f^n(a)$) if and only if $m \equiv n \pmod{\#s}$.

Equiv.Perm.IsCycleOn.pow_card_apply theorem

{s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) : (f ^ #s) a = a

Full source

theorem IsCycleOn.pow_card_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) :
    (f ^ #s) a = a :=
  (hf.pow_apply_eq ha).2 dvd_rfl

Cycle-on-Set Fixpoint Property: $f^{\#s}(a) = a$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a \in s$. Then the $\#s$-th power of $f$ fixes $a$, i.e., $f^{\#s}(a) = a$.

Equiv.Perm.IsCycleOn.exists_pow_eq theorem

{s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) : ∃ n < #s, (f ^ n) a = b

Full source

theorem IsCycleOn.exists_pow_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
    ∃ n < #s, (f ^ n) a = b := by
  classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
    refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
    rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _

Existence of Power Mapping Elements in a Cycle-on-Set: $f^n(a) = b$ for some $n < \#s$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a, b \in s$. Then there exists a natural number $n$ less than the cardinality of $s$ such that the $n$-th power of $f$ maps $a$ to $b$, i.e., $f^n(a) = b$.

Equiv.Perm.IsCycleOn.exists_pow_eq' theorem

(hs : s.Finite) (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) : ∃ n : ℕ, (f ^ n) a = b

Full source

theorem IsCycleOn.exists_pow_eq' (hs : s.Finite) (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
    ∃ n : ℕ, (f ^ n) a = b := by
  lift s to Finset α using id hs
  obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb
  exact ⟨n, hn⟩

Existence of Power Mapping Elements in a Finite Cycle-on-Set: $f^n(a) = b$ for some $n$

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and let $a, b \in s$. Then there exists a natural number $n$ such that the $n$-th power of $f$ maps $a$ to $b$, i.e., $f^n(a) = b$.

Equiv.Perm.IsCycleOn.range_pow theorem

(hs : s.Finite) (h : f.IsCycleOn s) (ha : a ∈ s) : Set.range (fun n => (f ^ n) a : ℕ → α) = s

Full source

theorem IsCycleOn.range_pow (hs : s.Finite) (h : f.IsCycleOn s) (ha : a ∈ s) :
    Set.range (fun n => (f ^ n) a : ℕ → α) = s :=
  Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => h.1.mapsTo.perm_pow _ ha) fun _ =>
    h.exists_pow_eq' hs ha

Range of Natural Powers of a Cyclic Permutation on a Finite Set Equals the Set

Informal description

For a permutation $f$ of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$, and for any element $a \in s$, the range of the function $n \mapsto f^n(a)$ over all natural numbers $n \in \mathbb{N}$ is equal to $s$. In other words, every element of $s$ can be obtained by applying some natural number power of $f$ to $a$.

Equiv.Perm.IsCycleOn.range_zpow theorem

(h : f.IsCycleOn s) (ha : a ∈ s) : Set.range (fun n => (f ^ n) a : ℤ → α) = s

Full source

theorem IsCycleOn.range_zpow (h : f.IsCycleOn s) (ha : a ∈ s) :
    Set.range (fun n => (f ^ n) a : ℤ → α) = s :=
  Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => (h.1.perm_zpow _).mapsTo ha) <| h.2 ha

Range of Integer Powers of a Cyclic Permutation on a Set

Informal description

For a permutation $f$ of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$, and for any element $a \in s$, the range of the function $n \mapsto f^n(a)$ over all integers $n \in \mathbb{Z}$ is equal to $s$. In other words, every element of $s$ can be obtained by applying some integer power of $f$ to $a$.

Equiv.Perm.IsCycleOn.of_pow theorem

{n : ℕ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) : f.IsCycleOn s

Full source

theorem IsCycleOn.of_pow {n : ℕ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) : f.IsCycleOn s :=
  ⟨h, fun _ hx _ hy => (hf.2 hx hy).of_pow⟩

Cycle Property Preservation Under Powers: $(f^n \text{ is cycle on } s) \to (f \text{ is cycle on } s)$

Informal description

For a permutation $f$ of a type $\alpha$, a natural number $n$, and a subset $s \subseteq \alpha$, if the $n$-th power $f^n$ is a cycle on $s$ and $f$ restricts to a bijection on $s$, then $f$ itself is a cycle on $s$.

Equiv.Perm.IsCycleOn.of_zpow theorem

{n : ℤ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) : f.IsCycleOn s

Full source

theorem IsCycleOn.of_zpow {n : ℤ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) :
    f.IsCycleOn s :=
  ⟨h, fun _ hx _ hy => (hf.2 hx hy).of_zpow⟩

Cycle Property Preservation Under Integer Powers: $(f^n \text{ is cycle on } s) \to (f \text{ is cycle on } s)$

Informal description

For any integer $n$, if the permutation $f^n$ is a cycle on a set $s$ and $f$ restricts to a bijection on $s$, then $f$ itself is a cycle on $s$.

Equiv.Perm.IsCycleOn.extendDomain theorem

 {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (h : g.IsCycleOn s) : (g.extendDomain f).IsCycleOn ((↑) ∘ f '' s)

Full source

theorem IsCycleOn.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
    (h : g.IsCycleOn s) : (g.extendDomain f).IsCycleOn ((↑) ∘ f(↑) ∘ f '' s) :=
  ⟨h.1.extendDomain, by
    rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
    exact (h.2 ha hb).extendDomain⟩

Cycle Preservation under Permutation Extension

Informal description

Let $p$ be a decidable predicate on a type $\beta$, and let $f : \alpha \simeq \{x \in \beta \mid p(x)\}$ be an equivalence. If a permutation $g$ of $\alpha$ is a cycle on a set $s \subseteq \alpha$, then the extended permutation $g.\text{extendDomain}(f)$ is a cycle on the image of $s$ under the composition of the coercion map and $f$, i.e., on $\{f(x) \mid x \in s\}$.

Equiv.Perm.IsCycleOn.countable theorem

(hs : f.IsCycleOn s) : s.Countable

Full source

protected theorem IsCycleOn.countable (hs : f.IsCycleOn s) : s.Countable := by
  obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty
  · exact Set.countable_empty
  · exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)

Countability of the Support of a Cyclic Permutation

Informal description

If a permutation $f$ on a type $\alpha$ is a cycle on a set $s \subseteq \alpha$, then $s$ is countable.

List.Nodup.isCycleOn_formPerm theorem

(h : l.Nodup) : l.formPerm.IsCycleOn {a | a ∈ l}

Full source

theorem Nodup.isCycleOn_formPerm (h : l.Nodup) :
    l.formPerm.IsCycleOn { a | a ∈ l } := by
  refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
  rw [Set.mem_setOf, ← List.idxOf_lt_length_iff] at ha hb
  rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]
  refine ⟨l.idxOf b - l.idxOf a, ?_⟩
  simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast,
    Equiv.Perm.coe_mul, List.formPerm_pow_apply_getElem _ h, Function.comp]
  rw [add_comm]

Cycle Property of Permutation Generated by a List of Distinct Elements

Informal description

For any list `l` of distinct elements (i.e., `l.Nodup` holds), the permutation `l.formPerm` is a cycle on the set of elements occurring in `l`. In other words, the permutation generated by the list cycles through all its elements.

Finset.exists_cycleOn theorem

(s : Finset α) : ∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s

Full source

theorem exists_cycleOn (s : Finset α) :
    ∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s := by
  refine ⟨s.toList.formPerm, ?_, fun x hx => by
    simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)⟩
  convert s.nodup_toList.isCycleOn_formPerm
  simp

Existence of a Cycle Permutation on a Finite Set

Informal description

For any finite set $s$ of type $\alpha$, there exists a permutation $f$ of $\alpha$ such that $f$ is a cycle on $s$ and the support of $f$ (the set of elements moved by $f$) is contained in $s$.

Set.Countable.exists_cycleOn theorem

(hs : s.Countable) : ∃ f : Perm α, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Full source

theorem Countable.exists_cycleOn (hs : s.Countable) :
    ∃ f : Perm α, f.IsCycleOn s ∧ { x | f x ≠ x } ⊆ s := by
  classical
  obtain hs' | hs' := s.finite_or_infinite
  · refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne hx⟩
    convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
    simp
  · haveI := hs.to_subtype
    haveI := hs'.to_subtype
    obtain ⟨f⟩ : Nonempty (ℤℤ ≃ s) := inferInstance
    refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
    convert Int.addRight_one_isCycle.isCycleOn.extendDomain f
    rw [Set.image_comp, Equiv.image_eq_preimage]
    ext
    simp

Existence of a Cycle Permutation on a Countable Set

Informal description

For any countable set $s$ in a type $\alpha$, there exists a permutation $f$ of $\alpha$ such that $f$ is a cycle on $s$ and the set of non-fixed points $\{x \mid f(x) \neq x\}$ is contained in $s$.

Set.prod_self_eq_iUnion_perm theorem

(hf : f.IsCycleOn s) : s ×ˢ s = ⋃ n : ℤ, (fun a => (a, (f ^ n) a)) '' s

Full source

theorem prod_self_eq_iUnion_perm (hf : f.IsCycleOn s) :
    s ×ˢ s = ⋃ n : ℤ, (fun a => (a, (f ^ n) a)) '' s := by
  ext ⟨a, b⟩
  simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
  refine ⟨fun hx => ?_, ?_⟩
  · obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
    exact ⟨_, _, hx.1, rfl⟩
  · rintro ⟨n, a, ha, ⟨⟩⟩
    exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩

Cartesian Product Decomposition for Cycle Permutations

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a set $s \subseteq \alpha$. Then the Cartesian product $s \times s$ equals the union over all integers $n$ of the images of $s$ under the map $a \mapsto (a, f^n(a))$.

Finset.product_self_eq_disjiUnion_perm_aux theorem

 (hf : f.IsCycleOn s) :
  (range #s : Set ℕ).PairwiseDisjoint fun k => s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩

Full source

theorem product_self_eq_disjiUnion_perm_aux (hf : f.IsCycleOn s) :
    (range #s : Set ℕ).PairwiseDisjoint fun k =>
      s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩ := by
  obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
  · refine Set.Subsingleton.pairwise ?_ _
    simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢
    rwa [card_range]
  classical
    rintro m hm n hn hmn
    simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk, exists_prop,
      not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk_inj]
    rintro _ _ _ - rfl rfl a ha rfl h
    rw [hf.pow_apply_eq_pow_apply ha] at h
    rw [mem_coe, mem_range] at hm hn
    exact hmn.symm (h.eq_of_lt_of_lt hn hm)

Pairwise Disjointness of Graph Powers in Cycle Permutations

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$. Then for any natural numbers $k$ in the range $[0, \#s)$, the images of $s$ under the maps $i \mapsto (i, f^k(i))$ are pairwise disjoint as subsets of $s \times s$.

Finset.product_self_eq_disjiUnion_perm theorem

 (hf : f.IsCycleOn s) :
  s ×ˢ s =
    (range #s).disjiUnion (fun k => s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩)
      (product_self_eq_disjiUnion_perm_aux hf)

Full source

/-- 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 product_self_eq_disjiUnion_perm (hf : f.IsCycleOn s) :
    s ×ˢ s =
      (range #s).disjiUnion
        (fun k => s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩)
        (product_self_eq_disjiUnion_perm_aux hf) := by
  ext ⟨a, b⟩
  simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
    Function.Embedding.coeFn_mk, Prod.mk_inj, exists_prop]
  refine ⟨fun hx => ?_, ?_⟩
  · obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
    exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩
  · rintro ⟨n, -, a, ha, rfl, rfl⟩
    exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩

Disjoint Union Decomposition of $s \times s$ for Cycle Permutations

Informal description

Let $f$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$. Then the Cartesian product $s \times s$ can be expressed as the disjoint union over $k \in \{0, \ldots, \#s - 1\}$ of the images of $s$ under the maps $i \mapsto (i, f^k(i))$.

Finset.sum_smul_sum_eq_sum_perm theorem

 (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
  (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Full source

theorem sum_smul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
    (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i) := by
  rw [sum_smul_sum, ← sum_product']
  simp_rw [product_self_eq_disjiUnion_perm hσ, sum_disjiUnion, sum_map, Embedding.coeFn_mk]

Sum-Scalar Product Identity for Cycle Permutations

Informal description

Let $\sigma$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$. For any functions $f \colon \iota \to \alpha$ and $g \colon \iota \to \beta$, the scalar product of the sums of $f$ and $g$ over $s$ equals the sum over $k \in \{0, \ldots, \#s - 1\}$ of the sums of $f(i) \smul g(\sigma^k(i))$ for $i \in s$. In symbols: $$ \left(\sum_{i \in s} f(i)\right) \smul \left(\sum_{i \in s} g(i)\right) = \sum_{k \in \{0, \ldots, \#s - 1\}} \sum_{i \in s} f(i) \smul g(\sigma^k(i)). $$

Finset.sum_mul_sum_eq_sum_perm theorem

 (hσ : σ.IsCycleOn s) (f g : ι → α) : ((∑ i ∈ s, f i) * ∑ i ∈ s, g i) = ∑ k ∈ range #s, ∑ i ∈ s, f i * g ((σ ^ k) i)

Full source

theorem sum_mul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f g : ι → α) :
    ((∑ i ∈ s, f i) * ∑ i ∈ s, g i) = ∑ k ∈ range #s, ∑ i ∈ s, f i * g ((σ ^ k) i) :=
  sum_smul_sum_eq_sum_perm hσ f g

Product of Sums Identity for Cycle Permutations

Informal description

Let $\sigma$ be a permutation of a type $\alpha$ that is a cycle on a finite set $s \subseteq \alpha$. For any functions $f, g \colon \iota \to \alpha$, the product of the sums of $f$ and $g$ over $s$ equals the sum over $k \in \{0, \ldots, \#s - 1\}$ of the sums of $f(i) \cdot g(\sigma^k(i))$ for $i \in s$. In symbols: $$ \left(\sum_{i \in s} f(i)\right) \cdot \left(\sum_{i \in s} g(i)\right) = \sum_{k \in \{0, \ldots, \#s - 1\}} \sum_{i \in s} f(i) \cdot g(\sigma^k(i)). $$

Equiv.Perm.subtypePerm_apply_pow_of_mem theorem

 {g : Perm α} {s : Finset α} (hs : ∀ x : α, x ∈ s ↔ g x ∈ s) {n : ℕ} {x : α} (hx : x ∈ s) :
  ((g.subtypePerm hs ^ n) (⟨x, hx⟩ : s) : α) = (g ^ n) x

Full source

theorem subtypePerm_apply_pow_of_mem {g : Perm α} {s : Finset α}
    (hs : ∀ x : α, x ∈ sx ∈ s ↔ g x ∈ s) {n : ℕ} {x : α} (hx : x ∈ s) :
    ((g.subtypePerm hs ^ n) (⟨x, hx⟩ : s) : α) = (g ^ n) x := by
  simp only [subtypePerm_pow, subtypePerm_apply]

Equality of Powers for Restricted Permutation on Invariant Subset

Informal description

Let $g$ be a permutation of a type $\alpha$, and let $s$ be a finite subset of $\alpha$ that is invariant under $g$ (i.e., $x \in s$ if and only if $g(x) \in s$). For any natural number $n$ and any $x \in s$, the $n$-th power of the restricted permutation $g_{|s}$ applied to $x$ equals the $n$-th power of $g$ applied to $x$. In symbols: $$(g_{|s}^n)(x) = g^n(x).$$

Equiv.Perm.subtypePerm_apply_zpow_of_mem theorem

 {g : Perm α} {s : Finset α} (hs : ∀ x : α, x ∈ s ↔ g x ∈ s) {i : ℤ} {x : α} (hx : x ∈ s) :
  ((g.subtypePerm hs ^ i) (⟨x, hx⟩ : s) : α) = (g ^ i) x

Full source

theorem subtypePerm_apply_zpow_of_mem {g : Perm α} {s : Finset α}
    (hs : ∀ x : α, x ∈ sx ∈ s ↔ g x ∈ s) {i : ℤ} {x : α} (hx : x ∈ s) :
    ((g.subtypePerm hs ^ i) (⟨x, hx⟩ : s) : α) = (g ^ i) x := by
  simp only [subtypePerm_zpow, subtypePerm_apply]

Equality of Powers for Restricted Permutation and Original Permutation on Invariant Subset

Informal description

Let $g$ be a permutation of a type $\alpha$, and let $s$ be a finite subset of $\alpha$ such that for any $x \in \alpha$, $x \in s$ if and only if $g(x) \in s$. For any integer $i$ and any $x \in s$, the $i$-th power of the restricted permutation $g_{|s}$ applied to $x$ (viewed as an element of $s$) equals the $i$-th power of $g$ applied to $x$ (viewed as an element of $\alpha$). In symbols: $$(g_{|s}^i)(x) = g^i(x).$$

Equiv.Perm.subtypePermOfSupport definition

(c : Perm α) : Perm c.support

Full source

/-- Restrict a permutation to its support -/
def subtypePermOfSupport (c : Perm α) : Perm c.support :=
  subtypePerm c fun _ : α => apply_mem_support.symm

Restriction of a permutation to its support

Informal description

Given a permutation `c` of a type `α`, the function `subtypePermOfSupport` restricts `c` to its support, i.e., the set of elements that are not fixed by `c`. This yields a permutation on the subtype consisting of those elements.

Equiv.Perm.subtypePerm_of_support_le definition

(c : Perm α) {s : Finset α} (hcs : c.support ⊆ s) : Equiv.Perm s

Full source

/-- Restrict a permutation to a Finset containing its support -/
def subtypePerm_of_support_le (c : Perm α) {s : Finset α}
    (hcs : c.support ⊆ s) : Equiv.Perm s :=
  subtypePerm c (isInvariant_of_support_le hcs)

Restriction of a permutation to a finite superset of its support

Informal description

Given a permutation `c` of a type `α` and a finite subset `s` of `α` containing the support of `c` (i.e., all elements moved by `c`), this defines the restriction of `c` to `s` as a permutation of `s`.

Equiv.Perm.IsCycle.nonempty_support theorem

{g : Perm α} (hg : g.IsCycle) : g.support.Nonempty

Full source

/-- Support of a cycle is nonempty -/
theorem IsCycle.nonempty_support {g : Perm α} (hg : g.IsCycle) :
    g.support.Nonempty := by
  rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty_iff]
  exact IsCycle.ne_one hg

Nonempty Support of a Cycle Permutation

Informal description

For any cycle permutation $g$ of a type $\alpha$, the support of $g$ (the set of elements not fixed by $g$) is nonempty.

Equiv.Perm.IsCycle.commute_iff' theorem

 {g c : Perm α} (hc : c.IsCycle) :
  Commute g c ↔
    ∃ hc' : ∀ x : α, x ∈ c.support ↔ g x ∈ c.support, subtypePerm g hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Full source

/-- Centralizer of a cycle is a power of that cycle on the cycle -/
theorem IsCycle.commute_iff' {g c : Perm α} (hc : c.IsCycle) :
    CommuteCommute g c ↔
      ∃ hc' : ∀ x : α, x ∈ c.support ↔ g x ∈ c.support,
        subtypePerm g hc' ∈ Subgroup.zpowers c.subtypePermOfSupport := by
  constructor
  · intro hgc
    have hgc' := mem_support_iff_of_commute hgc
    use hgc'
    obtain ⟨a, ha⟩ := IsCycle.nonempty_support hc
    obtain ⟨i, hi⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mp ha))
    use i
    ext ⟨x, hx⟩
    simp only [subtypePermOfSupport, Subtype.coe_mk, subtypePerm_apply]
    rw [subtypePerm_apply_zpow_of_mem]
    obtain ⟨j, rfl⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
    simp only [← mul_apply, Commute.eq (Commute.zpow_right hgc j)]
    rw [← zpow_add, add_comm i j, zpow_add]
    simp only [mul_apply, EmbeddingLike.apply_eq_iff_eq]
    exact hi
  · rintro ⟨hc', ⟨i, hi⟩⟩
    ext x
    simp only [coe_mul, Function.comp_apply]
    by_cases hx : x ∈ c.support
    · suffices hi' : ∀ x ∈ c.support, g x = (c ^ i) x by
        rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
        simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]
      intro x hx
      have hix := Perm.congr_fun hi ⟨x, hx⟩
      simp only [← Subtype.coe_inj, subtypePermOfSupport, Subtype.coe_mk, subtypePerm_apply,
        subtypePerm_apply_zpow_of_mem] at hix
      exact hix.symm
    · rw [not_mem_support.mp hx, eq_comm, ← not_mem_support]
      contrapose! hx
      exact (hc' x).mpr hx

Characterization of Commuting Permutations for a Cycle: $g$ Commutes with Cycle $c$ iff $g$ Preserves Support and is a Power of $c$ on Support

Informal description

Let $g$ and $c$ be permutations of a type $\alpha$, with $c$ being a cycle. Then $g$ commutes with $c$ if and only if there exists a condition $hc'$ stating that for any $x \in \alpha$, $x$ is in the support of $c$ if and only if $g(x)$ is in the support of $c$, and the restriction of $g$ to the support of $c$ (under condition $hc'$) is an integer power of the restriction of $c$ to its own support.

Equiv.Perm.IsCycle.commute_iff theorem

 {g c : Perm α} (hc : c.IsCycle) :
  Commute g c ↔ ∃ hc' : ∀ x : α, x ∈ c.support ↔ g x ∈ c.support, ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c

Full source

/-- A permutation `g` commutes with a cycle `c` if and only if
  `c.support` is invariant under `g`, and `g` acts on it as a power of `c`. -/
theorem IsCycle.commute_iff {g c : Perm α} (hc : c.IsCycle) :
    CommuteCommute g c ↔
      ∃ hc' : ∀ x : α, x ∈ c.support ↔ g x ∈ c.support,
        ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c := by
  simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]
  refine exists_congr fun hc' => exists_congr fun k => ?_
  rw [subtypePermOfSupport, subtypePerm_zpow c k]
  simp only [Perm.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
  apply forall_congr'
  intro a
  by_cases ha : a ∈ c.support
  · rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]
  · rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← not_mem_support]
    · exact Finset.not_mem_mono (support_zpow_le c k) ha
    · exact ha

Characterization of Commuting Permutations for a Cycle: $g$ Commutes with $c$ iff $g$ Preserves Support and is a Power of $c$

Informal description

Let $g$ and $c$ be permutations of a type $\alpha$, with $c$ being a cycle. Then $g$ commutes with $c$ if and only if there exists a condition $hc'$ stating that for any $x \in \alpha$, $x$ is in the support of $c$ if and only if $g(x)$ is in the support of $c$, and the permutation obtained by lifting the restriction of $g$ to the support of $c$ (under condition $hc'$) is an integer power of $c$.

Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff theorem

 {g c : Equiv.Perm α} {s : Finset α} (hg : ∀ x, x ∈ s ↔ g x ∈ s) (hc : c.support ⊆ s) (n : ℤ) :
  c ^ n = ofSubtype (g.subtypePerm hg) ↔ c.subtypePerm (isInvariant_of_support_le hc) ^ n = g.subtypePerm hg

Full source

theorem zpow_eq_ofSubtype_subtypePerm_iff
    {g c : Equiv.Perm α} {s : Finset α}
    (hg : ∀ x, x ∈ sx ∈ s ↔ g x ∈ s) (hc : c.support ⊆ s) (n : ℤ) :
    c ^ n = ofSubtype (g.subtypePerm hg) ↔
      c.subtypePerm (isInvariant_of_support_le hc) ^ n = g.subtypePerm hg := by
  constructor
  · intro h
    ext ⟨x, hx⟩
    simp only [Perm.congr_fun h x, subtypePerm_apply_zpow_of_mem, Subtype.coe_mk, subtypePerm_apply]
    rw [ofSubtype_apply_of_mem]
    · simp only [Subtype.coe_mk, subtypePerm_apply]
    · exact hx
  · intro h; ext x
    rw [← h]
    by_cases hx : x ∈ s
    · rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
    · rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← not_mem_support]
      exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

Equivalence of Permutation Powers and Their Restrictions on Invariant Subsets

Informal description

Let $g$ and $c$ be permutations of a type $\alpha$, and let $s$ be a finite subset of $\alpha$ such that for every $x \in \alpha$, $x \in s$ if and only if $g(x) \in s$. Suppose further that the support of $c$ is contained in $s$. Then for any integer $n$, the $n$-th power of $c$ equals the permutation obtained by lifting the restriction of $g$ to $s$ if and only if the $n$-th power of the restriction of $c$ to $s$ equals the restriction of $g$ to $s$. In symbols: $$c^n = \text{ofSubtype}(g_{|s}) \leftrightarrow c_{|s}^n = g_{|s}.$$

Equiv.Perm.cycle_zpow_mem_support_iff theorem

{g : Perm α} (hg : g.IsCycle) {n : ℤ} {x : α} (hx : g x ≠ x) : (g ^ n) x = x ↔ n % #g.support = 0

Full source

theorem cycle_zpow_mem_support_iff {g : Perm α}
    (hg : g.IsCycle) {n : ℤ} {x : α} (hx : g x ≠ x) :
    (g ^ n) x = x ↔ n % #g.support = 0 := by
  set q := n / #g.support
  set r := n % #g.support
  have div_euc : r + #g.support * q = n ∧ 0 ≤ r ∧ r < #g.support := by
    rw [← Int.ediv_emod_unique _]
    · exact ⟨rfl, rfl⟩
    simp only [Int.natCast_pos]
    apply lt_of_lt_of_le _ (IsCycle.two_le_card_support hg); norm_num
  simp only [← hg.orderOf] at div_euc
  obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le div_euc.2.1
  simp only [hm, Nat.cast_nonneg, Nat.cast_lt, true_and] at div_euc
  rw [← div_euc.1, zpow_add g]
  simp only [hm, Nat.cast_eq_zero, zpow_natCast, coe_mul, comp_apply,zpow_mul,
    pow_orderOf_eq_one, one_zpow, coe_one, id_eq]
  have : (g ^ m) x = x ↔ g ^ m = 1 := by
    constructor
    · intro hgm
      simp only [IsCycle.pow_eq_one_iff hg]
      use x
    · intro hgm
      simp only [hgm, coe_one, id_eq]
  rw [this]
  by_cases hm0 : m = 0
  · simp only [hm0, pow_zero, Nat.cast_zero]
  · simp only [Nat.cast_eq_zero, hm0, iff_false]
    exact pow_ne_one_of_lt_orderOf hm0 div_euc.2

Cycle Permutation Power Fixes Element iff Exponent is Multiple of Support Size

Informal description

Let $g$ be a cycle permutation of a type $\alpha$, and let $x \in \alpha$ be an element not fixed by $g$ (i.e., $g(x) \neq x$). Then for any integer $n$, the permutation $g^n$ fixes $x$ if and only if $n$ is divisible by the cardinality of the support of $g$ (i.e., $n \equiv 0 \pmod{\#\text{supp}(g)}$). In symbols: $$(g^n)(x) = x \leftrightarrow n \equiv 0 \pmod{\#\text{supp}(g)}.$$

Mathlib.GroupTheory.Perm.Cycle.Basic

Main definitions

Notes