Documentation

Mathlib.GroupTheory.Perm.Cycle.Factors

Cycle factors of a permutation #

Let β be a Fintype and f : Equiv.Perm β.

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} [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
      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 = σ

            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 σ