cycle notation

Stream: maths

[Johan Commelin]

Challenge: make the most comfy-to-use cycle notation. This is inspired by #7453.
Here is what I have so far. (I would love to have something like mk_cycle in mathlib.)

section vector_index

variables {α : Type*}

def vector.find_index (p : α → Prop) [decidable_pred p] : Π {n}, vector α n → option (fin n)
| 0     ⟨[],     rfl⟩ := none
| (n+1) ⟨(a::l), hl⟩  :=
if p a then ↑(0 : fin (n+1))
else option.map fin.succ (vector.find_index ⟨l, nat.succ_injective hl⟩)

def vector.index_of [decidable_eq α] {n : ℕ} (v : vector α n) (a : α) :
  option (fin n) :=
v.find_index (eq a)

end vector_index

open equiv

def equiv.perm.mk_cycle (n : ℕ) [inhabited (fin n)]
  (σ : list (fin n)) (h : σ.length = n . tactic.interactive.refl)
  (σ_inv : fin n → fin n := option.iget ∘ vector.index_of ⟨σ, h⟩)
  (h1 : ∀ i, σ_inv (vector.nth ⟨σ, h⟩ i) = i . tactic.exact_dec_trivial)
  (h2 : ∀ i, vector.nth ⟨σ, h⟩ (σ_inv i) = i . tactic.exact_dec_trivial) :
  perm (fin n) :=
⟨vector.nth ⟨σ, h⟩, σ_inv, h1, h2⟩

open equiv.perm

/-- A 3-cycle -/
def σ1 := mk_cycle 5 [0, 1, 3, 4, 2]

/-- A (2,2)-cycle -/
def σ2 := mk_cycle 5 [3, 4, 2, 0, 1]

/-- A 3-cycle -/
def σ3 := mk_cycle 5 [2, 1, 4, 3, 0]

lemma mem_derived_series (n : ℕ) : σ1 ∈ derived_series (equiv.perm (fin 5)) n :=
begin
  induction n with n ih,
  { exact mem_top σ1 },
  rw show σ1 = σ3 * ((σ2 * σ1 * σ2⁻¹) * σ1 * (σ2 * σ1 * σ2⁻¹)⁻¹ * σ1⁻¹) * σ3⁻¹,
  { ext, dec_trivial! },
  exact (derived_series_normal _ _).conj_mem _
    (general_commutator_containment _ _ ((derived_series_normal _ _).conj_mem _ ih _) ih) _,
end

lemma not_solvable' : ¬ is_solvable (equiv.perm (fin 5)) :=
have σ1 ≠ 1, by { rw [ne.def, equiv.ext_iff], dec_trivial },
not_solvable_of_mem_derived_series this mem_derived_series

[Yakov Pechersky]

I've been working a lot towards this

[Yakov Pechersky]

That's what my form_perm PR is for

let x : equiv.perm (fin 5) := form_perm [0, 1, 2]
let y : equiv.perm (fin 5) := (form_perm [0, 3]) * (form_perm [1, 4])
let z : equiv.perm (fin 5) := form_perm [1, 3]

[Yakov Pechersky]

With other branches working towards a cycle type that is the quotient of lists by cyclic permutations

[Yakov Pechersky]

#7451

[Johan Commelin]

This looks really sweet! I haven't been following the PR stream close enough apparently. Great job!

[Aaron Anderson]

There’s still a question of what the notation looks like