Mathlib.GroupTheory.Perm.Cycle.Type

Equiv.Perm.cycleType definition

(σ : Perm α) : Multiset ℕ

Full source

/-- The cycle type of a permutation -/
def cycleType (σ : Perm α) : Multiset ℕ :=
  σ.cycleFactorsFinset.1.map (Finset.cardFinset.card ∘ support)

Cycle type of a permutation

Informal description

The cycle type of a permutation $\sigma$ of a finite type $\alpha$ is the multiset of natural numbers where each number corresponds to the size of a cycle in the cycle decomposition of $\sigma$. More precisely, for a permutation $\sigma$, its cycle type is obtained by taking the cycle factors of $\sigma$ (as a finset), and mapping each cycle to the cardinality of its support (the set of elements it moves).

Equiv.Perm.cycleType_def theorem

(σ : Perm α) : σ.cycleType = σ.cycleFactorsFinset.1.map (Finset.card ∘ support)

Full source

theorem cycleType_def (σ : Perm α) :
    σ.cycleType = σ.cycleFactorsFinset.1.map (Finset.cardFinset.card ∘ support) :=
  rfl

Definition of Cycle Type via Cycle Decomposition

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the cycle type of $\sigma$ is equal to the multiset obtained by mapping each cycle in the cycle decomposition of $\sigma$ to the cardinality of its support (the set of elements it moves). More precisely, if $\sigma.cycleFactorsFinset$ is the finset of cycles in the cycle decomposition of $\sigma$, then $\sigma.cycleType$ is the multiset formed by applying the function $\text{card} \circ \text{support}$ to each cycle in this finset.

Equiv.Perm.cycleType_eq' theorem

 {σ : Perm α} (s : Finset (Perm α)) (h1 : ∀ f : Perm α, f ∈ s → f.IsCycle) (h2 : (s : Set (Perm α)).Pairwise Disjoint)
  (h0 : s.noncommProd id (h2.imp fun _ _ => Disjoint.commute) = σ) : σ.cycleType = s.1.map (Finset.card ∘ support)

Full source

theorem cycleType_eq' {σ : Perm α} (s : Finset (Perm α)) (h1 : ∀ f : Perm α, f ∈ s → f.IsCycle)
    (h2 : (s : Set (Perm α)).Pairwise Disjoint)
    (h0 : s.noncommProd id (h2.imp fun _ _ => Disjoint.commute) = σ) :
    σ.cycleType = s.1.map (Finset.cardFinset.card ∘ support) := by
  rw [cycleType_def]
  congr
  rw [cycleFactorsFinset_eq_finset]
  exact ⟨h1, h2, h0⟩

Cycle Type via Disjoint Cycle Decomposition

Informal description

Let $\sigma$ be a permutation of a finite type $\alpha$, and let $s$ be a finset of permutations of $\alpha$ such that: 1. Every permutation $f \in s$ is a cycle, 2. The permutations in $s$ are pairwise disjoint, and 3. The noncommutative product of the permutations in $s$ equals $\sigma$. Then the cycle type of $\sigma$ is equal to the multiset obtained by mapping each permutation in $s$ to the cardinality of its support. That is, \[ \text{cycleType}(\sigma) = \text{map} (\text{card} \circ \text{support}) (s.1). \]

Equiv.Perm.cycleType_eq theorem

 {σ : Perm α} (l : List (Perm α)) (h0 : l.prod = σ) (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) :
  σ.cycleType = l.map (Finset.card ∘ support)

Full source

theorem cycleType_eq {σ : Perm α} (l : List (Perm α)) (h0 : l.prod = σ)
    (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) :
    σ.cycleType = l.map (Finset.cardFinset.card ∘ support) := by
  have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
  rw [cycleType_eq' l.toFinset]
  · simp [List.dedup_eq_self.mpr hl, Function.comp_def]
  · simpa using h1
  · simpa [hl] using h2
  · simp [hl, h0]

Cycle Type via List of Disjoint Cycles

Informal description

Let $\sigma$ be a permutation of a finite type $\alpha$, and let $l$ be a list of permutations of $\alpha$ such that: 1. The product of the permutations in $l$ equals $\sigma$, 2. Every permutation in $l$ is a cycle, and 3. The permutations in $l$ are pairwise disjoint. Then the cycle type of $\sigma$ is equal to the list obtained by mapping each permutation in $l$ to the cardinality of its support. That is, \[ \text{cycleType}(\sigma) = \text{map} (\text{card} \circ \text{support}) (l). \]

Equiv.Perm.CycleType.count_def theorem

 {σ : Perm α} (n : ℕ) : σ.cycleType.count n = Fintype.card { c : σ.cycleFactorsFinset // #(c : Perm α).support = n }

Full source

theorem CycleType.count_def {σ : Perm α} (n : ℕ) :
    σ.cycleType.count n =
      Fintype.card {c : σ.cycleFactorsFinset // #(c : Perm α).support = n } := by
  -- work on the LHS
  rw [cycleType, Multiset.count_eq_card_filter_eq]
  -- rewrite the `Fintype.card` as a `Finset.card`
  rw [Fintype.subtype_card, Finset.univ_eq_attach, Finset.filter_attach',
    Finset.card_map, Finset.card_attach]
  simp only [Function.comp_apply, Finset.card, Finset.filter_val,
    Multiset.filter_map, Multiset.card_map]
  congr 1
  apply Multiset.filter_congr
  intro d h
  simp only [Function.comp_apply, eq_comm, Finset.mem_val.mp h, exists_const]

Count in Cycle Type Equals Number of Cycles with Given Support Size

Informal description

For any permutation $\sigma$ of a finite type $\alpha$ and any natural number $n$, the count of $n$ in the cycle type of $\sigma$ equals the cardinality of the set of cycle factors of $\sigma$ whose support has size $n$. That is, \[ \text{count}(n, \sigma.\text{cycleType}) = \#\{ c \in \sigma.\text{cycleFactorsFinset} \mid \#\text{support}(c) = n \}. \]

Equiv.Perm.cycleType_eq_zero theorem

{σ : Perm α} : σ.cycleType = 0 ↔ σ = 1

Full source

@[simp]
theorem cycleType_eq_zero {σ : Perm α} : σ.cycleType = 0 ↔ σ = 1 := by
  simp [cycleType_def, cycleFactorsFinset_eq_empty_iff]

Cycle type is empty if and only if permutation is identity

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the cycle type of $\sigma$ is the empty multiset if and only if $\sigma$ is the identity permutation.

Equiv.Perm.cycleType_one theorem

: (1 : Perm α).cycleType = 0

Full source

@[simp]
theorem cycleType_one : (1 : Perm α).cycleType = 0 := cycleType_eq_zero.2 rfl

Cycle Type of Identity Permutation is Empty

Informal description

The cycle type of the identity permutation on a finite type $\alpha$ is the empty multiset, i.e., $(1 : \text{Perm } \alpha).\text{cycleType} = 0$.

Equiv.Perm.card_cycleType_eq_zero theorem

{σ : Perm α} : Multiset.card σ.cycleType = 0 ↔ σ = 1

Full source

theorem card_cycleType_eq_zero {σ : Perm α} : Multiset.cardMultiset.card σ.cycleType = 0 ↔ σ = 1 := by
  rw [card_eq_zero, cycleType_eq_zero]

Cardinality of Cycle Type is Zero if and Only if Identity Permutation

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the number of cycles in the cycle decomposition of $\sigma$ is zero if and only if $\sigma$ is the identity permutation.

Equiv.Perm.card_cycleType_pos theorem

{σ : Perm α} : 0 < Multiset.card σ.cycleType ↔ σ ≠ 1

Full source

theorem card_cycleType_pos {σ : Perm α} : 0 < Multiset.card σ.cycleType ↔ σ ≠ 1 :=
  pos_iff_ne_zero.trans card_cycleType_eq_zero.not

Positivity of Cycle Count in Non-Identity Permutations

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the number of cycles in the cycle decomposition of $\sigma$ is positive if and only if $\sigma$ is not the identity permutation.

Equiv.Perm.two_le_of_mem_cycleType theorem

{σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 2 ≤ n

Full source

theorem two_le_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 2 ≤ n := by
  simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map,
    mem_cycleFactorsFinset_iff] at h
  obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h
  exact hc.two_le_card_support

Cycle Type Elements Are At Least Two

Informal description

For any permutation $\sigma$ of a finite type $\alpha$ and any natural number $n$ in the cycle type of $\sigma$, we have $2 \leq n$.

Equiv.Perm.one_lt_of_mem_cycleType theorem

{σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 1 < n

Full source

theorem one_lt_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 1 < n :=
  two_le_of_mem_cycleType h

Cycle Type Elements Are Greater Than One

Informal description

For any permutation $\sigma$ of a finite type $\alpha$ and any natural number $n$ in the cycle type of $\sigma$, we have $1 < n$.

Equiv.Perm.IsCycle.cycleType theorem

{σ : Perm α} (hσ : IsCycle σ) : σ.cycleType = {#σ.support}

Full source

theorem IsCycle.cycleType {σ : Perm α} (hσ : IsCycle σ) : σ.cycleType = {#σ.support} :=
  cycleType_eq [σ] (mul_one σ) (fun _τ hτ => (congr_arg IsCycle (List.mem_singleton.mp hτ)).mpr hσ)
    (List.pairwise_singleton Disjoint σ)

Cycle Type of a Cycle Permutation is Singleton of Support Size

Informal description

For a cycle permutation $\sigma$ of a finite type $\alpha$, the cycle type of $\sigma$ is the singleton multiset consisting of the cardinality of its support, i.e., \[ \text{cycleType}(\sigma) = \{\#\text{support}(\sigma)\}. \]

Equiv.Perm.card_cycleType_eq_one theorem

{σ : Perm α} : Multiset.card σ.cycleType = 1 ↔ σ.IsCycle

Full source

theorem card_cycleType_eq_one {σ : Perm α} : Multiset.cardMultiset.card σ.cycleType = 1 ↔ σ.IsCycle := by
  rw [card_eq_one]
  simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
    cycleFactorsFinset_eq_singleton_iff]
  constructor
  · rintro ⟨_, _, ⟨h, -⟩, -⟩
    exact h
  · intro h
    use #σ.support, σ
    simp [h]

Cycle Type Cardinality One iff Permutation is a Cycle

Informal description

For a permutation $\sigma$ of a finite type $\alpha$, the cardinality of its cycle type multiset is equal to 1 if and only if $\sigma$ is a cycle permutation. In other words, $\sigma$ has exactly one non-trivial cycle in its cycle decomposition if and only if it is a cycle permutation.

Equiv.Perm.Disjoint.cycleType theorem

{σ τ : Perm α} (h : Disjoint σ τ) : (σ * τ).cycleType = σ.cycleType + τ.cycleType

Full source

theorem Disjoint.cycleType {σ τ : Perm α} (h : Disjoint σ τ) :
    (σ * τ).cycleType = σ.cycleType + τ.cycleType := by
  rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ←
    Multiset.map_add, Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]
  exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset

Cycle Type Additivity for Disjoint Permutations

Informal description

For any two disjoint permutations $\sigma$ and $\tau$ of a finite type $\alpha$, the cycle type of their composition $\sigma \circ \tau$ is equal to the sum of their individual cycle types. That is, \[ \text{cycleType}(\sigma \circ \tau) = \text{cycleType}(\sigma) + \text{cycleType}(\tau). \]

Equiv.Perm.cycleType_inv theorem

(σ : Perm α) : σ⁻¹.cycleType = σ.cycleType

Full source

@[simp]
theorem cycleType_inv (σ : Perm α) : σ⁻¹.cycleType = σ.cycleType :=
  cycle_induction_on (P := fun τ : Perm α => τ⁻¹.cycleType = τ.cycleType) σ rfl
    (fun σ hσ => by simp only [hσ.cycleType, hσ.inv.cycleType, support_inv])
    fun σ τ hστ _ hσ hτ => by
      simp only [mul_inv_rev, hστ.cycleType, hστ.symm.inv_left.inv_right.cycleType, hσ, hτ,
        add_comm]

Invariance of Cycle Type under Inversion

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the cycle type of its inverse $\sigma^{-1}$ is equal to the cycle type of $\sigma$. That is, \[ \text{cycleType}(\sigma^{-1}) = \text{cycleType}(\sigma). \]

Equiv.Perm.cycleType_conj theorem

{σ τ : Perm α} : (τ * σ * τ⁻¹).cycleType = σ.cycleType

Full source

@[simp]
theorem cycleType_conj {σ τ : Perm α} : (τ * σ * τ⁻¹).cycleType = σ.cycleType := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
  | induction_disjoint σ π hd _ hσ hπ =>
    rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]

Invariance of Cycle Type under Conjugation

Informal description

For any permutations $\sigma$ and $\tau$ of a finite type $\alpha$, the cycle type of the conjugate permutation $\tau \sigma \tau^{-1}$ is equal to the cycle type of $\sigma$. That is, \[ \text{cycleType}(\tau \sigma \tau^{-1}) = \text{cycleType}(\sigma). \]

Equiv.Perm.sum_cycleType theorem

(σ : Perm α) : σ.cycleType.sum = #σ.support

Full source

theorem sum_cycleType (σ : Perm α) : σ.cycleType.sum = #σ.support := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]

Sum of Cycle Type Equals Support Cardinality

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the sum of the cycle type of $\sigma$ equals the cardinality of its support. That is, \[ \sum_{n \in \text{cycleType}(\sigma)} n = \#\text{support}(\sigma). \]

Equiv.Perm.card_fixedPoints theorem

(σ : Equiv.Perm α) : Fintype.card (Function.fixedPoints σ) = Fintype.card α - σ.cycleType.sum

Full source

theorem card_fixedPoints (σ : Equiv.Perm α) :
    Fintype.card (Function.fixedPoints σ) = Fintype.card α - σ.cycleType.sum := by
  rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl, Fintype.card_ofFinset]
  congr; aesop

Cardinality of Fixed Points Equals Total Elements Minus Sum of Cycle Lengths

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the number of fixed points of $\sigma$ is equal to the cardinality of $\alpha$ minus the sum of the cycle type of $\sigma$. That is, \[ \text{card}(\text{FixedPoints}(\sigma)) = \text{card}(\alpha) - \sum_{n \in \text{cycleType}(\sigma)} n. \]

Equiv.Perm.sign_of_cycleType' theorem

(σ : Perm α) : sign σ = (σ.cycleType.map fun n => -(-1 : ℤˣ) ^ n).prod

Full source

theorem sign_of_cycleType' (σ : Perm α) :
    sign σ = (σ.cycleType.map fun n => -(-1 : ℤℤˣ) ^ n).prod := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType]

Sign of Permutation via Cycle Type: $\text{sign}(\sigma) = \prod_{n \in \text{cycleType}(\sigma)} -(-1)^n$

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the sign of $\sigma$ is equal to the product over the cycle type of $\sigma$ of the terms $-(-1)^n$ for each cycle length $n$ in the cycle type. That is, \[ \text{sign}(\sigma) = \prod_{n \in \text{cycleType}(\sigma)} -(-1)^n. \]

Equiv.Perm.sign_of_cycleType theorem

(f : Perm α) : sign f = (-1 : ℤˣ) ^ (f.cycleType.sum + Multiset.card f.cycleType)

Full source

theorem sign_of_cycleType (f : Perm α) :
    sign f = (-1 : ℤℤˣ) ^ (f.cycleType.sum + Multiset.card f.cycleType) := by
  rw [sign_of_cycleType']
  induction' f.cycleType using Multiset.induction_on with a s ihs
  · rfl
  · rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, mul_neg_one, neg_mul, mul_neg, mul_assoc, mul_one]

Sign of Permutation via Cycle Type: $\text{sign}(f) = (-1)^{\sum \text{cycleType}(f) + |\text{cycleType}(f)|}$

Informal description

For any permutation $f$ of a finite type $\alpha$, the sign of $f$ is given by $(-1)^{s + k}$, where $s$ is the sum of the cycle lengths in the cycle type of $f$ and $k$ is the number of cycles in the cycle type. That is, \[ \text{sign}(f) = (-1)^{\sum \text{cycleType}(f) + |\text{cycleType}(f)|}. \]

Equiv.Perm.lcm_cycleType theorem

(σ : Perm α) : σ.cycleType.lcm = orderOf σ

Full source

@[simp]
theorem lcm_cycleType (σ : Perm α) : σ.cycleType.lcm = orderOf σ := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

Least Common Multiple of Cycle Type Equals Permutation Order

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the least common multiple of the cycle lengths in the cycle type of $\sigma$ equals the order of $\sigma$ in the permutation group. That is, \[ \text{lcm}(\text{cycleType}(\sigma)) = \text{orderOf}(\sigma). \]

Equiv.Perm.dvd_of_mem_cycleType theorem

{σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : n ∣ orderOf σ

Full source

theorem dvd_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : n ∣ orderOf σ := by
  rw [← lcm_cycleType]
  exact dvd_lcm h

Cycle Length Divides Permutation Order

Informal description

For any permutation $\sigma$ of a finite type $\alpha$ and any natural number $n$ in the cycle type of $\sigma$, $n$ divides the order of $\sigma$. That is, if $n \in \text{cycleType}(\sigma)$, then $n \mid \text{orderOf}(\sigma)$.

Equiv.Perm.orderOf_cycleOf_dvd_orderOf theorem

(f : Perm α) (x : α) : orderOf (cycleOf f x) ∣ orderOf f

Full source

theorem orderOf_cycleOf_dvd_orderOf (f : Perm α) (x : α) : orderOforderOf (cycleOf f x) ∣ orderOf f := by
  by_cases hx : f x = x
  · rw [← cycleOf_eq_one_iff] at hx
    simp [hx]
  · refine dvd_of_mem_cycleType ?_
    rw [cycleType, Multiset.mem_map]
    refine ⟨f.cycleOf x, ?_, ?_⟩
    · rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
    · simp [(isCycle_cycleOf _ hx).orderOf]

Order of Cycle in Permutation Divides Order of Permutation

Informal description

For any permutation $f$ of a finite type $\alpha$ and any element $x \in \alpha$, the order of the cycle permutation $\text{cycleOf}(f, x)$ divides the order of $f$. That is, $\text{orderOf}(\text{cycleOf}(f, x)) \mid \text{orderOf}(f)$.

Equiv.Perm.two_dvd_card_support theorem

{σ : Perm α} (hσ : σ ^ 2 = 1) : 2 ∣ #σ.support

Full source

theorem two_dvd_card_support {σ : Perm α} (hσ : σ ^ 2 = 1) : 2 ∣ #σ.support :=
  (congr_arg (Dvd.dvd 2) σ.sum_cycleType).mp
    (Multiset.dvd_sum fun n hn => by
      rw [_root_.le_antisymm
          (Nat.le_of_dvd zero_lt_two <|
            (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
          (two_le_of_mem_cycleType hn)])

Even Cardinality of Support for Involutive Permutations

Informal description

For any permutation $\sigma$ of a finite type $\alpha$ such that $\sigma^2 = 1$, the cardinality of the support of $\sigma$ is divisible by 2. That is, $2 \mid \#\text{support}(\sigma)$.

Equiv.Perm.cycleType_prime_order theorem

{σ : Perm α} (hσ : (orderOf σ).Prime) : ∃ n : ℕ, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Full source

theorem cycleType_prime_order {σ : Perm α} (hσ : (orderOf σ).Prime) :
    ∃ n : ℕ, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ) := by
  refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
  · rw [tsub_add_cancel_of_le]
    rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]
    exact hσ.ne_one
  · exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left
      (one_lt_of_mem_cycleType hn).ne'

Cycle Type Structure for Permutations of Prime Order

Informal description

For any permutation $\sigma$ of a finite type $\alpha$ with prime order $p$, there exists a natural number $n$ such that the cycle type of $\sigma$ consists of $n+1$ copies of $p$. In other words, $\sigma$ has $n+1$ cycles, each of length $p$.

Equiv.Perm.pow_prime_eq_one_iff theorem

{σ : Perm α} {p : ℕ} [hp : Fact (Nat.Prime p)] : σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p

Full source

theorem pow_prime_eq_one_iff {σ : Perm α} {p : ℕ} [hp : Fact (Nat.Prime p)] :
    σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p := by
  rw [← orderOf_dvd_iff_pow_eq_one, ← lcm_cycleType, Multiset.lcm_dvd]
  apply forall_congr'
  exact fun c ↦ ⟨fun hc h ↦ Or.resolve_left (hp.elim.eq_one_or_self_of_dvd c (hc h))
       (Nat.ne_of_lt' (one_lt_of_mem_cycleType h)),
     fun hc h ↦ by rw [hc h]⟩

Permutation to Prime Power is Identity if and only if All Cycle Lengths are Prime

Informal description

For a permutation $\sigma$ of a finite type $\alpha$ and a prime number $p$, the permutation $\sigma$ raised to the power $p$ equals the identity permutation if and only if every cycle length in the cycle type of $\sigma$ is equal to $p$. That is, \[ \sigma^p = 1 \leftrightarrow \forall c \in \text{cycleType}(\sigma), c = p. \]

Equiv.Perm.isCycle_of_prime_order theorem

{σ : Perm α} (h1 : (orderOf σ).Prime) (h2 : #σ.support < 2 * orderOf σ) : σ.IsCycle

Full source

theorem isCycle_of_prime_order {σ : Perm α} (h1 : (orderOf σ).Prime)
    (h2 : #σ.support < 2 * orderOf σ) : σ.IsCycle := by
  obtain ⟨n, hn⟩ := cycleType_prime_order h1
  rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id,
    mul_lt_mul_right (orderOf_pos σ), Nat.succ_lt_succ_iff, Nat.lt_succ_iff, Nat.le_zero] at h2
  rw [← card_cycleType_eq_one, hn, card_replicate, h2]

Permutation of Prime Order with Small Support is a Cycle

Informal description

For a permutation $\sigma$ of a finite type $\alpha$, if the order of $\sigma$ is a prime number $p$ and the cardinality of its support is less than $2p$, then $\sigma$ is a cycle permutation.

Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset theorem

{f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) : f.cycleType ≤ g.cycleType

Full source

theorem cycleType_le_of_mem_cycleFactorsFinset {f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) :
    f.cycleType ≤ g.cycleType := by
  have hf' := mem_cycleFactorsFinset_iff.1 hf
  rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]
  refine map_le_map ?_
  simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf

Cycle Type Comparison for Cycle Factors of a Permutation

Informal description

For any permutations $f$ and $g$ of a finite type $\alpha$, if $f$ is a cycle factor of $g$ (i.e., $f \in g.\text{cycleFactorsFinset}$), then the cycle type of $f$ is less than or equal to the cycle type of $g$ in the multiset order.

Equiv.Perm.Disjoint.cycleType_mul theorem

{f g : Perm α} (h : f.Disjoint g) : (f * g).cycleType = f.cycleType + g.cycleType

Full source

theorem Disjoint.cycleType_mul {f g : Perm α} (h : f.Disjoint g) :
    (f * g).cycleType = f.cycleType + g.cycleType := by
  simp only [Perm.cycleType]
  rw [h.cycleFactorsFinset_mul_eq_union]
  simp only [Finset.union_val, Function.comp_apply]
  rw [← Multiset.add_eq_union_iff_disjoint.mpr _, Multiset.map_add]
  simp only [Finset.disjoint_val, Disjoint.disjoint_cycleFactorsFinset h]

Cycle Type Additivity for Disjoint Permutations

Informal description

For any two disjoint permutations $f$ and $g$ of a finite type $\alpha$, the cycle type of their composition $f \circ g$ is equal to the sum of their individual cycle types. That is, $$\text{cycleType}(f \circ g) = \text{cycleType}(f) + \text{cycleType}(g).$$

Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub theorem

{f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) : (g * f⁻¹).cycleType = g.cycleType - f.cycleType

Full source

theorem cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub
    {f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) :
    (g * f⁻¹).cycleType = g.cycleType - f.cycleType :=
  add_right_cancel (b := f.cycleType) <| by
    rw [← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType, inv_mul_cancel_right,
      tsub_add_cancel_of_le (cycleType_le_of_mem_cycleFactorsFinset hf)]

Cycle Type Difference for Permutation Composition with Inverse Cycle Factor

Informal description

For any permutations $f$ and $g$ of a finite type $\alpha$, if $f$ is a cycle factor of $g$ (i.e., $f \in g.\text{cycleFactorsFinset}$), then the cycle type of the composition $g \circ f^{-1}$ is equal to the difference of the cycle types of $g$ and $f$. That is, \[ \text{cycleType}(g \circ f^{-1}) = \text{cycleType}(g) - \text{cycleType}(f). \]

Equiv.Perm.isConj_of_cycleType_eq theorem

{σ τ : Perm α} (h : cycleType σ = cycleType τ) : IsConj σ τ

Full source

theorem isConj_of_cycleType_eq {σ τ : Perm α} (h : cycleType σ = cycleType τ) : IsConj σ τ := by
  induction σ using cycle_induction_on generalizing τ with
  | base_one =>
    rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
    rw [h]
  | base_cycles σ hσ =>
    have hτ := card_cycleType_eq_one.2 hσ
    rw [h, card_cycleType_eq_one] at hτ
    apply hσ.isConj hτ
    rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
  | induction_disjoint σ π hd hc hσ hπ =>
    rw [hd.cycleType] at h
    have h' : #σ.support#σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
    obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
    have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
    refine IsConj.trans ?_ key
    rw [mul_assoc]
    have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
    refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
    · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]
      rwa [Finset.mem_def]
    · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm

Conjugacy of Permutations with Equal Cycle Types

Informal description

For any two permutations $\sigma$ and $\tau$ of a finite type $\alpha$, if their cycle types are equal, then $\sigma$ and $\tau$ are conjugate in the symmetric group on $\alpha$.

Equiv.Perm.isConj_iff_cycleType_eq theorem

{σ τ : Perm α} : IsConj σ τ ↔ σ.cycleType = τ.cycleType

Full source

theorem isConj_iff_cycleType_eq {σ τ : Perm α} : IsConjIsConj σ τ ↔ σ.cycleType = τ.cycleType :=
  ⟨fun h => by
    obtain ⟨π, rfl⟩ := isConj_iff.1 h
    rw [cycleType_conj], isConj_of_cycleType_eq⟩

Conjugacy Criterion via Cycle Type Equality

Informal description

Two permutations $\sigma$ and $\tau$ of a finite type $\alpha$ are conjugate if and only if their cycle types are equal, i.e., $\text{IsConj}(\sigma, \tau) \leftrightarrow \text{cycleType}(\sigma) = \text{cycleType}(\tau)$.

Equiv.Perm.cycleType_extendDomain theorem

 {β : Type*} [Fintype β] [DecidableEq β] {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) {g : Perm α} :
  cycleType (g.extendDomain f) = cycleType g

Full source

@[simp]
theorem cycleType_extendDomain {β : Type*} [Fintype β] [DecidableEq β] {p : β → Prop}
    [DecidablePred p] (f : α ≃ Subtype p) {g : Perm α} :
    cycleType (g.extendDomain f) = cycleType g := by
  induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ =>
    rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]

Invariance of Cycle Type Under Permutation Extension

Informal description

Let $\alpha$ and $\beta$ be finite types with decidable equality, and let $p$ be a decidable predicate on $\beta$. Given an equivalence $f : \alpha \simeq \{x \in \beta \mid p(x)\}$ and a permutation $g$ of $\alpha$, the cycle type of the extended permutation $g.\text{extendDomain}(f)$ on $\beta$ is equal to the cycle type of $g$.

Equiv.Perm.cycleType_ofSubtype theorem

{p : α → Prop} [DecidablePred p] {g : Perm (Subtype p)} : cycleType (ofSubtype g) = cycleType g

Full source

theorem cycleType_ofSubtype {p : α → Prop} [DecidablePred p] {g : Perm (Subtype p)} :
    cycleType (ofSubtype g) = cycleType g :=
  cycleType_extendDomain (Equiv.refl (Subtype p))

Cycle Type Preservation under Subtype Permutation Lifting

Informal description

For any decidable predicate $p$ on a finite type $\alpha$ and any permutation $g$ of the subtype $\{x \in \alpha \mid p(x)\}$, the cycle type of the permutation $\text{ofSubtype}(g)$ (viewed as a permutation of $\alpha$) is equal to the cycle type of $g$.

Equiv.Perm.mem_cycleType_iff theorem

 {n : ℕ} {σ : Perm α} : n ∈ cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ c.support.card = n

Full source

theorem mem_cycleType_iff {n : ℕ} {σ : Perm α} :
    n ∈ cycleType σn ∈ cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ c.support.card = n := by
  constructor
  · intro h
    obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
    rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
    obtain ⟨c, cl, rfl⟩ := h
    rw [(List.perm_cons_erase cl).pairwise_iff @(Disjoint.symmetric)] at hld
    refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
    · rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
    · exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld
  · rintro ⟨c, t, rfl, hd, hc, rfl⟩
    simp [hd.cycleType, hc.cycleType]

Characterization of Cycle Type Membership via Cycle Decomposition

Informal description

For a natural number $n$ and a permutation $\sigma$ of a finite type $\alpha$, the number $n$ is in the cycle type of $\sigma$ if and only if there exist permutations $c$ and $\tau$ of $\alpha$ such that: 1. $\sigma = c \circ \tau$, 2. $c$ and $\tau$ are disjoint, 3. $c$ is a cycle, and 4. The cardinality of the support of $c$ is equal to $n$.

Equiv.Perm.le_card_support_of_mem_cycleType theorem

{n : ℕ} {σ : Perm α} (h : n ∈ cycleType σ) : n ≤ #σ.support

Full source

theorem le_card_support_of_mem_cycleType {n : ℕ} {σ : Perm α} (h : n ∈ cycleType σ) :
    n ≤ #σ.support :=
  (le_sum_of_mem h).trans (le_of_eq σ.sum_cycleType)

Cycle Size Bound in Permutation Support: $n \leq \#\text{support}(\sigma)$ for $n \in \text{cycleType}(\sigma)$

Informal description

For any natural number $n$ and permutation $\sigma$ of a finite type $\alpha$, if $n$ is in the cycle type of $\sigma$, then $n$ is less than or equal to the cardinality of the support of $\sigma$, i.e., \[ n \leq \#\text{support}(\sigma). \]

Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two theorem

{n : ℕ} {g : Perm α} (hn2 : Fintype.card α < n + 2) (hng : n ∈ g.cycleType) : g.cycleType = { n }

Full source

theorem cycleType_of_card_le_mem_cycleType_add_two {n : ℕ} {g : Perm α}
    (hn2 : Fintype.card α < n + 2) (hng : n ∈ g.cycleType) : g.cycleType = {n} := by
  obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng
  suffices g'1 : g' = 1 by
    rw [hd.cycleType, hc.cycleType, g'1, cycleType_one, add_zero]
  contrapose! hn2 with g'1
  apply le_trans _ (c * g').support.card_le_univ
  rw [hd.card_support_mul]
  exact add_le_add_left (two_le_card_support_of_ne_one g'1) _

Cycle Type Simplification for Large Cycles: $\text{cycleType}(g) = \{n\}$ when $|\alpha| < n + 2$ and $n \in \text{cycleType}(g)$

Informal description

For a natural number $n$ and a permutation $g$ of a finite type $\alpha$, if the cardinality of $\alpha$ is less than $n + 2$ and $n$ is in the cycle type of $g$, then the cycle type of $g$ is the singleton multiset $\{n\}$.

Equiv.Perm.card_compl_support_modEq theorem

 [DecidableEq α] {p n : ℕ} [hp : Fact p.Prime] {σ : Perm α} (hσ : σ ^ p ^ n = 1) :
  σ.supportᶜ.card ≡ Fintype.card α [MOD p]

Full source

theorem card_compl_support_modEq [DecidableEq α] {p n : ℕ} [hp : Fact p.Prime] {σ : Perm α}
    (hσ : σ ^ p ^ n = 1) : σ.supportᶜσ.supportᶜ.card ≡ Fintype.card α [MOD p] := by
  rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]
  · refine Multiset.dvd_sum fun k hk => ?_
    obtain ⟨m, -, hm⟩ := (Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hσ)
    obtain ⟨l, -, rfl⟩ := (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ hm).mp (dvd_of_mem_cycleType hk))
    exact dvd_pow_self _ fun h => (one_lt_of_mem_cycleType hk).ne <| by rw [h, pow_zero]
  · exact Finset.card_le_univ _

Cardinality of Fixed Points Modulo a Prime Power for Permutations

Informal description

Let $\alpha$ be a finite type with decidable equality, $p$ a prime number, and $n$ a natural number. For any permutation $\sigma$ of $\alpha$ such that $\sigma^{p^n} = 1$, the cardinality of the complement of the support of $\sigma$ is congruent modulo $p$ to the cardinality of $\alpha$. That is, \[ |\alpha \setminus \text{supp}(\sigma)| \equiv |\alpha| \pmod{p}. \]

Equiv.Perm.card_fixedPoints_modEq theorem

 [DecidableEq α] {f : Function.End α} {p n : ℕ} [hp : Fact p.Prime] (hf : f ^ p ^ n = 1) :
  Fintype.card α ≡ Fintype.card f.fixedPoints [MOD p]

Full source

/-- The number of fixed points of a `p ^ n`-th root of the identity function over a finite set
and the set's cardinality have the same residue modulo `p`, where `p` is a prime. -/
theorem card_fixedPoints_modEq [DecidableEq α] {f : Function.End α} {p n : ℕ}
    [hp : Fact p.Prime] (hf : f ^ p ^ n = 1) :
    Fintype.cardFintype.card α ≡ Fintype.card f.fixedPoints [MOD p] := by
  let σ : α ≃ α := ⟨f, f ^ (p ^ n - 1),
    leftInverse_iff_comp.mpr ((pow_sub_mul_pow f (Nat.one_le_pow n p hp.out.pos)).trans hf),
    leftInverse_iff_comp.mpr ((pow_mul_pow_sub f (Nat.one_le_pow n p hp.out.pos)).trans hf)⟩
  have hσ : σ ^ p ^ n = 1 := by
    rw [DFunLike.ext'_iff, coe_pow]
    exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf
  suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from
    this ▸ (card_compl_support_modEq hσ).symm
  suffices f.fixedPoints = (support σ)ᶜ by
    simp only [this]; apply Fintype.card_coe
  simp [σ, Set.ext_iff, IsFixedPt]

Fixed Points Cardinality Congruence for Endomorphisms of Prime Power Order

Informal description

Let $\alpha$ be a finite type with decidable equality, $p$ a prime number, and $n$ a natural number. For any endomorphism $f$ of $\alpha$ such that $f^{p^n} = 1$, the cardinality of $\alpha$ is congruent modulo $p$ to the cardinality of the fixed points of $f$. That is, \[ |\alpha| \equiv |\{a \in \alpha \mid f(a) = a\}| \pmod{p}. \]

Equiv.Perm.exists_fixed_point_of_prime theorem

 {p n : ℕ} [hp : Fact p.Prime] (hα : ¬p ∣ Fintype.card α) {σ : Perm α} (hσ : σ ^ p ^ n = 1) : ∃ a : α, σ a = a

Full source

theorem exists_fixed_point_of_prime {p n : ℕ} [hp : Fact p.Prime] (hα : ¬p ∣ Fintype.card α)
    {σ : Perm α} (hσ : σ ^ p ^ n = 1) : ∃ a : α, σ a = a := by
  classical
    contrapose! hα
    simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
    exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
      (card_compl_support_modEq hσ).symm)

Existence of Fixed Points for Permutations of Prime Power Order When Cardinality is Not Divisible by $p$

Informal description

Let $\alpha$ be a finite type, $p$ a prime number, and $n$ a natural number. If $p$ does not divide the cardinality of $\alpha$, then for any permutation $\sigma$ of $\alpha$ satisfying $\sigma^{p^n} = 1$, there exists a fixed point $a \in \alpha$ such that $\sigma(a) = a$.

Equiv.Perm.exists_fixed_point_of_prime' theorem

 {p n : ℕ} [hp : Fact p.Prime] (hα : p ∣ Fintype.card α) {σ : Perm α} (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) :
  ∃ b : α, σ b = b ∧ b ≠ a

Full source

theorem exists_fixed_point_of_prime' {p n : ℕ} [hp : Fact p.Prime] (hα : p ∣ Fintype.card α)
    {σ : Perm α} (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) : ∃ b : α, σ b = b ∧ b ≠ a := by
  classical
    have h : ∀ b : α, b ∈ σ.supportᶜb ∈ σ.supportᶜ ↔ σ b = b := fun b => by
      rw [Finset.mem_compl, mem_support, Classical.not_not]
    obtain ⟨b, hb1, hb2⟩ := Finset.exists_ne_of_one_lt_card (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
        ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a
    exact ⟨b, (h b).mp hb1, hb2⟩

Existence of Distinct Fixed Points for Prime Power Order Permutations

Informal description

Let $\alpha$ be a finite type, $p$ a prime number, and $n$ a natural number. Suppose $p$ divides the cardinality of $\alpha$, and let $\sigma$ be a permutation of $\alpha$ such that $\sigma^{p^n} = 1$. If $a \in \alpha$ is a fixed point of $\sigma$ (i.e., $\sigma(a) = a$), then there exists another fixed point $b \in \alpha$ of $\sigma$ with $b \neq a$.

Equiv.Perm.isCycle_of_prime_order' theorem

{σ : Perm α} (h1 : (orderOf σ).Prime) (h2 : Fintype.card α < 2 * orderOf σ) : σ.IsCycle

Full source

theorem isCycle_of_prime_order' {σ : Perm α} (h1 : (orderOf σ).Prime)
    (h2 : Fintype.card α < 2 * orderOf σ) : σ.IsCycle := by
  classical exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)

Cycle Property for Permutations of Prime Order with Small Domain

Informal description

Let $\sigma$ be a permutation of a finite type $\alpha$. If the order of $\sigma$ is a prime number $p$ and the cardinality of $\alpha$ is less than $2p$, then $\sigma$ is a cycle permutation.

Equiv.Perm.isCycle_of_prime_order'' theorem

{σ : Perm α} (h1 : (Fintype.card α).Prime) (h2 : orderOf σ = Fintype.card α) : σ.IsCycle

Full source

theorem isCycle_of_prime_order'' {σ : Perm α} (h1 : (Fintype.card α).Prime)
    (h2 : orderOf σ = Fintype.card α) : σ.IsCycle :=
  isCycle_of_prime_order' ((congr_arg Nat.Prime h2).mpr h1) <| by
    rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_right (orderOf_pos σ)]
    exact one_lt_two

Cycle Property for Permutations of Prime Order Matching Domain Size

Informal description

Let $\sigma$ be a permutation of a finite type $\alpha$. If the cardinality of $\alpha$ is a prime number $p$ and the order of $\sigma$ equals $p$, then $\sigma$ is a cycle permutation.

Equiv.Perm.vectorsProdEqOne definition

: Set (List.Vector G n)

Full source

/-- The type of vectors with terms from `G`, length `n`, and product equal to `1:G`. -/
def vectorsProdEqOne : Set (List.Vector G n) :=
  { v | v.toList.prod = 1 }

Vectors with product equal to identity

Informal description

The set of all vectors of length $n$ with entries from a group $G$ whose product equals the identity element $1 \in G$.

Equiv.Perm.VectorsProdEqOne.mem_iff theorem

{n : ℕ} (v : List.Vector G n) : v ∈ vectorsProdEqOne G n ↔ v.toList.prod = 1

Full source

theorem mem_iff {n : ℕ} (v : List.Vector G n) : v ∈ vectorsProdEqOne G nv ∈ vectorsProdEqOne G n ↔ v.toList.prod = 1 :=
  Iff.rfl

Characterization of Vectors with Product Identity in Group $G$

Informal description

For any natural number $n$ and any vector $v$ of length $n$ with elements from a group $G$, the vector $v$ belongs to the set of vectors whose product equals the identity element if and only if the product of the elements in $v$ equals $1 \in G$.

Equiv.Perm.VectorsProdEqOne.zero_eq theorem

: vectorsProdEqOne G 0 = { Vector.nil }

Full source

theorem zero_eq : vectorsProdEqOne G 0 = {Vector.nil} :=
  Set.eq_singleton_iff_unique_mem.mpr ⟨Eq.refl (1 : G), fun v _ => v.eq_nil⟩

Empty Vectors with Product Equal to Identity

Informal description

For any group $G$, the set of vectors of length $0$ with product equal to the identity element consists solely of the empty vector `Vector.nil`.

Equiv.Perm.VectorsProdEqOne.one_eq theorem

: vectorsProdEqOne G 1 = {Vector.nil.cons 1}

Full source

theorem one_eq : vectorsProdEqOne G 1 = {Vector.nil.cons 1} := by
  simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, List.Vector.toList_singleton,
    List.prod_singleton, List.Vector.head_cons, true_and]
  exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)

Characterization of Length-1 Vectors with Product Identity in Group $G$

Informal description

For any group $G$, the set of vectors of length $1$ with product equal to the identity element consists solely of the vector containing the identity element $1$ of $G$.

Equiv.Perm.VectorsProdEqOne.zeroUnique instance

: Unique (vectorsProdEqOne G 0)

Full source

instance zeroUnique : Unique (vectorsProdEqOne G 0) := by
  rw [zero_eq]
  exact Set.uniqueSingleton Vector.nil

Uniqueness of the Empty Vector with Product Identity

Informal description

For any group $G$, the set of vectors of length $0$ with product equal to the identity element is uniquely determined by the empty vector.

Equiv.Perm.VectorsProdEqOne.oneUnique instance

: Unique (vectorsProdEqOne G 1)

Full source

instance oneUnique : Unique (vectorsProdEqOne G 1) := by
  rw [one_eq]
  exact Set.uniqueSingleton (Vector.nil.cons 1)

Uniqueness of Length-1 Vectors with Product Identity in a Group

Informal description

For any group $G$, the set of vectors of length $1$ with product equal to the identity element is uniquely determined by the vector containing the identity element $1$ of $G$.

Equiv.Perm.VectorsProdEqOne.vectorEquiv definition

: List.Vector G n ≃ vectorsProdEqOne G (n + 1)

Full source

/-- Given a vector `v` of length `n`, make a vector of length `n + 1` whose product is `1`,
by appending the inverse of the product of `v`. -/
@[simps]
def vectorEquiv : List.VectorList.Vector G n ≃ vectorsProdEqOne G (n + 1) where
  toFun v := ⟨v.toList.prod⁻¹ ::ᵥ v, by
    rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]⟩
  invFun v := v.1.tail
  left_inv v := v.tail_cons v.toList.prod⁻¹
  right_inv v := Subtype.ext <|
    calc
      v.1.tail.toList.prod⁻¹v.1.tail.toList.prod⁻¹ ::ᵥ v.1.tail = v.1.head ::ᵥ v.1.tail :=
        congr_arg (· ::ᵥ v.1.tail) <| Eq.symm <| eq_inv_of_mul_eq_one_left <| by
          rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]
          exact v.2
      _ = v.1 := v.1.cons_head_tail

Equivalence between vectors and vectors with product one

Informal description

Given a group $G$ and a natural number $n$, the equivalence `vectorEquiv` maps a vector $v$ of length $n$ to a vector of length $n + 1$ whose product is the identity element $1 \in G$. The new vector is constructed by prepending the inverse of the product of the entries of $v$ to $v$ itself. The inverse operation takes a vector of length $n + 1$ with product $1$ and returns its tail (i.e., the vector without the first element).

Equiv.Perm.VectorsProdEqOne.equivVector definition

: ∀ n, vectorsProdEqOne G n ≃ List.Vector G (n - 1)

Full source

/-- Given a vector `v` of length `n` whose product is 1, make a vector of length `n - 1`,
by deleting the last entry of `v`. -/
def equivVector : ∀ n, vectorsProdEqOnevectorsProdEqOne G n ≃ List.Vector G (n - 1)
  | 0 => (ofUnique (vectorsProdEqOne G 0) (vectorsProdEqOne G 1)).trans (vectorEquiv G 0).symm
  | (n + 1) => (vectorEquiv G n).symm

Equivalence between identity-product vectors and shorter vectors

Informal description

For any group $G$ and natural number $n$, there is an equivalence between the set of vectors of length $n$ with product equal to the identity element and the set of vectors of length $n-1$ over $G$. When $n=0$, the equivalence is constructed via the unique empty vector. For $n+1$, the equivalence is given by the inverse of the operation that prepends the inverse product to a vector of length $n$.

Equiv.Perm.VectorsProdEqOne.instFintypeElemVectorVectorsProdEqOne instance

[Fintype G] : Fintype (vectorsProdEqOne G n)

Full source

instance [Fintype G] : Fintype (vectorsProdEqOne G n) :=
  Fintype.ofEquiv (List.Vector G (n - 1)) (equivVector G n).symm

Finiteness of Identity-Product Vectors in Finite Groups

Informal description

For any finite group $G$ and natural number $n$, the set of vectors of length $n$ with entries in $G$ whose product equals the identity element is finite.

Equiv.Perm.VectorsProdEqOne.card theorem

[Fintype G] : Fintype.card (vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)

Full source

theorem card [Fintype G] : Fintype.card (vectorsProdEqOne G n) = Fintype.card G ^ (n - 1) :=
  (Fintype.card_congr (equivVector G n)).trans (card_vector (n - 1))

Cardinality of Identity-Product Vectors: $|G|^{n-1}$

Informal description

For a finite group $G$ and a natural number $n$, the number of vectors of length $n$ with entries in $G$ whose product equals the identity element is $|G|^{n-1}$, where $|G|$ denotes the cardinality of $G$.

Equiv.Perm.VectorsProdEqOne.rotate definition

: vectorsProdEqOne G n

Full source

/-- Rotate a vector whose product is 1. -/
def rotate : vectorsProdEqOne G n :=
  ⟨⟨_, (v.1.1.length_rotate k).trans v.1.2⟩, List.prod_rotate_eq_one_of_prod_eq_one v.2 k⟩

Rotation of a vector with product one

Informal description

Given a vector $ v $ of length $ n $ in a group $ G $ whose product of entries is the identity element, the function `rotate` returns a rotated version of $ v $ by $ k $ positions, which also has product equal to the identity.

Equiv.Perm.VectorsProdEqOne.rotate_zero theorem

: rotate v 0 = v

Full source

theorem rotate_zero : rotate v 0 = v :=
  Subtype.ext (Subtype.ext v.1.1.rotate_zero)

Rotation by Zero Preserves Vector Identity

Informal description

For any vector $v$ in the set of vectors with product equal to the identity, rotating $v$ by $0$ positions leaves it unchanged, i.e., $\text{rotate}(v, 0) = v$.

Equiv.Perm.VectorsProdEqOne.rotate_rotate theorem

: rotate (rotate v j) k = rotate v (j + k)

Full source

theorem rotate_rotate : rotate (rotate v j) k = rotate v (j + k) :=
  Subtype.ext (Subtype.ext (v.1.1.rotate_rotate j k))

Rotation Composition Property for Vectors with Product One

Informal description

For any vector $v$ in the set of vectors with product equal to the identity, rotating $v$ by $j$ positions and then by $k$ positions is equivalent to rotating $v$ by $j + k$ positions, i.e., $\text{rotate}(\text{rotate}(v, j), k) = \text{rotate}(v, j + k)$.

Equiv.Perm.VectorsProdEqOne.rotate_length theorem

: rotate v n = v

Full source

theorem rotate_length : rotate v n = v :=
  Subtype.ext (Subtype.ext ((congr_arg _ v.1.2.symm).trans v.1.1.rotate_length))

Full Rotation Preserves Vector Identity

Informal description

For any vector $v$ of length $n$ in a group $G$ whose product of entries is the identity element, rotating $v$ by $n$ positions returns the original vector, i.e., $\text{rotate}(v, n) = v$.

exists_prime_orderOf_dvd_card theorem

 {G : Type*} [Group G] [Fintype G] (p : ℕ) [hp : Fact p.Prime] (hdvd : p ∣ Fintype.card G) : ∃ x : G, orderOf x = p

Full source

/-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
`p` in `G`. This is known as Cauchy's theorem. -/
theorem _root_.exists_prime_orderOf_dvd_card {G : Type*} [Group G] [Fintype G] (p : ℕ)
    [hp : Fact p.Prime] (hdvd : p ∣ Fintype.card G) : ∃ x : G, orderOf x = p := by
  have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_lt hp.out.one_lt)
  have Scard :=
    calc
      p ∣ Fintype.card G ^ (p - 1) := hdvd.trans (dvd_pow (dvd_refl _) hp')
      _ = Fintype.card (vectorsProdEqOne G p) := (VectorsProdEqOne.card G p).symm
  let f : ℕ → vectorsProdEqOne G p → vectorsProdEqOne G p := fun k v =>
    VectorsProdEqOne.rotate v k
  have hf1 : ∀ v, f 0 v = v := VectorsProdEqOne.rotate_zero
  have hf2 : ∀ j k v, f k (f j v) = f (j + k) v := fun j k v =>
    VectorsProdEqOne.rotate_rotate v j k
  have hf3 : ∀ v, f p v = v := VectorsProdEqOne.rotate_length
  let σ :=
    Equiv.mk (f 1) (f (p - 1)) (fun s => by rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3])
      fun s => by rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
  have hσ : ∀ k v, (σ ^ k) v = f k v := fun k =>
    Nat.rec (fun v => (hf1 v).symm) (fun k hk v => by
      rw [pow_succ, Perm.mul_apply, hk (σ v), Nat.succ_eq_one_add, ← hf2 1 k]
      simp only [σ, coe_fn_mk]) k
  replace hσ : σ ^ p ^ 1 = 1 := Perm.ext fun v => by rw [pow_one, hσ, hf3, one_apply]
  let v₀ : vectorsProdEqOne G p :=
    ⟨List.Vector.replicate p 1, (List.prod_replicate p 1).trans (one_pow p)⟩
  have hv₀ : σ v₀ = v₀ := Subtype.ext (Subtype.ext (List.rotate_replicate (1 : G) p 1))
  obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀
  refine
    Exists.imp (fun g hg => orderOf_eq_prime ?_ fun hg' => hv2 ?_)
      (List.rotate_one_eq_self_iff_eq_replicate.mp (Subtype.ext_iff.mp (Subtype.ext_iff.mp hv1)))
  · rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
  · rw [Subtype.ext_iff_val, Subtype.ext_iff_val, hg, hg', v.1.2]
    simp only [v₀, List.Vector.replicate]

Cauchy's Theorem: Existence of Elements of Prime Order in Finite Groups

Informal description

For any finite group $G$ and prime number $p$ dividing the order of $G$, there exists an element $x \in G$ of order $p$.

exists_prime_addOrderOf_dvd_card theorem

 {G : Type*} [AddGroup G] [Fintype G] (p : ℕ) [Fact p.Prime] (hdvd : p ∣ Fintype.card G) : ∃ x : G, addOrderOf x = p

Full source

/-- For every prime `p` dividing the order of a finite additive group `G` there exists an element of
order `p` in `G`. This is the additive version of Cauchy's theorem. -/
theorem _root_.exists_prime_addOrderOf_dvd_card {G : Type*} [AddGroup G] [Fintype G] (p : ℕ)
    [Fact p.Prime] (hdvd : p ∣ Fintype.card G) : ∃ x : G, addOrderOf x = p :=
  @exists_prime_orderOf_dvd_card (Multiplicative G) _ _ _ _ (by convert hdvd)

Cauchy's Theorem for Additive Groups: Existence of Elements of Prime Additive Order

Informal description

For any finite additive group $G$ and prime number $p$ dividing the order of $G$, there exists an element $x \in G$ whose additive order is $p$.

exists_prime_orderOf_dvd_card' theorem

{G : Type*} [Group G] [Finite G] (p : ℕ) [hp : Fact p.Prime] (hdvd : p ∣ Nat.card G) : ∃ x : G, orderOf x = p

Full source

/-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
`p` in `G`. This is known as Cauchy's theorem. -/
@[to_additive]
theorem _root_.exists_prime_orderOf_dvd_card' {G : Type*} [Group G] [Finite G] (p : ℕ)
    [hp : Fact p.Prime] (hdvd : p ∣ Nat.card G) : ∃ x : G, orderOf x = p := by
  have := Fintype.ofFinite G
  rw [Nat.card_eq_fintype_card] at hdvd
  exact exists_prime_orderOf_dvd_card p hdvd

Cauchy's Theorem for Finite Groups (General Version)

Informal description

For any finite group $G$ and prime number $p$ dividing the order of $G$, there exists an element $x \in G$ of order $p$.

Equiv.Perm.subgroup_eq_top_of_swap_mem theorem

 [DecidableEq α] {H : Subgroup (Perm α)} [d : DecidablePred (· ∈ H)] {τ : Perm α} (h0 : (Fintype.card α).Prime)
  (h1 : Fintype.card α ∣ Fintype.card H) (h2 : τ ∈ H) (h3 : IsSwap τ) : H = ⊤

Full source

theorem subgroup_eq_top_of_swap_mem [DecidableEq α] {H : Subgroup (Perm α)}
    [d : DecidablePred (· ∈ H)] {τ : Perm α} (h0 : (Fintype.card α).Prime)
    (h1 : Fintype.cardFintype.card α ∣ Fintype.card H) (h2 : τ ∈ H) (h3 : IsSwap τ) : H = ⊤ := by
  haveI : Fact (Fintype.card α).Prime := ⟨h0⟩
  obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
  have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (Subgroup.orderOf_coe σ).trans hσ
  have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
  have hσ3 : (σ : Perm α).support = ⊤ :=
    Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
  have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
  rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]
  exact ⟨Subtype.mem σ, h2⟩

Subgroup of Permutation Group Containing a Transposition is Entire Group for Prime Degree

Informal description

Let $\alpha$ be a finite type with prime cardinality, and let $H$ be a subgroup of the permutation group $\text{Perm}(\alpha)$. Suppose that: 1. The cardinality of $\alpha$ divides the cardinality of $H$, 2. $H$ contains a transposition $\tau$ (i.e., a permutation that swaps two elements and fixes the rest). Then $H$ is equal to the entire permutation group $\text{Perm}(\alpha)$.

Equiv.Perm.partition definition

(σ : Perm α) : (Fintype.card α).Partition

Full source

/-- The partition corresponding to a permutation -/
def partition (σ : Perm α) : (Fintype.card α).Partition where
  parts := σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
  parts_pos {n hn} := by
    rcases mem_add.mp hn with hn | hn
    · exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)
    · exact lt_of_lt_of_le zero_lt_one (ge_of_eq (Multiset.eq_of_mem_replicate hn))
  parts_sum := by
    rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]

Partition associated with a permutation

Informal description

The partition associated with a permutation $\sigma$ of a finite type $\alpha$ is defined as the multiset consisting of the cycle type of $\sigma$ together with additional $1$'s, where the number of $1$'s is equal to the difference between the cardinality of $\alpha$ and the size of the support of $\sigma$. More precisely, the parts of the partition are given by $\sigma.\text{cycleType} + \text{replicate} (|\alpha| - |\text{supp}(\sigma)|) 1$, where $\text{replicate} \, n \, x$ denotes a multiset containing $n$ copies of $x$. Each part in the partition is positive, and the sum of all parts equals the cardinality of $\alpha$.

Equiv.Perm.parts_partition theorem

{σ : Perm α} : σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1

Full source

theorem parts_partition {σ : Perm α} :
    σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 :=
  rfl

Decomposition of Permutation Partition into Cycle Type and Fixed Points

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the parts of the partition associated with $\sigma$ are equal to the cycle type of $\sigma$ plus a multiset consisting of $|\alpha| - |\text{supp}(\sigma)|$ copies of $1$, where $|\alpha|$ is the cardinality of $\alpha$ and $|\text{supp}(\sigma)|$ is the size of the support of $\sigma$.

Equiv.Perm.filter_parts_partition_eq_cycleType theorem

{σ : Perm α} : ((partition σ).parts.filter fun n => 2 ≤ n) = σ.cycleType

Full source

theorem filter_parts_partition_eq_cycleType {σ : Perm α} :
    ((partition σ).parts.filter fun n => 2 ≤ n) = σ.cycleType := by
  rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
    Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]
  rw [Multiset.eq_of_mem_replicate h]
  decide

Cycle Type as Filtered Partition Parts: $\mathrm{filter}_{\geq 2}(\mathrm{parts}(\sigma.\mathrm{partition})) = \sigma.\mathrm{cycleType}$

Informal description

For any permutation $\sigma$ of a finite type $\alpha$, the multiset obtained by filtering the parts of the partition associated with $\sigma$ to include only those parts of size at least 2 is equal to the cycle type of $\sigma$. In other words, if we take the parts of $\sigma$'s partition and remove all the $1$'s (which correspond to fixed points), we are left with exactly the cycle type of $\sigma$.

Equiv.Perm.partition_eq_of_isConj theorem

{σ τ : Perm α} : IsConj σ τ ↔ σ.partition = τ.partition

Full source

theorem partition_eq_of_isConj {σ τ : Perm α} : IsConjIsConj σ τ ↔ σ.partition = τ.partition := by
  rw [isConj_iff_cycleType_eq]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
  · rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

Conjugacy Criterion via Partition Equality for Permutations

Informal description

Two permutations $\sigma$ and $\tau$ of a finite type $\alpha$ are conjugate if and only if their associated partitions are equal, i.e., $\text{IsConj}(\sigma, \tau) \leftrightarrow \text{partition}(\sigma) = \text{partition}(\tau)$.

Equiv.Perm.IsThreeCycle definition

[DecidableEq α] (σ : Perm α) : Prop

Full source

/-- A three-cycle is a cycle of length 3. -/
def IsThreeCycle [DecidableEq α] (σ : Perm α) : Prop :=
  σ.cycleType = {3}

Three-cycle permutation

Informal description

A permutation $\sigma$ of a finite type $\alpha$ is called a three-cycle if its cycle type is exactly the multiset $\{3\}$, meaning it consists of exactly one cycle of length 3 in its cycle decomposition.

Equiv.Perm.IsThreeCycle.cycleType theorem

(h : IsThreeCycle σ) : σ.cycleType = { 3 }

Full source

theorem cycleType (h : IsThreeCycle σ) : σ.cycleType = {3} :=
  h

Cycle type of a three-cycle permutation is $\{3\}$

Informal description

If $\sigma$ is a three-cycle permutation of a finite type $\alpha$, then its cycle type is the multiset $\{3\}$.

Equiv.Perm.IsThreeCycle.card_support theorem

(h : IsThreeCycle σ) : #σ.support = 3

Full source

theorem card_support (h : IsThreeCycle σ) : #σ.support = 3 := by
  rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]

Support Cardinality of a Three-Cycle Permutation is 3

Informal description

If $\sigma$ is a three-cycle permutation of a finite type $\alpha$, then the cardinality of its support is 3, i.e., $\#\text{support}(\sigma) = 3$.

card_support_eq_three_iff theorem

: #σ.support = 3 ↔ σ.IsThreeCycle

Full source

theorem _root_.card_support_eq_three_iff : #σ.support#σ.support = 3 ↔ σ.IsThreeCycle := by
  refine ⟨fun h => ?_, IsThreeCycle.card_support⟩
  by_cases h0 : σ.cycleType = 0
  · rw [← sum_cycleType, h0, sum_zero] at h
    exact (ne_of_lt zero_lt_three h).elim
  obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0
  by_cases h1 : σ.cycleType.erase n = 0
  · rw [← sum_cycleType, ← cons_erase hn, h1, cons_zero, Multiset.sum_singleton] at h
    rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
  obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1
  rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h
  have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False := by omega
  cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h

Support Cardinality Three if and only if Three-Cycle Permutation

Informal description

For a permutation $\sigma$ of a finite type $\alpha$, the cardinality of its support is 3 if and only if $\sigma$ is a three-cycle permutation. That is, \[ \#\text{support}(\sigma) = 3 \leftrightarrow \text{IsThreeCycle}(\sigma). \]

Equiv.Perm.IsThreeCycle.isCycle theorem

(h : IsThreeCycle σ) : IsCycle σ

Full source

theorem isCycle (h : IsThreeCycle σ) : IsCycle σ := by
  rw [← card_cycleType_eq_one, h.cycleType, card_singleton]

Three-Cycle Permutations are Cycles

Informal description

If $\sigma$ is a three-cycle permutation of a finite type $\alpha$, then $\sigma$ is a cycle permutation.

Equiv.Perm.IsThreeCycle.sign theorem

(h : IsThreeCycle σ) : sign σ = 1

Full source

theorem sign (h : IsThreeCycle σ) : sign σ = 1 := by
  rw [Equiv.Perm.sign_of_cycleType, h.cycleType]
  rfl

Sign of a Three-Cycle Permutation is $1$

Informal description

For any three-cycle permutation $\sigma$ of a finite type $\alpha$, the sign of $\sigma$ is equal to $1$.

Equiv.Perm.IsThreeCycle.inv theorem

{f : Perm α} (h : IsThreeCycle f) : IsThreeCycle f⁻¹

Full source

theorem inv {f : Perm α} (h : IsThreeCycle f) : IsThreeCycle f⁻¹ := by
  rwa [IsThreeCycle, cycleType_inv]

Inverse of a Three-Cycle is a Three-Cycle

Informal description

For any permutation $f$ of a finite type $\alpha$, if $f$ is a three-cycle (i.e., its cycle type is $\{3\}$), then its inverse $f^{-1}$ is also a three-cycle.

Equiv.Perm.IsThreeCycle.inv_iff theorem

{f : Perm α} : IsThreeCycle f⁻¹ ↔ IsThreeCycle f

Full source

@[simp]
theorem inv_iff {f : Perm α} : IsThreeCycleIsThreeCycle f⁻¹ ↔ IsThreeCycle f :=
  ⟨by
    rw [← inv_inv f]
    apply inv, inv⟩

Inverse of a Permutation is a Three-Cycle if and only if the Permutation is a Three-Cycle

Informal description

For any permutation $f$ of a finite type $\alpha$, the inverse permutation $f^{-1}$ is a three-cycle if and only if $f$ itself is a three-cycle.

Equiv.Perm.IsThreeCycle.orderOf theorem

{g : Perm α} (ht : IsThreeCycle g) : orderOf g = 3

Full source

theorem orderOf {g : Perm α} (ht : IsThreeCycle g) : orderOf g = 3 := by
  rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]

Order of a Three-Cycle Permutation is 3

Informal description

For any three-cycle permutation $g$ of a finite type $\alpha$, the order of $g$ is equal to $3$.

Equiv.Perm.IsThreeCycle.isThreeCycle_sq theorem

{g : Perm α} (ht : IsThreeCycle g) : IsThreeCycle (g * g)

Full source

theorem isThreeCycle_sq {g : Perm α} (ht : IsThreeCycle g) : IsThreeCycle (g * g) := by
  rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
  rw [ht.orderOf]
  norm_num

Square of a Three-Cycle Permutation is a Three-Cycle

Informal description

For any three-cycle permutation $g$ of a finite type $\alpha$, the square of $g$ (i.e., $g \circ g$) is also a three-cycle.

Equiv.Perm.isThreeCycle_swap_mul_swap_same theorem

{a b c : α} (ab : a ≠ b) (ac : a ≠ c) (bc : b ≠ c) : IsThreeCycle (swap a b * swap a c)

Full source

theorem isThreeCycle_swap_mul_swap_same {a b c : α} (ab : a ≠ b) (ac : a ≠ c) (bc : b ≠ c) :
    IsThreeCycle (swap a b * swap a c) := by
  suffices h : support (swap a b * swap a c) = {a, b, c} by
    rw [← card_support_eq_three_iff, h]
    simp [ab, ac, bc]
  apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
  · simp [ab, ac, bc]
  · simp only [Finset.mem_insert, Finset.mem_singleton] at hx
    rw [mem_support]
    simp only [Perm.coe_mul, Function.comp_apply, Ne]
    obtain rfl | rfl | rfl := hx
    · rw [swap_apply_left, swap_apply_of_ne_of_ne ac.symm bc.symm]
      exact ac.symm
    · rw [swap_apply_of_ne_of_ne ab.symm bc, swap_apply_right]
      exact ab
    · rw [swap_apply_right, swap_apply_left]
      exact bc

Composition of Two Transpositions with a Common Element is a Three-Cycle

Informal description

For any three distinct elements $a, b, c$ in a finite type $\alpha$, the composition of the transpositions swapping $a$ with $b$ and $a$ with $c$ is a three-cycle permutation. That is, if $a \neq b$, $a \neq c$, and $b \neq c$, then the permutation $\text{swap}(a, b) \circ \text{swap}(a, c)$ is a three-cycle.

Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles theorem

{a b c : α} (ab : a ≠ b) (ac : a ≠ c) : swap a b * swap a c ∈ closure {σ : Perm α | IsThreeCycle σ}

Full source

theorem swap_mul_swap_same_mem_closure_three_cycles {a b c : α} (ab : a ≠ b) (ac : a ≠ c) :
    swapswap a b * swap a c ∈ closure { σ : Perm α | IsThreeCycle σ } := by
  by_cases bc : b = c
  · subst bc
    simp [one_mem]
  exact subset_closure (isThreeCycle_swap_mul_swap_same ab ac bc)

Composition of Transpositions with Common Element is in Three-Cycle Subgroup

Informal description

For any three distinct elements $a, b, c$ in a finite type $\alpha$ with $a \neq b$ and $a \neq c$, the composition of the transpositions swapping $a$ with $b$ and $a$ with $c$ belongs to the subgroup generated by all three-cycle permutations. That is, $\text{swap}(a, b) \circ \text{swap}(a, c) \in \langle \{\sigma \in \text{Perm}(\alpha) \mid \sigma \text{ is a three-cycle}\} \rangle$.

Equiv.Perm.IsSwap.mul_mem_closure_three_cycles theorem

{σ τ : Perm α} (hσ : IsSwap σ) (hτ : IsSwap τ) : σ * τ ∈ closure {σ : Perm α | IsThreeCycle σ}

Full source

theorem IsSwap.mul_mem_closure_three_cycles {σ τ : Perm α} (hσ : IsSwap σ) (hτ : IsSwap τ) :
    σ * τ ∈ closure { σ : Perm α | IsThreeCycle σ } := by
  obtain ⟨a, b, ab, rfl⟩ := hσ
  obtain ⟨c, d, cd, rfl⟩ := hτ
  by_cases ac : a = c
  · subst ac
    exact swap_mul_swap_same_mem_closure_three_cycles ab cd
  have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d) := by
    simp [swap_comm c a, mul_assoc]
  rw [h']
  exact
    mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
      (swap_mul_swap_same_mem_closure_three_cycles (Ne.symm ac) cd)

Composition of Two Transpositions is in Three-Cycle Subgroup

Informal description

For any two transpositions $\sigma$ and $\tau$ of a finite type $\alpha$, their composition $\sigma \circ \tau$ belongs to the subgroup generated by all three-cycle permutations. That is, $\sigma \circ \tau \in \langle \{\sigma \in \text{Perm}(\alpha) \mid \sigma \text{ is a three-cycle}\} \rangle$.

Mathlib.GroupTheory.Perm.Cycle.Type

Main definitions

Main results