Documentation

Mathlib.GroupTheory.Perm.Cycle.Concrete

Properties of cyclic permutations constructed from lists/cycles #

In the following, {α : Type*} [Fintype α] [DecidableEq α].

Main definitions #

Main results #

Implementation details #

The forward direction of Equiv.Perm.isoCycle' uses Fintype.choose of the uniqueness result, relying on the Fintype instance of a Cycle.nodup subtype. It is unclear if this works faster than the Equiv.Perm.toCycle, which relies on recursion over Finset.univ. Running #eval on even a simple noncyclic permutation c[(1 : Fin 7), 2, 3] * c[0, 5] to show it takes a long time. TODO: is this because computing the cycle factors is slow?

theorem List.formPerm_disjoint_iff {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) (hn : 2 l.length) (hn' : 2 l'.length) :
l.formPerm.Disjoint l'.formPerm l.Disjoint l'
theorem List.isCycle_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : l.Nodup) (hn : 2 l.length) :
l.formPerm.IsCycle
theorem List.pairwise_sameCycle_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : l.Nodup) (hn : 2 l.length) :
List.Pairwise l.formPerm.SameCycle l
theorem List.cycleOf_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : l.Nodup) (hn : 2 l.length) (x : { x : α // x l }) :
l.attach.formPerm.cycleOf x = l.attach.formPerm
theorem List.cycleType_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : l.Nodup) (hn : 2 l.length) :
l.attach.formPerm.cycleType = {l.length}
theorem List.formPerm_apply_mem_eq_next {α : Type u_1} [DecidableEq α] {l : List α} (hl : l.Nodup) (x : α) (hx : x l) :
l.formPerm x = l.next x hx
def Cycle.formPerm {α : Type u_1} [DecidableEq α] (s : Cycle α) :
s.NodupEquiv.Perm α

A cycle s : Cycle α, given Nodup s can be interpreted as an Equiv.Perm α where each element in the list is permuted to the next one, defined as formPerm.

Equations
Instances For
    @[simp]
    theorem Cycle.formPerm_coe {α : Type u_1} [DecidableEq α] (l : List α) (hl : l.Nodup) :
    (↑l).formPerm hl = l.formPerm
    theorem Cycle.formPerm_subsingleton {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : s.Subsingleton) :
    s.formPerm = 1
    theorem Cycle.isCycle_formPerm {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : s.Nodup) (hn : s.Nontrivial) :
    (s.formPerm h).IsCycle
    theorem Cycle.support_formPerm {α : Type u_1} [DecidableEq α] [Fintype α] (s : Cycle α) (h : s.Nodup) (hn : s.Nontrivial) :
    (s.formPerm h).support = s.toFinset
    theorem Cycle.formPerm_eq_self_of_not_mem {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : s.Nodup) (x : α) (hx : xs) :
    (s.formPerm h) x = x
    theorem Cycle.formPerm_apply_mem_eq_next {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : s.Nodup) (x : α) (hx : x s) :
    (s.formPerm h) x = s.next h x hx
    theorem Cycle.formPerm_reverse {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : s.Nodup) :
    s.reverse.formPerm = (s.formPerm h)⁻¹
    theorem Cycle.formPerm_eq_formPerm_iff {α : Type u_2} [DecidableEq α] {s : Cycle α} {s' : Cycle α} {hs : s.Nodup} {hs' : s'.Nodup} :
    s.formPerm hs = s'.formPerm hs' s = s' s.Subsingleton s'.Subsingleton
    def Equiv.Perm.toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) :
    List α

    Equiv.Perm.toList (f : Perm α) (x : α) generates the list [x, f x, f (f x), ...] until looping. That means when f x = x, toList f x = [].

    Equations
    Instances For
      @[simp]
      theorem Equiv.Perm.toList_one {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) :
      @[simp]
      theorem Equiv.Perm.toList_eq_nil_iff {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} :
      p.toList x = [] xp.support
      @[simp]
      theorem Equiv.Perm.length_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) :
      (p.toList x).length = (p.cycleOf x).support.card
      theorem Equiv.Perm.toList_ne_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (y : α) :
      p.toList x [y]
      theorem Equiv.Perm.two_le_length_toList_iff_mem_support {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} :
      2 (p.toList x).length x p.support
      theorem Equiv.Perm.length_toList_pos_of_mem_support {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (h : x p.support) :
      0 < (p.toList x).length
      theorem Equiv.Perm.get_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (n : ) (hn : n < (p.toList x).length) :
      (p.toList x).get n, hn = (p ^ n) x
      theorem Equiv.Perm.toList_get_zero {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (h : x p.support) :
      (p.toList x).get 0, = x
      theorem Equiv.Perm.mem_toList_iff {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} {y : α} :
      y p.toList x p.SameCycle x y x p.support
      theorem Equiv.Perm.nodup_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) :
      (p.toList x).Nodup
      theorem Equiv.Perm.next_toList_eq_apply {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (y : α) (hy : y p.toList x) :
      (p.toList x).next y hy = p y
      theorem Equiv.Perm.toList_pow_apply_eq_rotate {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (k : ) :
      p.toList ((p ^ k) x) = (p.toList x).rotate k
      theorem Equiv.Perm.SameCycle.toList_isRotated {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {x : α} {y : α} (h : f.SameCycle x y) :
      f.toList x ~r f.toList y
      theorem Equiv.Perm.pow_apply_mem_toList_iff_mem_support {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} {n : } :
      (p ^ n) x p.toList x x p.support
      theorem Equiv.Perm.toList_formPerm_nil {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) :
      [].formPerm.toList x = []
      theorem Equiv.Perm.toList_formPerm_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) (y : α) :
      [x].formPerm.toList y = []
      theorem Equiv.Perm.toList_formPerm_nontrivial {α : Type u_1} [Fintype α] [DecidableEq α] (l : List α) (hl : 2 l.length) (hn : l.Nodup) :
      l.formPerm.toList (l.get 0, ) = l
      theorem Equiv.Perm.toList_formPerm_isRotated_self {α : Type u_1} [Fintype α] [DecidableEq α] (l : List α) (hl : 2 l.length) (hn : l.Nodup) (x : α) (hx : x l) :
      l.formPerm.toList x ~r l
      theorem Equiv.Perm.formPerm_toList {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (x : α) :
      (f.toList x).formPerm = f.cycleOf x
      def Equiv.Perm.toCycle {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle) :

      Given a cyclic f : Perm α, generate the Cycle α in the order of application of f. Implemented by finding an element x : α in the support of f in Finset.univ, and iterating on using Equiv.Perm.toList f x.

      Equations
      Instances For
        theorem Equiv.Perm.toCycle_eq_toList {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle) (x : α) (hx : f x x) :
        f.toCycle hf = (f.toList x)
        theorem Equiv.Perm.nodup_toCycle {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle) :
        (f.toCycle hf).Nodup
        theorem Equiv.Perm.nontrivial_toCycle {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle) :
        (f.toCycle hf).Nontrivial
        def Equiv.Perm.isoCycle {α : Type u_1} [Fintype α] [DecidableEq α] :
        { f : Equiv.Perm α // f.IsCycle } { s : Cycle α // s.Nodup s.Nontrivial }

        Any cyclic f : Perm α is isomorphic to the nontrivial Cycle α that corresponds to repeated application of f. The forward direction is implemented by Equiv.Perm.toCycle.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Equiv.Perm.IsCycle.existsUnique_cycle {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) :
          ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
          theorem Equiv.Perm.IsCycle.existsUnique_cycle_subtype {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) :
          ∃! s : { s : Cycle α // s.Nodup }, (↑s).formPerm = f
          theorem Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) :
          ∃! s : { s : Cycle α // s.Nodup s.Nontrivial }, (↑s).formPerm = f
          def Equiv.Perm.isoCycle' {α : Type u_1} [Fintype α] [DecidableEq α] :
          { f : Equiv.Perm α // f.IsCycle } { s : Cycle α // s.Nodup s.Nontrivial }

          Any cyclic f : Perm α is isomorphic to the nontrivial Cycle α that corresponds to repeated application of f. The forward direction is implemented by finding this Cycle α using Fintype.choose.

          Equations
          • Equiv.Perm.isoCycle' = { toFun := Fintype.bijInv , invFun := fun (s : { s : Cycle α // s.Nodup s.Nontrivial }) => (↑s).formPerm , , left_inv := , right_inv := }
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              unsafe instance Equiv.Perm.repr_perm {α : Type u_1} [Fintype α] [DecidableEq α] [Repr α] :