Documentation

Mathlib.GroupTheory.Perm.Cycle.Basic

Cyclic permutations #

This file develops the theory of cycles in permutations.

Main definitions #

In the following, f : Equiv.Perm β.

The following two definitions require that β is a Fintype:

Main results #

Notes #

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

SameCycle #

def Equiv.Perm.SameCycle {α : Type u_2} (f : Equiv.Perm α) (x : α) (y : α) :

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

Equations
Instances For
    theorem Equiv.Perm.SameCycle.refl {α : Type u_2} (f : Equiv.Perm α) (x : α) :
    theorem Equiv.Perm.SameCycle.rfl {α : Type u_2} {f : Equiv.Perm α} {x : α} :
    theorem Eq.sameCycle {α : Type u_2} {x : α} {y : α} (h : x = y) (f : Equiv.Perm α) :
    theorem Equiv.Perm.SameCycle.symm {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
    theorem Equiv.Perm.sameCycle_comm {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
    theorem Equiv.Perm.SameCycle.trans {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {z : α} :

    The setoid defined by the SameCycle relation.

    Equations
    Instances For
      @[simp]
      theorem Equiv.Perm.sameCycle_one {α : Type u_2} {x : α} {y : α} :
      @[simp]
      theorem Equiv.Perm.sameCycle_inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      theorem Equiv.Perm.SameCycle.inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :

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

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

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

      @[simp]
      theorem Equiv.Perm.sameCycle_conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} {y : α} :
      theorem Equiv.Perm.SameCycle.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} {y : α} :
      Equiv.Perm.SameCycle f x yEquiv.Perm.SameCycle (g * f * g⁻¹) (g x) (g y)
      theorem Equiv.Perm.SameCycle.apply_eq_self_iff {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      Equiv.Perm.SameCycle f x y(f x = x f y = y)
      theorem Equiv.Perm.SameCycle.eq_of_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hx : Function.IsFixedPt (f) x) :
      x = y
      theorem Equiv.Perm.SameCycle.eq_of_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hy : Function.IsFixedPt (f) y) :
      x = y
      @[simp]
      theorem Equiv.Perm.sameCycle_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      @[simp]
      theorem Equiv.Perm.sameCycle_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      @[simp]
      theorem Equiv.Perm.sameCycle_inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      @[simp]
      theorem Equiv.Perm.sameCycle_inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      @[simp]
      theorem Equiv.Perm.sameCycle_zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      @[simp]
      theorem Equiv.Perm.sameCycle_zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      @[simp]
      theorem Equiv.Perm.sameCycle_pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      @[simp]
      theorem Equiv.Perm.sameCycle_pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      theorem Equiv.Perm.SameCycle.of_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      theorem Equiv.Perm.SameCycle.pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.of_pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.of_pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.of_zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.of_zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :

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

      theorem Equiv.Perm.SameCycle.of_pow {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      theorem Equiv.Perm.SameCycle.of_zpow {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      @[simp]
      theorem Equiv.Perm.sameCycle_subtypePerm {α : Type u_2} {f : Equiv.Perm α} {p : αProp} {h : ∀ (x : α), p x p (f x)} {x : { x : α // p x }} {y : { x : α // p x }} :
      theorem Equiv.Perm.SameCycle.subtypePerm {α : Type u_2} {f : Equiv.Perm α} {p : αProp} {h : ∀ (x : α), p x p (f x)} {x : { x : α // p x }} {y : { x : α // p x }} :

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

      @[simp]
      theorem Equiv.Perm.sameCycle_extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x : α} {y : α} {p : βProp} [DecidablePred p] {f : α Subtype p} :
      theorem Equiv.Perm.SameCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x : α} {y : α} {p : βProp} [DecidablePred p] {f : α Subtype p} :

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

      theorem Equiv.Perm.SameCycle.exists_pow_eq' {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] :
      Equiv.Perm.SameCycle f x y∃ i < orderOf f, (f ^ i) x = y
      theorem Equiv.Perm.SameCycle.exists_pow_eq'' {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] (h : Equiv.Perm.SameCycle f x y) :
      ∃ (i : ), 0 < i i orderOf f (f ^ i) x = y
      Equations
      • One or more equations did not get rendered due to their size.

      IsCycle #

      def Equiv.Perm.IsCycle {α : Type u_2} (f : Equiv.Perm α) :

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

      Equations
      Instances For
        theorem Equiv.Perm.IsCycle.ne_one {α : Type u_2} {f : Equiv.Perm α} (h : Equiv.Perm.IsCycle f) :
        f 1
        theorem Equiv.Perm.IsCycle.sameCycle {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (hf : Equiv.Perm.IsCycle f) (hx : f x x) (hy : f y y) :
        theorem Equiv.Perm.IsCycle.exists_zpow_eq {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
        Equiv.Perm.IsCycle ff x xf y y∃ (i : ), (f ^ i) x = y
        theorem Equiv.Perm.isCycle_iff_sameCycle {α : Type u_2} {f : Equiv.Perm α} {x : α} (hx : f x x) :
        Equiv.Perm.IsCycle f ∀ {y : α}, Equiv.Perm.SameCycle f x y f y y
        theorem Equiv.Perm.IsCycle.exists_pow_eq {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] (hf : Equiv.Perm.IsCycle f) (hx : f x x) (hy : f y y) :
        ∃ (i : ), (f ^ i) x = y
        theorem Equiv.Perm.isCycle_swap {α : Type u_2} {x : α} {y : α} [DecidableEq α] (hxy : x y) :
        noncomputable def Equiv.Perm.IsCycle.zpowersEquivSupport {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) :
        (Subgroup.zpowers σ) { x : α // x Equiv.Perm.support σ }

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Equiv.Perm.IsCycle.zpowersEquivSupport_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) {n : } :
          (Equiv.Perm.IsCycle.zpowersEquivSupport ) { val := σ ^ n, property := (_ : ∃ (y : ), (fun (x : ) => σ ^ x) y = σ ^ n) } = { val := (σ ^ n) (Classical.choose ), property := (_ : (σ ^ n) (Classical.choose ) Equiv.Perm.support σ) }
          @[simp]
          theorem Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) (n : ) :
          (Equiv.Perm.IsCycle.zpowersEquivSupport ).symm { val := (σ ^ n) (Classical.choose ), property := (_ : (σ ^ n) (Classical.choose ) Equiv.Perm.support σ) } = { val := σ ^ n, property := (_ : ∃ (y : ), (fun (x : ) => σ ^ x) y = σ ^ n) }
          theorem Equiv.Perm.isCycle_swap_mul_aux₁ {α : Type u_4} [DecidableEq α] (n : ) {b : α} {x : α} {f : Equiv.Perm α} :
          (Equiv.swap x (f x) * f) b b(f ^ n) (f x) = b∃ (i : ), ((Equiv.swap x (f x) * f) ^ i) (f x) = b
          theorem Equiv.Perm.isCycle_swap_mul_aux₂ {α : Type u_4} [DecidableEq α] (n : ) {b : α} {x : α} {f : Equiv.Perm α} :
          (Equiv.swap x (f x) * f) b b(f ^ n) (f x) = b∃ (i : ), ((Equiv.swap x (f x) * f) ^ i) (f x) = b
          theorem Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self {α : Type u_4} [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) {x : α} (hfx : f x x) (hffx : f (f x) = x) :
          f = Equiv.swap x (f x)
          theorem Equiv.Perm.IsCycle.swap_mul {α : Type u_4} [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) {x : α} (hx : f x x) (hffx : f (f x) x) :
          theorem Equiv.Perm.IsCycle.sign {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) :
          Equiv.Perm.sign f = -(-1) ^ (Equiv.Perm.support f).card
          theorem Equiv.Perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : List (Equiv.Perm β)} (h1 : fl, Equiv.Perm.IsCycle f) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
          theorem Equiv.Perm.IsCycle.support_congr {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) (hg : Equiv.Perm.IsCycle g) (h : Equiv.Perm.support f Equiv.Perm.support g) (h' : xEquiv.Perm.support f, f x = g x) :
          f = g

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

          theorem Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} [DecidableEq α] [Fintype α] (hf : Equiv.Perm.IsCycle f) (hg : Equiv.Perm.IsCycle g) (h : xEquiv.Perm.support f Equiv.Perm.support g, f x = g x) (hx : f x = g x) (hx' : x Equiv.Perm.support f) :
          f = g

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

          theorem Equiv.Perm.IsCycle.pow_eq_one_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : } :
          f ^ n = 1 ∃ (x : β), f x x (f ^ n) x = x
          theorem Equiv.Perm.IsCycle.pow_eq_one_iff' {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : } {x : β} (hx : f x x) :
          f ^ n = 1 (f ^ n) x = x
          theorem Equiv.Perm.IsCycle.pow_eq_one_iff'' {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {n : } :
          f ^ n = 1 ∀ (x : β), f x x(f ^ n) x = x
          theorem Equiv.Perm.IsCycle.pow_eq_pow_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) {a : } {b : } :
          f ^ a = f ^ b ∃ (x : β), f x x (f ^ a) x = (f ^ b) x
          theorem Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : Equiv.Perm.IsCycle f) (hf' : Nat.Prime (orderOf f)) (n : ) (hn : 0 < n) (hn' : n < orderOf f) :

          IsCycleOn #

          def Equiv.Perm.IsCycleOn {α : Type u_2} (f : Equiv.Perm α) (s : Set α) :

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

          Equations
          Instances For

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

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

            @[simp]
            theorem Equiv.Perm.isCycleOn_singleton {α : Type u_2} {f : Equiv.Perm α} {a : α} :

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

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

            theorem Equiv.Perm.IsCycleOn.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {s : Set α} (h : Equiv.Perm.IsCycleOn f s) :
            Equiv.Perm.IsCycleOn (g * f * g⁻¹) (g '' s)
            theorem Equiv.Perm.isCycleOn_swap {α : Type u_2} {a : α} {b : α} [DecidableEq α] (hab : a b) :
            theorem Equiv.Perm.IsCycleOn.apply_ne {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (hf : Equiv.Perm.IsCycleOn f s) (hs : Set.Nontrivial s) (ha : a s) :
            f a a
            theorem Equiv.Perm.IsCycle.isCycleOn {α : Type u_2} {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) :
            Equiv.Perm.IsCycleOn f {x : α | f x x}
            theorem Equiv.Perm.isCycle_iff_exists_isCycleOn {α : Type u_2} {f : Equiv.Perm α} :
            Equiv.Perm.IsCycle f ∃ (s : Set α), Set.Nontrivial s Equiv.Perm.IsCycleOn f s ∀ ⦃x : α⦄, ¬Function.IsFixedPt (f) xx s

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

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

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

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

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

            theorem Equiv.Perm.IsCycleOn.pow_apply_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) {n : } :
            (f ^ n) a = a s.card n
            theorem Equiv.Perm.IsCycleOn.zpow_apply_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) {n : } :
            (f ^ n) a = a s.card n
            theorem Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) {m : } {n : } :
            (f ^ m) a = (f ^ n) a m n [MOD s.card]
            theorem Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) {m : } {n : } :
            (f ^ m) a = (f ^ n) a m n [ZMOD s.card]
            theorem Equiv.Perm.IsCycleOn.pow_card_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) :
            (f ^ s.card) a = a
            theorem Equiv.Perm.IsCycleOn.exists_pow_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {b : α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) (hb : b s) :
            ∃ n < s.card, (f ^ n) a = b
            theorem Equiv.Perm.IsCycleOn.exists_pow_eq' {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} {b : α} (hs : Set.Finite s) (hf : Equiv.Perm.IsCycleOn f s) (ha : a s) (hb : b s) :
            ∃ (n : ), (f ^ n) a = b
            theorem Equiv.Perm.IsCycleOn.range_pow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (hs : Set.Finite s) (h : Equiv.Perm.IsCycleOn f s) (ha : a s) :
            (Set.range fun (n : ) => (f ^ n) a) = s
            theorem Equiv.Perm.IsCycleOn.range_zpow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (h : Equiv.Perm.IsCycleOn f s) (ha : a s) :
            (Set.range fun (n : ) => (f ^ n) a) = s
            theorem Equiv.Perm.IsCycleOn.of_pow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : } (hf : Equiv.Perm.IsCycleOn (f ^ n) s) (h : Set.BijOn (f) s s) :
            theorem Equiv.Perm.IsCycleOn.of_zpow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : } (hf : Equiv.Perm.IsCycleOn (f ^ n) s) (h : Set.BijOn (f) s s) :
            theorem Equiv.Perm.IsCycleOn.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {s : Set α} {p : βProp} [DecidablePred p] (f : α Subtype p) (h : Equiv.Perm.IsCycleOn g s) :

            cycleOf #

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

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

            Equations
            Instances For
              theorem Equiv.Perm.cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (y : α) :
              (Equiv.Perm.cycleOf f x) y = if Equiv.Perm.SameCycle f x y then f y else y
              @[simp]
              theorem Equiv.Perm.cycleOf_pow_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (n : ) :
              (Equiv.Perm.cycleOf f x ^ n) x = (f ^ n) x
              @[simp]
              theorem Equiv.Perm.cycleOf_zpow_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (n : ) :
              (Equiv.Perm.cycleOf f x ^ n) x = (f ^ n) x
              theorem Equiv.Perm.SameCycle.cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} :
              theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} :
              theorem Equiv.Perm.SameCycle.cycleOf_eq {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) :
              @[simp]
              theorem Equiv.Perm.cycleOf_apply_apply_zpow_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (k : ) :
              (Equiv.Perm.cycleOf f x) ((f ^ k) x) = (f ^ (k + 1)) x
              @[simp]
              theorem Equiv.Perm.cycleOf_apply_apply_pow_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (k : ) :
              (Equiv.Perm.cycleOf f x) ((f ^ k) x) = (f ^ (k + 1)) x
              @[simp]
              theorem Equiv.Perm.cycleOf_apply_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) :
              (Equiv.Perm.cycleOf f x) (f x) = f (f x)
              @[simp]
              theorem Equiv.Perm.cycleOf_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) :
              (Equiv.Perm.cycleOf f x) x = f x
              theorem Equiv.Perm.IsCycle.cycleOf_eq {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hf : Equiv.Perm.IsCycle f) (hx : f x x) :
              @[simp]
              theorem Equiv.Perm.cycleOf_eq_one_iff {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) :
              @[simp]
              theorem Equiv.Perm.cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) :
              @[simp]
              theorem Equiv.Perm.cycleOf_self_apply_pow {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ) (x : α) :
              @[simp]
              theorem Equiv.Perm.cycleOf_self_apply_zpow {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ) (x : α) :
              theorem Equiv.Perm.IsCycle.cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hf : Equiv.Perm.IsCycle f) :
              Equiv.Perm.cycleOf f x = if f x = x then 1 else f
              theorem Equiv.Perm.cycleOf_one {α : Type u_2} [DecidableEq α] [Fintype α] (x : α) :
              theorem Equiv.Perm.isCycle_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) (hx : f x x) :
              @[simp]
              @[simp]
              theorem Equiv.Perm.card_support_cycleOf_pos_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} :
              theorem Equiv.Perm.pow_mod_orderOf_cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ) (x : α) :
              (f ^ (n % orderOf (Equiv.Perm.cycleOf f x))) x = (f ^ n) x
              theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Commute f g) (x : α) (hx : g x = x) :
              theorem Equiv.Perm.mem_support_cycleOf_iff' {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (hx : f x x) :
              theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ) (x : α) :
              (f ^ (n % (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card)) x = (f ^ n) x

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

              theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hx : x Equiv.Perm.support f) :
              ∃ i < (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card, (f ^ i) x = y
              theorem Equiv.Perm.SameCycle.exists_pow_eq {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} {y : α} (f : Equiv.Perm α) (h : Equiv.Perm.SameCycle f x y) :
              ∃ (i : ), 0 < i i (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card + 1 (f ^ i) x = y

              cycleFactors #

              def Equiv.Perm.cycleFactorsAux {α : Type u_2} [DecidableEq α] [Fintype α] (l : List α) (f : Equiv.Perm α) :
              (∀ {x : α}, f x xx l){ l : List (Equiv.Perm α) // List.prod l = f (gl, Equiv.Perm.IsCycle g) List.Pairwise Equiv.Perm.Disjoint l }

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

              Equations
              Instances For
                theorem Equiv.Perm.mem_list_cycles_iff {α : Type u_4} [Finite α] {l : List (Equiv.Perm α)} (h1 : σl, Equiv.Perm.IsCycle σ) (h2 : List.Pairwise Equiv.Perm.Disjoint l) {σ : Equiv.Perm α} :
                σ l Equiv.Perm.IsCycle σ ∀ (a : α), σ a aσ a = (List.prod l) a
                theorem Equiv.Perm.list_cycles_perm_list_cycles {α : Type u_4} [Finite α] {l₁ : List (Equiv.Perm α)} {l₂ : List (Equiv.Perm α)} (h₀ : List.prod l₁ = List.prod l₂) (h₁l₁ : σl₁, Equiv.Perm.IsCycle σ) (h₁l₂ : σl₂, Equiv.Perm.IsCycle σ) (h₂l₁ : List.Pairwise Equiv.Perm.Disjoint l₁) (h₂l₂ : List.Pairwise Equiv.Perm.Disjoint l₂) :
                List.Perm l₁ l₂
                def Equiv.Perm.cycleFactors {α : Type u_2} [DecidableEq α] [Fintype α] [LinearOrder α] (f : Equiv.Perm α) :
                { l : List (Equiv.Perm α) // List.prod l = f (gl, Equiv.Perm.IsCycle g) List.Pairwise Equiv.Perm.Disjoint l }

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Equiv.Perm.truncCycleFactors {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) :
                  Trunc { l : List (Equiv.Perm α) // List.prod l = f (gl, Equiv.Perm.IsCycle g) List.Pairwise Equiv.Perm.Disjoint l }

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

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

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Equiv.Perm.cycleFactorsFinset_eq_finset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {s : Finset (Equiv.Perm α)} :
                      Equiv.Perm.cycleFactorsFinset σ = s (fs, Equiv.Perm.IsCycle f) ∃ (h : Set.Pairwise (s) Equiv.Perm.Disjoint), Finset.noncommProd s id (_ : Set.Pairwise s fun (a b : Equiv.Perm α) => Commute (id a) (id b)) = σ

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

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

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

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

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

                      theorem Equiv.Perm.cycle_induction_on {β : Type u_3} [Finite β] (P : Equiv.Perm βProp) (σ : Equiv.Perm β) (base_one : P 1) (base_cycles : ∀ (σ : Equiv.Perm β), Equiv.Perm.IsCycle σP σ) (induction_disjoint : ∀ (σ τ : Equiv.Perm β), Equiv.Perm.Disjoint σ τEquiv.Perm.IsCycle σP σP τP (σ * τ)) :
                      P σ
                      theorem Equiv.Perm.closure_cycle_coprime_swap {α : Type u_2} [DecidableEq α] [Fintype α] {n : } {σ : Equiv.Perm α} (h0 : Nat.Coprime n (Fintype.card α)) (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = Finset.univ) (x : α) :
                      Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} =
                      theorem Equiv.Perm.closure_prime_cycle_swap {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h0 : Nat.Prime (Fintype.card α)) (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = Finset.univ) (h3 : Equiv.Perm.IsSwap τ) :
                      theorem Equiv.Perm.isConj_of_support_equiv {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (f : { x : α // x (Equiv.Perm.support σ) } { x : α // x (Equiv.Perm.support τ) }) (hf : ∀ (x : α) (hx : x (Equiv.Perm.support σ)), (f { val := σ x, property := (_ : σ x Equiv.Perm.support σ) }) = τ (f { val := x, property := hx })) :
                      IsConj σ τ
                      theorem Equiv.Perm.IsCycle.isConj {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) (hτ : Equiv.Perm.IsCycle τ) (h : (Equiv.Perm.support σ).card = (Equiv.Perm.support τ).card) :
                      IsConj σ τ
                      theorem Equiv.Perm.IsCycle.isConj_iff {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : Equiv.Perm.IsCycle σ) (hτ : Equiv.Perm.IsCycle τ) :
                      theorem Equiv.Perm.card_support_conj {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
                      (Equiv.Perm.support (σ * τ * σ⁻¹)).card = (Equiv.Perm.support τ).card
                      theorem Equiv.Perm.Disjoint.isConj_mul {α : Type u_4} [Finite α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} {π : Equiv.Perm α} {ρ : Equiv.Perm α} (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : Equiv.Perm.Disjoint σ τ) (hd2 : Equiv.Perm.Disjoint π ρ) :
                      IsConj (σ * τ) (π * ρ)

                      Fixed points #

                      theorem Equiv.Perm.fixed_point_card_lt_of_ne_one {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (h : σ 1) :
                      (Finset.filter (fun (x : α) => σ x = x) Finset.univ).card < Fintype.card α - 1
                      theorem List.Nodup.isCycleOn_formPerm {α : Type u_2} [DecidableEq α] {l : List α} (h : List.Nodup l) :
                      theorem Finset.exists_cycleOn {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) :
                      theorem Set.Countable.exists_cycleOn {α : Type u_2} [DecidableEq α] {s : Set α} (hs : Set.Countable s) :
                      ∃ (f : Equiv.Perm α), Equiv.Perm.IsCycleOn f s {x : α | f x x} s
                      theorem Set.prod_self_eq_iUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : Equiv.Perm.IsCycleOn f s) :
                      s ×ˢ s = ⋃ (n : ), (fun (a : α) => (a, (f ^ n) a)) '' s
                      theorem Finset.product_self_eq_disjiUnion_perm_aux {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) :
                      Set.PairwiseDisjoint (Finset.range s.card) fun (k : ) => Finset.map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := (_ : ∀ (i j : α), (fun (i : α) => (i, (f ^ k) i)) i = (fun (i : α) => (i, (f ^ k) i)) j((fun (i : α) => (i, (f ^ k) i)) i).1 = ((fun (i : α) => (i, (f ^ k) i)) j).1) } s
                      theorem Finset.product_self_eq_disjiUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : Equiv.Perm.IsCycleOn f s) :
                      s ×ˢ s = Finset.disjiUnion (Finset.range s.card) (fun (k : ) => Finset.map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := (_ : ∀ (i j : α), (fun (i : α) => (i, (f ^ k) i)) i = (fun (i : α) => (i, (f ^ k) i)) j((fun (i : α) => (i, (f ^ k) i)) i).1 = ((fun (i : α) => (i, (f ^ k) i)) j).1) } s) (_ : Set.PairwiseDisjoint (Finset.range s.card) fun (k : ) => Finset.map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := (_ : ∀ (i j : α), (fun (i : α) => (i, (f ^ k) i)) i = (fun (i : α) => (i, (f ^ k) i)) j((fun (i : α) => (i, (f ^ k) i)) i).1 = ((fun (i : α) => (i, (f ^ k) i)) j).1) } s)

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

                      01234
                      40123
                      34012
                      23401
                      12340
                      

                      The diagonals are given by the cycle f.

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