Proving the value of exp (S_5)

Stream: mathlib4

[Ruben Van de Velde]

I had hoped that I'd be able to brute-force this with decide, but it reaches the maximum recursion depth. Is there any hope to get this to work?

import Mathlib.GroupTheory.Exponent
import Mathlib.FieldTheory.Finite.Basic

theorem Monoid.ExponentExists.ofFintype (α : Type*) [Group α] [Fintype α] : Monoid.ExponentExists α := by
  simp only [Monoid.ExponentExists]
  refine ⟨Fintype.card α, Fintype.card_pos, fun g => ?_⟩
  rw [← orderOf_dvd_iff_pow_eq_one]
  exact orderOf_dvd_card

example : Monoid.exponent (Equiv.Perm (Fin 5)) = 60 := by
  have := Monoid.ExponentExists.ofFintype (Equiv.Perm (Fin 5))
  rw [Monoid.exponent, dif_pos this]
  convert (Nat.find_eq_iff this).mpr ?_
  simp only [Nat.zero_lt_succ, true_and, not_and, not_forall]
  decide

The goal does seem a little harsh at that point:

(∀ (g : Equiv.Perm (Fin 5)), g ^ 60 = 1) ∧ ∀ n < 60, 0 < n → ∃ x, ¬x ^ n = 1

[Ruben Van de Velde]

#eval Nat.find (Monoid.ExponentExists.ofFintype (Equiv.Perm (Fin 5)))

is instant, but doesn't really count as a proof

[Ruben Van de Velde]

Alternatively, suggestions for a better proof are also helpful. This is an exercise from a class I took when I was younger and smarter, and I somehow doubt that "brute force" was the intended solution

[Riccardo Brasca]

The math proof I would follow is the fact that if there is g such that g^60 ≠ 1 then the order of g would be 120, so the group would be cyclic.

[Riccardo Brasca]

And to prove that anything smaller than 60 (wrt to division) cannot work one has to find elements of order 3, 5 and 4, but this is easy.

[Riccardo Brasca]

I guess that the general result that the exponent is the lcm of 1,2,..., n is doable.

[Eric Wieser]

You can locally change the recursion depth

[Ruben Van de Velde]

Yeah, that works up to four, but not for 5

[Eric Rodriguez]

docs3#monoid.lcm_order_eq_exponent should be a good start for the general result no?

[Riccardo Brasca]

Do we have the fact that any permutation can be written as the product of disjoint cycles? This is the main point.

[Riccardo Brasca]

In any case the specific case of S_5 should really be easy: 60 divides the exponent because of Eric's theorem and the existence of elements of order 3,4 and 5. Then, the exponent divides the order of the group (this is probably there, or it should be added), so there are only two possibilities. If 60 doesn't work then there is an element of order 120.

[Ruben Van de Velde]

Can't find it, but it's easy:

theorem Monoid.exponent_dvd_card {G : Type*} [Group G] [Fintype G] :
    Monoid.exponent G ∣ Fintype.card G :=
  Monoid.exponent_dvd_of_forall_pow_eq_one G (Fintype.card G) <| fun _ =>
    orderOf_dvd_iff_pow_eq_one.mp orderOf_dvd_card

[Riccardo Brasca]

We have a lot of stuff about permutations, the general case should really be doable.

[Yakov Pechersky]

We have that any perm can be written as a product of disjoint cycles

[Yakov Pechersky]

One sec

[Riccardo Brasca]

everything is in Mathlib.GroupTheory.Perm.Cycle.Type and friends

[Yakov Pechersky]

docs#Equiv.Perm.cycleFactorsFinset

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Type.html#Equiv.Perm.lcm_cycleType is also presumably useful

[Riccardo Brasca]

Yes, all the maths is there. But I don't see a simple way of defining a cycle.

[Riccardo Brasca]

I mean, explictely.

[Riccardo Brasca]

Ah, we have docs#Fin.cycleRange

[Ruben Van de Velde]

There's also the c[(1 : Fin 4), 3, 2] notation

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Concrete.html#Equiv.Perm.%C2%ABtermC[_,]%C2%BB

[Riccardo Brasca]

Yes, but it seems really annoying to work with.

[Riccardo Brasca]

I playing with your problem, and I am stuck at proving that

set σ := Fin.cycleRange (3 : Fin 5) with σdef
have σsupp : Equiv.Perm.support σ = {1, 2, 3} := by

[Riccardo Brasca]

in principle it is easy, but I am looking for a short proof

[Riccardo Brasca]

Ah, Fin 5 starts at 0 :sweat_smile:

[Yakov Pechersky]

Riccardo, can you share more about what's frustrating in the c[...] notation?

[Riccardo Brasca]

Well, I forgot that Fin 5 starts at 0, so maybe that was the reason why simp/exact? and stuff like that didn't work. Anyway I wanted to prove that order of c[0,1,2] is 3.

[Riccardo Brasca]

And this is easy for Fin.cycleRange (2 : Fin 5)

[Yakov Pechersky]

Here's an example of proving on something concrete:

import Mathlib.GroupTheory.Perm.Cycle.Concrete

open Equiv.Perm

example : Equiv.Perm.cycleType c[(1 : Fin 5), 2, 0] = {3} := by
  rw [Equiv.Perm.cycleType,
      cycleFactorsFinset_eq_singleton_self_iff.mpr (Cycle.isCycle_formPerm _ _ _)]
  dsimp only [Finset.singleton_val, Multiset.map_singleton, Function.comp_apply]
  rw [Cycle.support_formPerm]
  all_goals decide

[Yakov Pechersky]

I think apply? times out because of too many Equiv.Perm lemmas (?)

[Riccardo Brasca]

I've done half of @Ruben Van de Velde 's exercice

import Mathlib.GroupTheory.Exponent
import Mathlib.FieldTheory.Finite.Basic
import Mathlib.GroupTheory.Perm.Cycle.Concrete

theorem Monoid.ExponentExists.ofFintype (α : Type*) [Group α] [Fintype α] : Monoid.ExponentExists α := by
  simp only [Monoid.ExponentExists]
  refine ⟨Fintype.card α, Fintype.card_pos, fun g => ?_⟩
  rw [← orderOf_dvd_iff_pow_eq_one]
  exact orderOf_dvd_card

example : Monoid.exponent (Equiv.Perm (Fin 5)) = 60 := by
  set e := Monoid.exponent (Equiv.Perm (Fin 5)) with he
  apply dvd_antisymm
  · sorry
  · suffices (((3 : ℕ) : ℤ) ∣ e) ∧ (((4 : ℕ) : ℤ) ∣ e) ∧ (((5 : ℕ) : ℤ) ∣ e) by
      rw [← Int.coe_nat_dvd, show ((60 : ℕ) : ℤ) = ((12 : ℕ) : ℤ) * ((5 : ℕ) : ℤ) by norm_num]
      apply IsCoprime.mul_dvd
      · rw [Nat.isCoprime_iff_coprime]
        norm_num
      · rw [show ((12 : ℕ) : ℤ) = ((3 : ℕ) : ℤ) * ((4 : ℕ) : ℤ) by norm_num]
        apply IsCoprime.mul_dvd
        · rw [Nat.isCoprime_iff_coprime]
          norm_num
        · exact this.1
        · exact this.2.1
      · exact this.2.2
    constructor
    · rw [he, ← Monoid.lcm_order_eq_exponent]
      let σ := Fin.cycleRange (2 : Fin 5)
      have σsupp : Equiv.Perm.support σ = Finset.filter (fun x ↦ x ≤ 2)
          (Finset.univ : Finset (Fin 5)) := by
        ext x
        constructor
        · intro hx
          by_cases Hx : x ≤ 2
          · exact hx
          · simp [Equiv.Perm.mem_support, ne_eq, Fin.cycleRange_of_gt (not_le.1 Hx)] at hx
        · intro hx
          by_cases Hx : x ≤ 2
          · by_cases Hx' : x = 2
            · simp [Hx']
              decide
            · simp [Fin.cycleRange_of_le Hx, Hx']
          · simp [Hx] at hx
      have σcycl : Equiv.Perm.IsCycle σ := by
        apply Fin.isCycle_cycleRange
        intro h
        have : (2 : Fin 5) ≠ 0 := by decide
        exact this h
      have hσ : orderOf σ = 3 := by
        rw [Equiv.Perm.IsCycle.orderOf σcycl, σsupp]
        decide
      rw [Int.coe_nat_dvd, ← hσ]
      exact Finset.dvd_lcm (Finset.mem_univ _)
    constructor
    · rw [he, ← Monoid.lcm_order_eq_exponent]
      let σ := Fin.cycleRange (3 : Fin 5)
      have σsupp : Equiv.Perm.support σ = Finset.filter (fun x ↦ x ≤ 3)
          (Finset.univ : Finset (Fin 5)) := by
        ext x
        constructor
        · intro hx
          by_cases Hx : x ≤ 3
          · exact hx
          · simp [Equiv.Perm.mem_support, ne_eq, Fin.cycleRange_of_gt (not_le.1 Hx)] at hx
        · intro hx
          by_cases Hx : x ≤ 3
          · by_cases Hx' : x = 3
            · simp [Hx']
              decide
            · simp [Fin.cycleRange_of_le Hx, Hx']
          · simp [Hx] at hx
      have σcycl : Equiv.Perm.IsCycle σ := by
        apply Fin.isCycle_cycleRange
        intro h
        have : (3 : Fin 5) ≠ 0 := by decide
        exact this h
      have hσ : orderOf σ = 4 := by
        rw [Equiv.Perm.IsCycle.orderOf σcycl, σsupp]
        decide
      rw [Int.coe_nat_dvd, ← hσ]
      exact Finset.dvd_lcm (Finset.mem_univ _)
    · rw [he, ← Monoid.lcm_order_eq_exponent]
      let σ := Fin.cycleRange (Fin.last 4)
      have σsupp : Equiv.Perm.support σ = (Finset.univ : Finset (Fin 5)) := by simp
      have σcycl : Equiv.Perm.IsCycle σ := by
        apply Fin.isCycle_cycleRange
        intro h
        have : (4 : Fin 5) ≠ 0 := by decide
        exact this h
      have hσ : orderOf σ = 5 := by
        rw [Equiv.Perm.IsCycle.orderOf σcycl, σsupp]
        decide
      rw [Int.coe_nat_dvd, ← hσ]
      convert Finset.dvd_lcm (Finset.mem_univ _)
      infer_instance
 ```

[Riccardo Brasca]

Extracting the fact that Equiv.Perm.support (Fin.cycleRange ...) is what it is supposed to be (and hence the order is done) would shorten the proof a lot.

[Yakov Pechersky]

One example of that in a concrete context:

  have : (c[(1 : Fin 5), 2, 0]).support = {1, 2, 0} := by decide

[Yakov Pechersky]

agreed that for the more abstract constructor, a factored out lemma makes sense

[Riccardo Brasca]

Yakov Pechersky said:

One example of that in a concrete context:

  have : (c[(1 : Fin 5), 2, 0]).support = {1, 2, 0} := by decide

If decide works here forget about my complain. It is the first thing I tried and it didn't work because my statement was false.

[Ruben Van de Velde]

Looks a bit simpler without the casts:

example : Monoid.exponent (Equiv.Perm (Fin 5)) = 60 := by
  set e := Monoid.exponent (Equiv.Perm (Fin 5)) with he
  apply dvd_antisymm
  · sorry
  · suffices (3 ∣ e) ∧ (4 ∣ e) ∧ (5 ∣ e) by
      rw [show 60 = 12 * 5 by norm_num]
      apply Nat.Coprime.mul_dvd_of_dvd_of_dvd
      · norm_num
      · rw [show 12 = 3 * 4 by norm_num]
        apply Nat.Coprime.mul_dvd_of_dvd_of_dvd
        · norm_num
        · exact this.1
        · exact this.2.1
      · exact this.2.2
    constructor
    · rw [he, ← Monoid.lcm_order_eq_exponent]
      let σ := Fin.cycleRange (2 : Fin 5)
      have σsupp : Equiv.Perm.support σ = Finset.filter (fun x ↦ x ≤ 2)
          (Finset.univ : Finset (Fin 5)) := by
        ext x
        constructor
        · intro hx
          by_cases Hx : x ≤ 2
          · exact hx
          · simp [Equiv.Perm.mem_support, ne_eq, Fin.cycleRange_of_gt (not_le.1 Hx)] at hx
        · intro hx
          by_cases Hx : x ≤ 2
          · by_cases Hx' : x = 2
            · simp [Hx']
              decide
            · simp [Fin.cycleRange_of_le Hx, Hx']
          · simp [Hx] at hx
      have σcycl : Equiv.Perm.IsCycle σ := by
        apply Fin.isCycle_cycleRange
        intro h
        have : (2 : Fin 5) ≠ 0 := by decide
        exact this h
      have hσ : orderOf σ = 3 := by
        rw [Equiv.Perm.IsCycle.orderOf σcycl, σsupp]
        decide
      rw [← hσ]
      exact Finset.dvd_lcm (Finset.mem_univ _)
    constructor
    · rw [he, ← Monoid.lcm_order_eq_exponent]
      let σ := Fin.cycleRange (3 : Fin 5)
      have σsupp : Equiv.Perm.support σ = Finset.filter (fun x ↦ x ≤ 3)
          (Finset.univ : Finset (Fin 5)) := by
        ext x
        constructor
        · intro hx
          by_cases Hx : x ≤ 3
          · exact hx
          · simp [Equiv.Perm.mem_support, ne_eq, Fin.cycleRange_of_gt (not_le.1 Hx)] at hx
        · intro hx
          by_cases Hx : x ≤ 3
          · by_cases Hx' : x = 3
            · simp [Hx']
              decide
            · simp [Fin.cycleRange_of_le Hx, Hx']
          · simp [Hx] at hx
      have σcycl : Equiv.Perm.IsCycle σ := by
        apply Fin.isCycle_cycleRange
        intro h
        have : (3 : Fin 5) ≠ 0 := by decide
        exact this h
      have hσ : orderOf σ = 4 := by
        rw [Equiv.Perm.IsCycle.orderOf σcycl, σsupp]
        decide
      rw [← hσ]
      exact Finset.dvd_lcm (Finset.mem_univ _)
    · rw [he, ← Monoid.lcm_order_eq_exponent]
      let σ := Fin.cycleRange (Fin.last 4)
      have σsupp : Equiv.Perm.support σ = (Finset.univ : Finset (Fin 5)) := by simp
      have σcycl : Equiv.Perm.IsCycle σ := by
        apply Fin.isCycle_cycleRange
        intro h
        have : (4 : Fin 5) ≠ 0 := by decide
        exact this h
      have hσ : orderOf σ = 5 := by
        rw [Equiv.Perm.IsCycle.orderOf σcycl, σsupp]
        decide
      rw [← hσ]
      convert Finset.dvd_lcm (Finset.mem_univ _)
      infer_instance

(though we should rename Nat.Coprime.mul_dvd_of_dvd_of_dvd to match IsCoprime.mul.dvd)

[Riccardo Brasca]

I didn't try to keep it short :D Anyway this essentially proves that lcm 1, 2,..., n divides the exponent, and we should add this general result