feat(GroupTheory/Perm/Cycle/Factors): Remove finiteness requirement from cycleOf. (#13145)

cycleOf can be defined using only a decidability condition, rather than the current finiteness condition (from which decidability can be inferred). This commit removes this dependency on finiteness.



Co-authored-by: Wrenna Robson <wren.robson@gmail.com>

Author: linesthatinterlace

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -243,6 +243,17 @@ theorem SameCycle.exists_pow_eq'' [Finite α] (h : SameCycle f x y) :
     · exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩
 #align equiv.perm.same_cycle.exists_pow_eq'' Equiv.Perm.SameCycle.exists_pow_eq''
 
+instance (f : Perm α) [DecidableRel (SameCycle f⁻¹)] :
+    DecidableRel (SameCycle f) := fun x y =>
+  decidable_of_iff (f⁻¹.SameCycle x y) (sameCycle_inv)
+
+instance (f : Perm α) [DecidableRel (SameCycle f)] :
+    DecidableRel (SameCycle f⁻¹) := fun x y =>
+  decidable_of_iff (f.SameCycle x y) (sameCycle_inv).symm
+
+instance (priority := 100) [DecidableEq α] : DecidableRel (SameCycle (1 : Perm α)) := fun x y =>
+  decidable_of_iff (x = y) sameCycle_one.symm
+
 instance [Fintype α] [DecidableEq α] (f : Perm α) : DecidableRel (SameCycle f) := fun x y =>
   decidable_of_iff (∃ n ∈ List.range (Fintype.card (Perm α)), (f ^ n) x = y)
     ⟨fun ⟨n, _, hn⟩ => ⟨n, hn⟩, fun ⟨i, hi⟩ => ⟨(i % orderOf f).natAbs,

Mathlib/GroupTheory/Perm/Cycle/Factors.lean

@@ -38,14 +38,14 @@ namespace Equiv.Perm
 
 section CycleOf
 
-variable [DecidableEq α] [Fintype α] {f g : Perm α} {x y : α}
+variable {f g : Perm α} {x y : α} [DecidableRel f.SameCycle] [DecidableRel g.SameCycle]
 
 /-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/
-def cycleOf (f : Perm α) (x : α) : Perm α :=
+def cycleOf (f : Perm α) [DecidableRel f.SameCycle] (x : α) : Perm α :=
   ofSubtype (subtypePerm f fun _ => sameCycle_apply_right.symm : Perm { y // SameCycle f x y })
 #align equiv.perm.cycle_of Equiv.Perm.cycleOf
 
-theorem cycleOf_apply (f : Perm α) (x y : α) :
+theorem cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (x y : α) :
     cycleOf f x y = if SameCycle f x y then f y else y := by
   dsimp only [cycleOf]
   split_ifs with h
@@ -55,14 +55,16 @@ theorem cycleOf_apply (f : Perm α) (x y : α) :
     exact h
 #align equiv.perm.cycle_of_apply Equiv.Perm.cycleOf_apply
 
-theorem cycleOf_inv (f : Perm α) (x : α) : (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
+theorem cycleOf_inv (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
+    (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
   Equiv.ext fun y => by
     rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
     split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]
 #align equiv.perm.cycle_of_inv Equiv.Perm.cycleOf_inv
 
 @[simp]
-theorem cycleOf_pow_apply_self (f : Perm α) (x : α) : ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x := by
+theorem cycleOf_pow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
+    ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x := by
   intro n
   induction' n with n hn
   · rfl
@@ -71,7 +73,7 @@ theorem cycleOf_pow_apply_self (f : Perm α) (x : α) : ∀ n : ℕ, (cycleOf f
 #align equiv.perm.cycle_of_pow_apply_self Equiv.Perm.cycleOf_pow_apply_self
 
 @[simp]
-theorem cycleOf_zpow_apply_self (f : Perm α) (x : α) :
+theorem cycleOf_zpow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
     ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x := by
   intro z
   induction' z with z hz
@@ -96,26 +98,27 @@ theorem SameCycle.cycleOf_eq (h : SameCycle f x y) : cycleOf f x = cycleOf f y :
 #align equiv.perm.same_cycle.cycle_of_eq Equiv.Perm.SameCycle.cycleOf_eq
 
 @[simp]
-theorem cycleOf_apply_apply_zpow_self (f : Perm α) (x : α) (k : ℤ) :
+theorem cycleOf_apply_apply_zpow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℤ) :
     cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
   rw [SameCycle.cycleOf_apply]
   · rw [add_comm, zpow_add, zpow_one, mul_apply]
   · exact ⟨k, rfl⟩
 #align equiv.perm.cycle_of_apply_apply_zpow_self Equiv.Perm.cycleOf_apply_apply_zpow_self
 
 @[simp]
-theorem cycleOf_apply_apply_pow_self (f : Perm α) (x : α) (k : ℕ) :
+theorem cycleOf_apply_apply_pow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℕ) :
     cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
   convert cycleOf_apply_apply_zpow_self f x k using 1
 #align equiv.perm.cycle_of_apply_apply_pow_self Equiv.Perm.cycleOf_apply_apply_pow_self
 
 @[simp]
-theorem cycleOf_apply_apply_self (f : Perm α) (x : α) : cycleOf f x (f x) = f (f x) := by
+theorem cycleOf_apply_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
+    cycleOf f x (f x) = f (f x) := by
   convert cycleOf_apply_apply_pow_self f x 1 using 1
 #align equiv.perm.cycle_of_apply_apply_self Equiv.Perm.cycleOf_apply_apply_self
 
 @[simp]
-theorem cycleOf_apply_self (f : Perm α) (x : α) : cycleOf f x x = f x :=
+theorem cycleOf_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f x x = f x :=
   SameCycle.rfl.cycleOf_apply
 #align equiv.perm.cycle_of_apply_self Equiv.Perm.cycleOf_apply_self
 
@@ -128,7 +131,7 @@ theorem IsCycle.cycleOf_eq (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :
 #align equiv.perm.is_cycle.cycle_of_eq Equiv.Perm.IsCycle.cycleOf_eq
 
 @[simp]
-theorem cycleOf_eq_one_iff (f : Perm α) : cycleOf f x = 1 ↔ f x = x := by
+theorem cycleOf_eq_one_iff (f : Perm α) [DecidableRel f.SameCycle] : cycleOf f x = 1 ↔ f x = x := by
   simp_rw [ext_iff, cycleOf_apply, one_apply]
   refine ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => ?_⟩
   by_cases hy : f y = y
@@ -137,32 +140,36 @@ theorem cycleOf_eq_one_iff (f : Perm α) : cycleOf f x = 1 ↔ f x = x := by
 #align equiv.perm.cycle_of_eq_one_iff Equiv.Perm.cycleOf_eq_one_iff
 
 @[simp]
-theorem cycleOf_self_apply (f : Perm α) (x : α) : cycleOf f (f x) = cycleOf f x :=
+theorem cycleOf_self_apply (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
+    cycleOf f (f x) = cycleOf f x :=
   (sameCycle_apply_right.2 SameCycle.rfl).symm.cycleOf_eq
 #align equiv.perm.cycle_of_self_apply Equiv.Perm.cycleOf_self_apply
 
 @[simp]
-theorem cycleOf_self_apply_pow (f : Perm α) (n : ℕ) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x :=
+theorem cycleOf_self_apply_pow (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
+    cycleOf f ((f ^ n) x) = cycleOf f x :=
   SameCycle.rfl.pow_left.cycleOf_eq
 #align equiv.perm.cycle_of_self_apply_pow Equiv.Perm.cycleOf_self_apply_pow
 
 @[simp]
-theorem cycleOf_self_apply_zpow (f : Perm α) (n : ℤ) (x : α) :
+theorem cycleOf_self_apply_zpow (f : Perm α) [DecidableRel f.SameCycle] (n : ℤ) (x : α) :
     cycleOf f ((f ^ n) x) = cycleOf f x :=
   SameCycle.rfl.zpow_left.cycleOf_eq
 #align equiv.perm.cycle_of_self_apply_zpow Equiv.Perm.cycleOf_self_apply_zpow
 
-protected theorem IsCycle.cycleOf (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f := by
+protected theorem IsCycle.cycleOf [DecidableEq α] (hf : IsCycle f) :
+    cycleOf f x = if f x = x then 1 else f := by
   by_cases hx : f x = x
   · rwa [if_pos hx, cycleOf_eq_one_iff]
   · rwa [if_neg hx, hf.cycleOf_eq]
 #align equiv.perm.is_cycle.cycle_of Equiv.Perm.IsCycle.cycleOf
 
-theorem cycleOf_one (x : α) : cycleOf 1 x = 1 :=
-  (cycleOf_eq_one_iff 1).mpr rfl
+theorem cycleOf_one [DecidableRel (1 : Perm α).SameCycle] (x : α) :
+    cycleOf 1 x = 1 := (cycleOf_eq_one_iff 1).mpr rfl
 #align equiv.perm.cycle_of_one Equiv.Perm.cycleOf_one
 
-theorem isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x) :=
+theorem isCycle_cycleOf (f : Perm α) [DecidableRel f.SameCycle] (hx : f x ≠ x) :
+    IsCycle (cycleOf f x) :=
   have : cycleOf f x x ≠ x := by rwa [SameCycle.rfl.cycleOf_apply]
   (isCycle_iff_sameCycle this).2 @fun y =>
     ⟨fun h => mt h.apply_eq_self_iff.2 this, fun h =>
@@ -175,29 +182,32 @@ theorem isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x) :
 #align equiv.perm.is_cycle_cycle_of Equiv.Perm.isCycle_cycleOf
 
 @[simp]
-theorem two_le_card_support_cycleOf_iff : 2 ≤ card (cycleOf f x).support ↔ f x ≠ x := by
+theorem two_le_card_support_cycleOf_iff [DecidableEq α] [Fintype α] :
+    2 ≤ card (cycleOf f x).support ↔ f x ≠ x := by
   refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
   contrapose! h
   rw [← cycleOf_eq_one_iff] at h
   simp [h]
 #align equiv.perm.two_le_card_support_cycle_of_iff Equiv.Perm.two_le_card_support_cycleOf_iff
 
-@[simp] lemma support_cycleOf_nonempty : (cycleOf f x).support.Nonempty ↔ f x ≠ x := by
+@[simp] lemma support_cycleOf_nonempty [DecidableEq α] [Fintype α] :
+    (cycleOf f x).support.Nonempty ↔ f x ≠ x := by
   rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]
   exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
 #align equiv.perm.card_support_cycle_of_pos_iff Equiv.Perm.support_cycleOf_nonempty
 
 @[deprecated support_cycleOf_nonempty (since := "2024-06-16")]
-theorem card_support_cycleOf_pos_iff : 0 < card (cycleOf f x).support ↔ f x ≠ x := by
+theorem card_support_cycleOf_pos_iff [DecidableEq α] [Fintype α] :
+    0 < card (cycleOf f x).support ↔ f x ≠ x := by
   rw [card_pos, support_cycleOf_nonempty]
 
-theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) (n : ℕ) (x : α) :
+theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
     (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x := by
   rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
 #align equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply Equiv.Perm.pow_mod_orderOf_cycleOf_apply
 
-theorem cycleOf_mul_of_apply_right_eq_self (h : Commute f g) (x : α) (hx : g x = x) :
-    (f * g).cycleOf x = f.cycleOf x := by
+theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel (f * g).SameCycle]
+    (h : Commute f g) (x : α) (hx : g x = x) : (f * g).cycleOf x = f.cycleOf x := by
   ext y
   by_cases hxy : (f * g).SameCycle x y
   · obtain ⟨z, rfl⟩ := hxy
@@ -210,25 +220,29 @@ theorem cycleOf_mul_of_apply_right_eq_self (h : Commute f g) (x : α) (hx : g x
     simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
 #align equiv.perm.cycle_of_mul_of_apply_right_eq_self Equiv.Perm.cycleOf_mul_of_apply_right_eq_self
 
-theorem Disjoint.cycleOf_mul_distrib (h : f.Disjoint g) (x : α) :
+theorem Disjoint.cycleOf_mul_distrib [DecidableRel (f * g).SameCycle]
+    [DecidableRel (g * f).SameCycle]  (h : f.Disjoint g) (x : α) :
     (f * g).cycleOf x = f.cycleOf x * g.cycleOf x := by
   cases' (disjoint_iff_eq_or_eq.mp h) x with hfx hgx
   · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
   · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
 #align equiv.perm.disjoint.cycle_of_mul_distrib Equiv.Perm.Disjoint.cycleOf_mul_distrib
 
-theorem support_cycleOf_eq_nil_iff : (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp
+theorem support_cycleOf_eq_nil_iff [DecidableEq α] [Fintype α] :
+    (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp
 #align equiv.perm.support_cycle_of_eq_nil_iff Equiv.Perm.support_cycleOf_eq_nil_iff
 
-theorem support_cycleOf_le (f : Perm α) (x : α) : support (f.cycleOf x) ≤ support f := by
+theorem support_cycleOf_le [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
+    support (f.cycleOf x) ≤ support f := by
   intro y hy
   rw [mem_support, cycleOf_apply] at hy
   split_ifs at hy
   · exact mem_support.mpr hy
   · exact absurd rfl hy
 #align equiv.perm.support_cycle_of_le Equiv.Perm.support_cycleOf_le
 
-theorem mem_support_cycleOf_iff : y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f := by
+theorem mem_support_cycleOf_iff [DecidableEq α] [Fintype α] :
+    y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f := by
   by_cases hx : f x = x
   · rw [(cycleOf_eq_one_iff _).mpr hx]
     simp [hx]
@@ -241,31 +255,35 @@ theorem mem_support_cycleOf_iff : y ∈ support (f.cycleOf x) ↔ SameCycle f x
     · simpa [hx] using hy
 #align equiv.perm.mem_support_cycle_of_iff Equiv.Perm.mem_support_cycleOf_iff
 
-theorem mem_support_cycleOf_iff' (hx : f x ≠ x) : y ∈ support (f.cycleOf x) ↔ SameCycle f x y := by
+theorem mem_support_cycleOf_iff' (hx : f x ≠ x) [DecidableEq α] [Fintype α] :
+    y ∈ support (f.cycleOf x) ↔ SameCycle f x y := by
   rw [mem_support_cycleOf_iff, and_iff_left (mem_support.2 hx)]
 #align equiv.perm.mem_support_cycle_of_iff' Equiv.Perm.mem_support_cycleOf_iff'
 
-theorem SameCycle.mem_support_iff (h : SameCycle f x y) : x ∈ support f ↔ y ∈ support f :=
+theorem SameCycle.mem_support_iff {f} [DecidableEq α] [Fintype α] (h : SameCycle f x y) :
+    x ∈ support f ↔ y ∈ support f :=
   ⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
     support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩
 #align equiv.perm.same_cycle.mem_support_iff Equiv.Perm.SameCycle.mem_support_iff
 
-theorem pow_mod_card_support_cycleOf_self_apply (f : Perm α) (n : ℕ) (x : α) :
-    (f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x := by
+theorem pow_mod_card_support_cycleOf_self_apply [DecidableEq α] [Fintype α]
+    (f : Perm α) (n : ℕ) (x : α) : (f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x := by
   by_cases hx : f x = x
   · rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
   · rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
       pow_mod_orderOf]
 #align equiv.perm.pow_mod_card_support_cycle_of_self_apply Equiv.Perm.pow_mod_card_support_cycleOf_self_apply
 
 /-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle. -/
-theorem isCycle_cycleOf_iff (f : Perm α) : IsCycle (cycleOf f x) ↔ f x ≠ x := by
+theorem isCycle_cycleOf_iff (f : Perm α) [DecidableRel f.SameCycle] :
+    IsCycle (cycleOf f x) ↔ f x ≠ x := by
   refine ⟨fun hx => ?_, f.isCycle_cycleOf⟩
   rw [Ne, ← cycleOf_eq_one_iff f]
   exact hx.ne_one
 #align equiv.perm.is_cycle_cycle_of_iff Equiv.Perm.isCycle_cycleOf_iff
 
-theorem isCycleOn_support_cycleOf (f : Perm α) (x : α) : f.IsCycleOn (f.cycleOf x).support :=
+theorem isCycleOn_support_cycleOf [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
+    f.IsCycleOn (f.cycleOf x).support :=
   ⟨f.bijOn <| by
     refine fun _ ↦ ⟨fun h ↦ mem_support_cycleOf_iff.2 ?_, fun h ↦ mem_support_cycleOf_iff.2 ?_⟩
     · exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff.1 h).1,
@@ -278,14 +296,14 @@ theorem isCycleOn_support_cycleOf (f : Perm α) (x : α) : f.IsCycleOn (f.cycleO
         exact ha.1.symm.trans hb.1⟩
 #align equiv.perm.is_cycle_on_support_cycle_of Equiv.Perm.isCycleOn_support_cycleOf
 
-theorem SameCycle.exists_pow_eq_of_mem_support (h : SameCycle f x y) (hx : x ∈ f.support) :
-    ∃ i < (f.cycleOf x).support.card, (f ^ i) x = y := by
+theorem SameCycle.exists_pow_eq_of_mem_support {f} [DecidableEq α] [Fintype α] (h : SameCycle f x y)
+    (hx : x ∈ f.support) : ∃ i < (f.cycleOf x).support.card, (f ^ i) x = y := by
   rw [mem_support] at hx
   exact Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf x)
     (by rw [mem_support_cycleOf_iff' hx]) (by rwa [mem_support_cycleOf_iff' hx])
 #align equiv.perm.same_cycle.exists_pow_eq_of_mem_support Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support
 
-theorem SameCycle.exists_pow_eq (f : Perm α) (h : SameCycle f x y) :
+theorem SameCycle.exists_pow_eq [DecidableEq α] [Fintype α] (f : Perm α) (h : SameCycle f x y) :
     ∃ i : ℕ, 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y := by
   by_cases hx : x ∈ f.support
   · obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx