From 0c0fb53cb9e37694abf7e9d16215d6e261c459d9 Mon Sep 17 00:00:00 2001
From: tb65536 <tb65536@uw.edu>
Date: Tue, 30 Mar 2021 17:12:56 +0000
Subject: [PATCH] feat(group_theory/perm/cycles): Order of is_cycle (#6873)

The order of a cycle equals the cardinality of its support.
---
 src/group_theory/perm/basic.lean  |  9 +++++----
 src/group_theory/perm/cycles.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/src/group_theory/perm/basic.lean b/src/group_theory/perm/basic.lean
index 2bb0721c6ad8a..0bc8dac90d123 100644
--- a/src/group_theory/perm/basic.lean
+++ b/src/group_theory/perm/basic.lean
@@ -3,11 +3,8 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import data.equiv.basic
-import algebra.group.basic
-import algebra.group.hom
 import algebra.group.pi
-import algebra.group.prod
+import algebra.group_power
 
 /-!
 # The group of permutations (self-equivalences) of a type `α`
@@ -54,6 +51,10 @@ lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y := f.eq_
 
 lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y := f.symm_apply_eq
 
+lemma gpow_apply_comm {α : Type*} (σ : equiv.perm α) (m n : ℤ) {x : α} :
+  (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x) :=
+by rw [←equiv.perm.mul_apply, ←equiv.perm.mul_apply, gpow_mul_comm]
+
 /-! Lemmas about mixing `perm` with `equiv`. Because we have multiple ways to express
 `equiv.refl`, `equiv.symm`, and `equiv.trans`, we want simp lemmas for every combination.
 The assumption made here is that if you're using the group structure, you want to preserve it after
diff --git a/src/group_theory/perm/cycles.lean b/src/group_theory/perm/cycles.lean
index 8326710491cfe..a9cded53aa11a 100644
--- a/src/group_theory/perm/cycles.lean
+++ b/src/group_theory/perm/cycles.lean
@@ -66,6 +66,37 @@ by classical; exact ⟨(n % order_of f).to_nat, by {
   have := n.mod_nonneg (int.coe_nat_ne_zero.mpr (ne_of_gt (order_of_pos f))),
   rwa [← gpow_coe_nat, int.to_nat_of_nonneg this, ← gpow_eq_mod_order_of] }⟩
 
+/-- The subgroup generated by a cycle is in bijection with its support -/
+noncomputable def is_cycle.gpowers_equiv_support {σ : perm α} (hσ : is_cycle σ) :
+  (↑(subgroup.gpowers σ) : set (perm α)) ≃ (↑(σ.support) : set α) :=
+equiv.of_bijective (λ τ, ⟨τ (classical.some hσ),
+begin
+  obtain ⟨τ, n, rfl⟩ := τ,
+  rw [finset.mem_coe, mem_support],
+  refine λ h, (classical.some_spec hσ).1 ((σ ^ n).injective _),
+  rwa [←mul_apply, mul_gpow_self, ←mul_self_gpow],
+end⟩)
+begin
+  split,
+  { rintros ⟨a, m, rfl⟩ ⟨b, n, rfl⟩ h,
+    ext y,
+    by_cases hy : σ y = y,
+    { simp_rw [subtype.coe_mk, gpow_apply_eq_self_of_apply_eq_self hy] },
+    { obtain ⟨i, rfl⟩ := (classical.some_spec hσ).2 y hy,
+      rw [subtype.coe_mk, subtype.coe_mk, gpow_apply_comm σ m i, gpow_apply_comm σ n i],
+      exact congr_arg _ (subtype.ext_iff.mp h) } }, by
+  { rintros ⟨y, hy⟩,
+    rw [finset.mem_coe, mem_support] at hy,
+    obtain ⟨n, rfl⟩ := (classical.some_spec hσ).2 y hy,
+    exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩ },
+end
+
+lemma order_of_is_cycle {σ : perm α} (hσ : is_cycle σ) : order_of σ = σ.support.card :=
+begin
+  rw [order_eq_card_gpowers, ←fintype.card_coe],
+  convert fintype.card_congr (is_cycle.gpowers_equiv_support hσ),
+end
+
 lemma is_cycle_swap_mul_aux₁ {α : Type*} [decidable_eq α] : ∀ (n : ℕ) {b x : α} {f : perm α}
   (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
   ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b