Documentation

Mathlib.GroupTheory.Perm.Cycle.Basic

Cycles of a permutation #

This file starts the theory of cycles in permutations.

Main definitions #

In the following, f : Equiv.Perm β.

Notes #

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

SameCycle #

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

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

Equations
    Instances For
      source
      theorem Equiv.Perm.SameCycle.refl {α : Type u_2} (f : Perm α) (x : α) :
      f.SameCycle x x
      source
      theorem Equiv.Perm.SameCycle.rfl {α : Type u_2} {f : Perm α} {x : α} :
      f.SameCycle x x
      source
      theorem Eq.sameCycle {α : Type u_2} {x y : α} (h : x = y) (f : Equiv.Perm α) :
      f.SameCycle x y
      source
      theorem Equiv.Perm.SameCycle.symm {α : Type u_2} {f : Perm α} {x y : α} :
      f.SameCycle x y → f.SameCycle y x
      source
      theorem Equiv.Perm.sameCycle_comm {α : Type u_2} {f : Perm α} {x y : α} :
      f.SameCycle x y ↔ f.SameCycle y x
      source
      theorem Equiv.Perm.SameCycle.trans {α : Type u_2} {f : Perm α} {x y z : α} :
      f.SameCycle x y → f.SameCycle y z → f.SameCycle x z
      source
      theorem Equiv.Perm.SameCycle.equivalence {α : Type u_2} (f : Perm α) :
      Equivalence f.SameCycle
      source
      def Equiv.Perm.SameCycle.setoid {α : Type u_2} (f : Perm α) :
      Setoid α

      The setoid defined by the SameCycle relation.

      Equations
        Instances For
          source
          @[simp]
          theorem Equiv.Perm.sameCycle_one {α : Type u_2} {x y : α} :
          SameCycle 1 x y ↔ x = y
          source
          @[simp]
          theorem Equiv.Perm.sameCycle_inv {α : Type u_2} {f : Perm α} {x y : α} :
          f⁻¹.SameCycle x y ↔ f.SameCycle x y
          source
          theorem Equiv.Perm.SameCycle.of_inv {α : Type u_2} {f : Perm α} {x y : α} :
          f⁻¹.SameCycle x y → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.inv {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle x y → f⁻¹.SameCycle x y

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

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

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

          source
          theorem Equiv.Perm.SameCycle.of_apply_left {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle (f x) y → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.of_apply_right {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle x (f y) → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.apply_right {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle x y → f.SameCycle x (f y)

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

          source
          theorem Equiv.Perm.SameCycle.inv_apply_left {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle x y → f.SameCycle (f⁻¹ x) y

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

          source
          theorem Equiv.Perm.SameCycle.of_inv_apply_left {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle (f⁻¹ x) y → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.inv_apply_right {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle x y → f.SameCycle x (f⁻¹ y)

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

          source
          theorem Equiv.Perm.SameCycle.of_inv_apply_right {α : Type u_2} {f : Perm α} {x y : α} :
          f.SameCycle x (f⁻¹ y) → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.of_pow_left {α : Type u_2} {f : Perm α} {x y : α} {n : ℕ} :
          f.SameCycle ((f ^ n) x) y → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.pow_left {α : Type u_2} {f : Perm α} {x y : α} {n : ℕ} :
          f.SameCycle x y → f.SameCycle ((f ^ n) x) y

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

          source
          theorem Equiv.Perm.SameCycle.of_pow_right {α : Type u_2} {f : Perm α} {x y : α} {n : ℕ} :
          f.SameCycle x ((f ^ n) y) → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.pow_right {α : Type u_2} {f : Perm α} {x y : α} {n : ℕ} :
          f.SameCycle x y → f.SameCycle x ((f ^ n) y)

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

          source
          theorem Equiv.Perm.SameCycle.of_zpow_left {α : Type u_2} {f : Perm α} {x y : α} {n : ℤ} :
          f.SameCycle ((f ^ n) x) y → f.SameCycle x y

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

          source
          theorem Equiv.Perm.SameCycle.zpow_left {α : Type u_2} {f : Perm α} {x y : α} {n : ℤ} :
          f.SameCycle x y → f.SameCycle ((f ^ n) x) y

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

          source
          theorem Equiv.Perm.SameCycle.zpow_right {α : Type u_2} {f : Perm α} {x y : α} {n : ℤ} :
          f.SameCycle x y → f.SameCycle x ((f ^ n) y)

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

          source
          theorem Equiv.Perm.SameCycle.of_zpow_right {α : Type u_2} {f : Perm α} {x y : α} {n : ℤ} :
          f.SameCycle x ((f ^ n) y) → f.SameCycle x y

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

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

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

          source
          @[simp]
          theorem Equiv.Perm.sameCycle_extendDomain {α : Type u_2} {β : Type u_3} {g : Perm α} {x y : α} {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} :
          (g.extendDomain f).SameCycle ↑(f x) ↑(f y) ↔ g.SameCycle x y
          source
          theorem Equiv.Perm.SameCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Perm α} {x y : α} {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} :
          g.SameCycle x y → (g.extendDomain f).SameCycle ↑(f x) ↑(f y)

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

          source
          theorem Equiv.Perm.SameCycle.exists_pow_eq' {α : Type u_2} {f : Perm α} {x y : α} [Finite α] :
          f.SameCycle x y → ∃ i < orderOf f, (f ^ i) x = y
          source
          theorem Equiv.Perm.SameCycle.exists_pow_eq'' {α : Type u_2} {f : Perm α} {x y : α} [Finite α] (h : f.SameCycle x y) :
          ∃ (i : ℕ), 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y
          source
          theorem Equiv.Perm.SameCycle.exists_fin_pow_eq {α : Type u_2} {f : Perm α} {x y : α} [Finite α] (h : f.SameCycle x y) :
          ∃ (i : Fin (orderOf f)), (f ^ ↑i) x = y
          source
          theorem Equiv.Perm.SameCycle.exists_nat_pow_eq {α : Type u_2} {f : Perm α} {x y : α} [Finite α] (h : f.SameCycle x y) :
          ∃ (i : ℕ), (f ^ i) x = y
          source
          instance Equiv.Perm.instDecidableRelSameCycleInv {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] :
          DecidableRel f⁻¹.SameCycle
          Equations
            source
            @[instance 100]
            instance Equiv.Perm.instDecidableRelSameCycleOfNatOfDecidableEq {α : Type u_2} [DecidableEq α] :
            DecidableRel (SameCycle 1)
            Equations

              IsCycle #

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

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

              Equations
                Instances For
                  source
                  theorem Equiv.Perm.IsCycle.ne_one {α : Type u_2} {f : Perm α} (h : f.IsCycle) :
                  f ≠ 1
                  source
                  @[simp]
                  theorem Equiv.Perm.not_isCycle_one {α : Type u_2} :
                  ¬IsCycle 1
                  source
                  theorem Equiv.Perm.IsCycle.sameCycle {α : Type u_2} {f : Perm α} {x y : α} (hf : f.IsCycle) (hx : f x ≠ x) (hy : f y ≠ y) :
                  f.SameCycle x y
                  source
                  theorem Equiv.Perm.IsCycle.exists_zpow_eq {α : Type u_2} {f : Perm α} {x y : α} :
                  f.IsCycle → f x ≠ x → f y ≠ y → ∃ (i : ℤ), (f ^ i) x = y
                  source
                  theorem Equiv.Perm.IsCycle.inv {α : Type u_2} {f : Perm α} (hf : f.IsCycle) :
                  f⁻¹.IsCycle
                  source
                  @[simp]
                  theorem Equiv.Perm.isCycle_inv {α : Type u_2} {f : Perm α} :
                  f⁻¹.IsCycle ↔ f.IsCycle
                  source
                  theorem Equiv.Perm.IsCycle.conj {α : Type u_2} {f g : Perm α} :
                  f.IsCycle → (g * f * g⁻¹).IsCycle
                  source
                  theorem Equiv.Perm.IsCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Perm α} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
                  g.IsCycle → (g.extendDomain f).IsCycle
                  source
                  theorem Equiv.Perm.isCycle_iff_sameCycle {α : Type u_2} {f : Perm α} {x : α} (hx : f x ≠ x) :
                  f.IsCycle ↔ ∀ {y : α}, f.SameCycle x y ↔ f y ≠ y
                  source
                  theorem Equiv.Perm.IsCycle.exists_pow_eq {α : Type u_2} {f : Perm α} {x y : α} [Finite α] (hf : f.IsCycle) (hx : f x ≠ x) (hy : f y ≠ y) :
                  ∃ (i : ℕ), (f ^ i) x = y
                  source
                  theorem Equiv.Perm.isCycle_swap {α : Type u_2} {x y : α} [DecidableEq α] (hxy : x ≠ y) :
                  (swap x y).IsCycle
                  source
                  theorem Equiv.Perm.IsSwap.isCycle {α : Type u_2} {f : Perm α} [DecidableEq α] :
                  f.IsSwap → f.IsCycle
                  source
                  theorem Equiv.Perm.IsCycle.two_le_card_support {α : Type u_2} {f : Perm α} [DecidableEq α] [Fintype α] (h : f.IsCycle) :
                  2 ≤ f.support.card
                  source
                  noncomputable def Equiv.Perm.IsCycle.zpowersEquivSupport {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Perm α} (hσ : σ.IsCycle) :
                  ↥(Subgroup.zpowers σ) ≃ { x : α // x ∈ σ.support }

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem Equiv.Perm.IsCycle.zpowersEquivSupport_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Perm α} (hσ : σ.IsCycle) {n : ℕ} :
                      hσ.zpowersEquivSupport ⟨σ ^ n, ⋯⟩ = ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩
                      source
                      @[simp]
                      theorem Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Perm α} (hσ : σ.IsCycle) (n : ℕ) :
                      hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩ = ⟨σ ^ n, ⋯⟩
                      source
                      theorem Equiv.Perm.IsCycle.orderOf {α : Type u_2} {f : Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) :
                      orderOf f = f.support.card
                      source
                      theorem Equiv.Perm.isCycle_swap_mul_aux₁ {α : Type u_4} [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
                      source
                      theorem Equiv.Perm.isCycle_swap_mul_aux₂ {α : Type u_4} [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
                      source
                      theorem Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self {α : Type u_4} [DecidableEq α] {f : Perm α} (hf : f.IsCycle) {x : α} (hfx : f x ≠ x) (hffx : f (f x) = x) :
                      f = swap x (f x)
                      source
                      theorem Equiv.Perm.IsCycle.swap_mul {α : Type u_4} [DecidableEq α] {f : Perm α} (hf : f.IsCycle) {x : α} (hx : f x ≠ x) (hffx : f (f x) ≠ x) :
                      (swap x (f x) * f).IsCycle
                      source
                      @[irreducible]
                      theorem Equiv.Perm.IsCycle.sign {α : Type u_2} [DecidableEq α] [Fintype α] {f : Perm α} (hf : f.IsCycle) :
                      Perm.sign f = -(-1) ^ f.support.card
                      source
                      theorem Equiv.Perm.IsCycle.of_pow {α : Type u_2} {f : Perm α} [DecidableEq α] [Fintype α] {n : ℕ} (h1 : (f ^ n).IsCycle) (h2 : f.support ⊆ (f ^ n).support) :
                      f.IsCycle
                      source
                      theorem Equiv.Perm.IsCycle.of_zpow {α : Type u_2} {f : Perm α} [DecidableEq α] [Fintype α] {n : ℤ} (h1 : (f ^ n).IsCycle) (h2 : f.support ⊆ (f ^ n).support) :
                      f.IsCycle
                      source
                      theorem Equiv.Perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : List (Perm β)} (h1 : ∀ f ∈ l, f.IsCycle) (h2 : List.Pairwise Disjoint l) :
                      l.Nodup
                      source
                      theorem Equiv.Perm.IsCycle.support_congr {α : Type u_2} {f g : Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) (hg : g.IsCycle) (h : f.support ⊆ g.support) (h' : ∀ x ∈ f.support, 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.

                      source
                      theorem Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f g : Perm α} {x : α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) (hg : g.IsCycle) (h : ∀ x ∈ f.support ∩ g.support, f x = g x) (hx : f x = g x) (hx' : x ∈ f.support) :
                      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.

                      source
                      theorem Equiv.Perm.IsCycle.support_pow_eq_iff {α : Type u_2} {f : Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) {n : ℕ} :
                      (f ^ n).support = f.support ↔ ¬orderOf f ∣ n
                      source
                      theorem Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf {α : Type u_2} {f : Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) {n : ℕ} (npos : 0 < n) (hn : n < orderOf f) :
                      (f ^ n).support = f.support
                      source
                      theorem Equiv.Perm.IsCycle.pow_iff {β : Type u_3} [Finite β] {f : Perm β} (hf : f.IsCycle) {n : ℕ} :
                      (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
                      source
                      theorem Equiv.Perm.IsCycle.pow_eq_one_iff {β : Type u_3} [Finite β] {f : Perm β} (hf : f.IsCycle) {n : ℕ} :
                      f ^ n = 1 ↔ ∃ (x : β), f x ≠ x ∧ (f ^ n) x = x
                      source
                      theorem Equiv.Perm.IsCycle.pow_eq_one_iff' {β : Type u_3} [Finite β] {f : Perm β} (hf : f.IsCycle) {n : ℕ} {x : β} (hx : f x ≠ x) :
                      f ^ n = 1 ↔ (f ^ n) x = x
                      source
                      theorem Equiv.Perm.IsCycle.pow_eq_one_iff'' {β : Type u_3} [Finite β] {f : Perm β} (hf : f.IsCycle) {n : ℕ} :
                      f ^ n = 1 ↔ ∀ (x : β), f x ≠ x → (f ^ n) x = x
                      source
                      theorem Equiv.Perm.IsCycle.pow_eq_pow_iff {β : Type u_3} [Finite β] {f : Perm β} (hf : f.IsCycle) {a b : ℕ} :
                      f ^ a = f ^ b ↔ ∃ (x : β), f x ≠ x ∧ (f ^ a) x = (f ^ b) x
                      source
                      theorem Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order {β : Type u_3} [Finite β] {f : Perm β} (hf : f.IsCycle) (hf' : Nat.Prime (orderOf f)) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) :
                      (f ^ n).IsCycle
                      source
                      theorem Int.addLeft_one_isCycle :
                      (Equiv.addLeft 1).IsCycle
                      source
                      theorem Int.addRight_one_isCycle :
                      (Equiv.addRight 1).IsCycle
                      source
                      theorem Equiv.Perm.IsCycle.isConj {α : Type u_2} [Fintype α] [DecidableEq α] {σ τ : Perm α} (hσ : σ.IsCycle) (hτ : τ.IsCycle) (h : σ.support.card = τ.support.card) :
                      IsConj σ τ
                      source
                      theorem Equiv.Perm.IsCycle.isConj_iff {α : Type u_2} [Fintype α] [DecidableEq α] {σ τ : Perm α} (hσ : σ.IsCycle) (hτ : τ.IsCycle) :
                      IsConj σ τ ↔ σ.support.card = τ.support.card

                      IsCycleOn #

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

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

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem Equiv.Perm.isCycleOn_empty {α : Type u_2} {f : Perm α} :
                          f.IsCycleOn ∅
                          source
                          @[simp]
                          theorem Equiv.Perm.isCycleOn_one {α : Type u_2} {s : Set α} :
                          IsCycleOn 1 s ↔ s.Subsingleton
                          source
                          theorem Set.Subsingleton.isCycleOn_one {α : Type u_2} {s : Set α} :
                          s.Subsingleton → Equiv.Perm.IsCycleOn 1 s

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

                          source
                          theorem Equiv.Perm.IsCycleOn.subsingleton {α : Type u_2} {s : Set α} :
                          IsCycleOn 1 s → s.Subsingleton

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

                          source
                          @[simp]
                          theorem Equiv.Perm.isCycleOn_singleton {α : Type u_2} {f : Perm α} {a : α} :
                          f.IsCycleOn {a} ↔ f a = a
                          source
                          theorem Equiv.Perm.isCycleOn_of_subsingleton {α : Type u_2} [Subsingleton α] (f : Perm α) (s : Set α) :
                          f.IsCycleOn s
                          source
                          @[simp]
                          theorem Equiv.Perm.isCycleOn_inv {α : Type u_2} {f : Perm α} {s : Set α} :
                          f⁻¹.IsCycleOn s ↔ f.IsCycleOn s
                          source
                          theorem Equiv.Perm.IsCycleOn.of_inv {α : Type u_2} {f : Perm α} {s : Set α} :
                          f⁻¹.IsCycleOn s → f.IsCycleOn s

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

                          source
                          theorem Equiv.Perm.IsCycleOn.inv {α : Type u_2} {f : Perm α} {s : Set α} :
                          f.IsCycleOn s → f⁻¹.IsCycleOn s

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

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

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

                          source
                          theorem Equiv.Perm.IsCycleOn.apply_mem_iff {α : Type u_2} {f : Perm α} {s : Set α} {x : α} (hf : f.IsCycleOn s) :
                          f x ∈ s ↔ x ∈ s
                          source
                          theorem Equiv.Perm.IsCycleOn.isCycle_subtypePerm {α : Type u_2} {f : Perm α} {s : Set α} (hf : f.IsCycleOn s) (hs : s.Nontrivial) :
                          (f.subtypePerm ⋯).IsCycle

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

                          source
                          theorem Equiv.Perm.IsCycleOn.subtypePerm {α : Type u_2} {f : Perm α} {s : Set α} (hf : f.IsCycleOn s) :
                          (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

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

                          source
                          theorem Equiv.Perm.IsCycleOn.pow_apply_eq {α : Type u_2} {f : Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) {n : ℕ} :
                          (f ^ n) a = a ↔ s.card ∣ n
                          source
                          theorem Equiv.Perm.IsCycleOn.zpow_apply_eq {α : Type u_2} {f : Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) {n : ℤ} :
                          (f ^ n) a = a ↔ ↑s.card ∣ n
                          source
                          theorem Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply {α : Type u_2} {f : Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) {m n : ℕ} :
                          (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card]
                          source
                          theorem Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply {α : Type u_2} {f : Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) {m n : ℤ} :
                          (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑s.card]
                          source
                          theorem Equiv.Perm.IsCycleOn.pow_card_apply {α : Type u_2} {f : Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) :
                          (f ^ s.card) a = a
                          source
                          theorem Equiv.Perm.IsCycleOn.exists_pow_eq {α : Type u_2} {f : Perm α} {a b : α} {s : Finset α} (hf : f.IsCycleOn ↑s) (ha : a ∈ s) (hb : b ∈ s) :
                          ∃ n < s.card, (f ^ n) a = b
                          source
                          theorem Equiv.Perm.IsCycleOn.exists_pow_eq' {α : Type u_2} {f : Perm α} {s : Set α} {a b : α} (hs : s.Finite) (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
                          ∃ (n : ℕ), (f ^ n) a = b
                          source
                          theorem Equiv.Perm.IsCycleOn.range_pow {α : Type u_2} {f : Perm α} {s : Set α} {a : α} (hs : s.Finite) (h : f.IsCycleOn s) (ha : a ∈ s) :
                          (Set.range fun (n : ℕ) => (f ^ n) a) = s
                          source
                          theorem Equiv.Perm.IsCycleOn.range_zpow {α : Type u_2} {f : Perm α} {s : Set α} {a : α} (h : f.IsCycleOn s) (ha : a ∈ s) :
                          (Set.range fun (n : ℤ) => (f ^ n) a) = s
                          source
                          theorem Equiv.Perm.IsCycleOn.of_pow {α : Type u_2} {f : Perm α} {s : Set α} {n : ℕ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn (⇑f) s s) :
                          f.IsCycleOn s
                          source
                          theorem Equiv.Perm.IsCycleOn.of_zpow {α : Type u_2} {f : Perm α} {s : Set α} {n : ℤ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn (⇑f) s s) :
                          f.IsCycleOn s
                          source
                          theorem Equiv.Perm.IsCycleOn.extendDomain {α : Type u_2} {β : Type u_3} {g : Perm α} {s : Set α} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (h : g.IsCycleOn s) :
                          (g.extendDomain f).IsCycleOn (Subtype.val ∘ ⇑f '' s)
                          source
                          theorem Equiv.Perm.IsCycleOn.countable {α : Type u_2} {f : Perm α} {s : Set α} (hs : f.IsCycleOn s) :
                          s.Countable
                          source
                          theorem List.Nodup.isCycleOn_formPerm {α : Type u_2} [DecidableEq α] {l : List α} (h : l.Nodup) :
                          l.formPerm.IsCycleOn {a : α | a ∈ l}
                          source
                          theorem Finset.exists_cycleOn {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) :
                          ∃ (f : Equiv.Perm α), f.IsCycleOn ↑s ∧ f.support ⊆ s
                          source
                          theorem Set.Countable.exists_cycleOn {α : Type u_2} {s : Set α} (hs : s.Countable) :
                          ∃ (f : Equiv.Perm α), f.IsCycleOn s ∧ {x : α | f x ≠ x} ⊆ s
                          source
                          theorem Set.prod_self_eq_iUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s) :
                          s ×ˢ s = ⋃ (n : ℤ), (fun (a : α) => (a, (f ^ n) a)) '' s
                          source
                          theorem Finset.product_self_eq_disjiUnion_perm_aux {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn ↑s) :
                          (↑(range s.card)).PairwiseDisjoint fun (k : ℕ) => map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := ⋯ } s
                          source
                          theorem Finset.product_self_eq_disjiUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn ↑s) :
                          s ×ˢ s = (range s.card).disjiUnion (fun (k : ℕ) => map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := ⋯ } s) ⋯

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

                          01234
40123
34012
23401
12340

                          The diagonals are given by the cycle f.

                          source
                          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σ : σ.IsCycleOn ↑s) (f : ι → α) (g : ι → β) :
                          (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range s.card, ∑ i ∈ s, f i • g ((σ ^ k) i)
                          source
                          theorem Finset.sum_mul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} [Semiring α] {s : Finset ι} {σ : Equiv.Perm ι} (hσ : σ.IsCycleOn ↑s) (f g : ι → α) :
                          (∑ i ∈ s, f i) * ∑ i ∈ s, g i = ∑ k ∈ range s.card, ∑ i ∈ s, f i * g ((σ ^ k) i)
                          source
                          theorem Equiv.Perm.subtypePerm_apply_pow_of_mem {α : Type u_2} {g : Perm α} {s : Finset α} (hs : ∀ (x : α), g x ∈ s ↔ x ∈ s) {n : ℕ} {x : α} (hx : x ∈ s) :
                          ↑((g.subtypePerm hs ^ n) ⟨x, hx⟩) = (g ^ n) x
                          source
                          theorem Equiv.Perm.subtypePerm_apply_zpow_of_mem {α : Type u_2} {g : Perm α} {s : Finset α} (hs : ∀ (x : α), g x ∈ s ↔ x ∈ s) {i : ℤ} {x : α} (hx : x ∈ s) :
                          ↑((g.subtypePerm hs ^ i) ⟨x, hx⟩) = (g ^ i) x
                          source
                          def Equiv.Perm.subtypePermOfSupport {α : Type u_2} [Fintype α] [DecidableEq α] (c : Perm α) :
                          Perm { x : α // x ∈ c.support }

                          Restrict a permutation to its support

                          Equations
                            Instances For
                              source
                              def Equiv.Perm.subtypePerm_of_support_le {α : Type u_2} [Fintype α] [DecidableEq α] (c : Perm α) {s : Finset α} (hcs : c.support ⊆ s) :
                              Perm { x : α // x ∈ s }

                              Restrict a permutation to a Finset containing its support

                              Equations
                                Instances For
                                  source
                                  theorem Equiv.Perm.IsCycle.nonempty_support {α : Type u_2} [Fintype α] [DecidableEq α] {g : Perm α} (hg : g.IsCycle) :
                                  g.support.Nonempty

                                  Support of a cycle is nonempty

                                  source
                                  theorem Equiv.Perm.IsCycle.commute_iff' {α : Type u_2} [Fintype α] [DecidableEq α] {g c : Perm α} (hc : c.IsCycle) :
                                  Commute g c ↔ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

                                  Centralizer of a cycle is a power of that cycle on the cycle

                                  source
                                  theorem Equiv.Perm.IsCycle.commute_iff {α : Type u_2} [Fintype α] [DecidableEq α] {g c : Perm α} (hc : c.IsCycle) :
                                  Commute g c ↔ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), ofSubtype (g.subtypePerm hc') ∈ Subgroup.zpowers c

                                  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.

                                  source
                                  theorem Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff {α : Type u_2} [Fintype α] [DecidableEq α] {g c : Perm α} {s : Finset α} (hg : ∀ (x : α), g x ∈ s ↔ x ∈ s) (hc : c.support ⊆ s) (n : ℤ) :
                                  c ^ n = ofSubtype (g.subtypePerm hg) ↔ c.subtypePerm ⋯ ^ n = g.subtypePerm hg
                                  source
                                  theorem Equiv.Perm.cycle_zpow_mem_support_iff {α : Type u_2} [Fintype α] [DecidableEq α] {g : Perm α} (hg : g.IsCycle) {n : ℤ} {x : α} (hx : g x ≠ x) :
                                  (g ^ n) x = x ↔ n % ↑g.support.card = 0