Cycle Types

Stream: Berkeley Lean Seminar

[Thomas Browning]

@Aaron Anderson Here are a few questions about cycle types:
1) Do you want to include 1's in the cycle type or not?
2) Should the cycle type be a partition, a multiset, a sorted list, or something else?

[Aaron Anderson]

There should certainly be a partition version of it, and I think there are advantages to including 1s.

[Aaron Anderson]

(If we include 1s, it should be very easy to make it a partition).

[Thomas Browning]

I agree that there advantages to including 1's. One disadvantage of including 1's is that it makes it painful to state things like "is_swap corresponds to this cycle type" or "an element of order p has a cycle type of this form"

[Thomas Browning]

Would it make sense to have two versions? A partition including 1's, and something (maybe a multiset or sorted list?) not including 1's.

[Aaron Anderson]

I'd probably say a multiset not including 1s and then a partition including 1s makes sense.

[Aaron Anderson]

If you derive it from same_cycle, you get 1s, and if you derive it from cycle_factors, you get no 1s.

[Aaron Anderson]

The advantage I see to including 1s is that it might make it easier to produce the bijection between cycles that I think you need for conjugacy.

[Aaron Anderson]

However, @Yakov Pechersky's work in #6959 may obviate the need to consider the 1s at all in the conjugacy argument.

[Thomas Browning]

I hadn't though about going from same_cycle (although I can't quite see how to do it nicely). If you go from cycle_factors, is there a nice way to avoid the linear_order assumption?

[Aaron Anderson]

On one of my recent PRs I threw in a trunc version...

[Aaron Anderson]

Yeah, trunc_cycle_factors in #6951

[Aaron Anderson]

We should be able to use that to computably define a cycle_type multiset.

[Thomas Browning]

Ok, I'll take a stab at this today, and I'll let you know when I've got something.

[Aaron Anderson]

As far as the partition, I might even suggest saving that for when we have conjugacy (and conjugacy classes, from #6896) and defining an equiv between conj_classes and partitions.

[Aaron Anderson]

As far as proving that the same cycle type implies conjugacy, I feel like we can maybe manage to prove it for cycles, and inductively for products of disjoint permutations.

[Thomas Browning]

@Aaron Anderson I've made a start at constructing cycles_type from trunc_cycle_factors, from which it shouldn't be too hard to make the partition. It look doable, but let me know if you see an easier to prove that the cycle_type doesn't depend on the choice of
cycle_factors.

[Aaron Anderson]

Where are you working on this?

[Aaron Anderson]

I think we want the lemma anyway that any two lists that satisfy the requirements of cycle factors are related by list.perm.

[Aaron Anderson]

That should be enough to appease the trunc, and it is a nicer place to put the sorry, but Idk how to prove it yet

[Thomas Browning]

ah, sorry, I forgot the link: https://github.com/leanprover-community/mathlib/compare/cycle_type

[Thomas Browning]

Good point that we should prove the permutation fact

[Aaron Anderson]

Actually, not that sure it does help, because we know the lists each satisfy list.erase_dup, so we can turn them into finsets and use finset.ext. I think we need to show that a member of one is a member of the other anyway.

[Thomas Browning]

@Aaron Anderson Would it make sense to prove something like this:

lemma main_theorem
  (l : list (perm α))
  (h1 : ∀ σ : perm α, σ ∈ l → σ.is_cycle)
  (h2 : l.pairwise disjoint)
  (c : perm α) (a : α) (hc : c a ≠ a) :
  c ∈ l ↔ l.prod.cycle_of a = c :=

[Aaron Anderson]

Yes, then you can just hit it with list.perm_ext

[Thomas Browning]

I just pushed this approach to the branch. There's just one sorry left, but it's a bit of a doozy.

[Thomas Browning]

lemma thm2
  (σ τ : perm α)
  (h : disjoint σ τ)
  (c : perm α)
  (a : α)
  (hc : c a ≠ a) :
  (σ * τ).cycle_of a = c ↔ (σ.cycle_of a = c ∨ τ.cycle_of a = c) :=
begin
  sorry
end

[Thomas Browning]

@Aaron Anderson The branch now is now sorry-free
https://github.com/leanprover-community/mathlib/compare/cycle_type

[Thomas Browning]

#6999

[Aaron Anderson]

Check out branch#cycle_conj

[Aaron Anderson]

I have a proof (although some things need to be cleaned up) that two cycles of the same size are conjugate

[Aaron Anderson]

#7024

[Thomas Browning]

@Aaron Anderson Great! I'm wondering whether we can get the full conjugate/partition theorem from the induction lemma?

[Aaron Anderson]

If you look at my proof, it basically glues two equivs together

[Thomas Browning]

Actually, so I'm curious. Do you think that this result will be useful in proving the full theorem? I'm starting to get worried that a cycle induction strategy won't work.

[Aaron Anderson]

For two disjoint perms, you could glue together equivs between their supports with one between the rest of the elements

[Aaron Anderson]

I think it will work.

[Thomas Browning]

Would that require passing permutations back and forth between subtypes? I'm worried that it might be a bit painful.

[Aaron Anderson]

Not more painful than the cycle proof, and I’m not sure I see a better option

[Thomas Browning]

Is it conceivable that you could prove a lemma along these lines?

Let a,b,c,d be permutations. Assume a and b are disjoint, c and d are disjoint, a is conjugate to c, b is conjugate to d. Then a*b is conjugate to c*d.

[Aaron Anderson]

Yes, that’s what I had in mind.

[Thomas Browning]

If so, then you could make a plain induction work, without the need for any more subtype mess (outside of the proof of the lemma)

[Aaron Anderson]

I think the alternative is creating some other data structure that represents cycle notation

[Aaron Anderson]

I have that lemma proven at branch#disjoint_conj.

[Aaron Anderson]

Again, messy, and I should really think more about how I'm going to organize all of these random permutation facts and long proofs, but the statement is there in case you want to sorry it and work on proving the cycle_type induction.

[Yakov Pechersky]

Kevin just let me know about this stream! I've been doing some parallel/complementary work. I've been trying to make it possible to specify explicit perm cycles using lists. Here's a smattering of what I have:

lemma perm.commutes_of_disjoint (e₁ e₂ : equiv.perm α)
  (h : _root_.disjoint (function.fixed_points e₁)ᶜ (function.fixed_points e₂)ᶜ) :
  commute e₁ e₂ :=
begin
  ext t,
  by_cases ht₁ : function.is_fixed_pt e₁ t;
  by_cases ht₂ : function.is_fixed_pt e₂ t,
  { simp [ht₁.eq, ht₂.eq] },
  { have : function.is_fixed_pt e₁ (e₂ t),
      { rw [←function.mem_fixed_points, ←set.not_mem_compl_iff],
        refine set.mem_disjoint_imp _ h.symm,
        rw [set.mem_compl_iff, function.mem_fixed_points],
        contrapose! ht₂,
        rw function.is_fixed_pt at ht₂ ⊢,
        apply e₂.injective,
        exact ht₂ },
    simp [ht₁.eq, this.eq] },
  { -- how does one use wlog to skip this?
    have : function.is_fixed_pt e₂ (e₁ t),
      { rw [←function.mem_fixed_points, ←set.not_mem_compl_iff],
        refine set.mem_disjoint_imp _ h,
        rw [set.mem_compl_iff, function.mem_fixed_points],
        contrapose! ht₁,
        rw function.is_fixed_pt at ht₁ ⊢,
        apply e₁.injective,
        exact ht₁ },
    simp [ht₂.eq, this.eq] },
  { exfalso,
    exact h (set.mem_inter ht₁ ht₂) }
end

def is_rotated (l l' : list α) : Prop := ∃ n, l.rotate n = l'

infixr ` ~r `:1000 := is_rotated

def cycle (α : Type*) : Type* := quotient (@is_rotated.setoid α)

[Yakov Pechersky]

With the goal of proving things like:

lemma form_perm_rotation_invariant (n : ℕ) (l : list α) (h : nodup l) :
  form_perm (l.rotate n) = form_perm l := sorry

lemma is_cycle_form_perm (l : list α) (x y : α) (h : nodup (x :: y :: l)) :
  is_cycle (form_perm (x :: y :: l)) := sorry

[Yakov Pechersky]

(not including a lot of API)

[Yakov Pechersky]

Which, looking at your code, is similar to cycle_type

[Yakov Pechersky]

If you'd like any contribution or if you have any suggestions on refactoring, let me know!

[Eric Wieser]

docs#set.not_mem_compl_iff and docs#set.mem_disjoint_imp seem not to exist

[Yakov Pechersky]

Yeah, I just wanted to share a snippet of what I had.

lemma set.mem_disjoint_imp {α : Type*} {s t : set α} {x : α} (h : x ∈ s) (hd : disjoint s t) :
  x ∉ t :=
λ ht, hd (set.mem_inter h ht)

lemma set.not_mem_compl_iff {α : Type*} (s : set α) (x : α) : x ∉ sᶜ ↔ x ∈ s := set.not_not_mem

[Aaron Anderson]

Hrm, I think that means we need to do a lot more coordination work, @Yakov Pechersky

[Aaron Anderson]

I'm not sure I see the benefit of this version of perm.commutes_of_disjoint over the existing proof of perm.disjoint.mul_comm

[Aaron Anderson]

but if you can represent cycles as lists, then that probably means you can give a much more intuitive proof of the conjugacy results

[Yakov Pechersky]

I haven't merged any of your branches -- just discovered them!

[Yakov Pechersky]

Is there a particular PR or branch I should rebase on?

[Aaron Anderson]

I'm not sure, equiv.perm.disjoint.mul_commis in master, just in the group_theory.perm.sign file, where it maybe shouldn't be

[Aaron Anderson]

Most of my random-helpful-lemmas are in branch#card_support_perm

[Aaron Anderson]

which is #6951

[Aaron Anderson]

but the work on branch#cycle_conj (#7024) which I've improved at branch#disjoint_conj involves some subtype shenanigans and long composition chains of equivs

[Aaron Anderson]

and the goal is just to prove the result that two permutations with the same cycle type are conjugate

[Aaron Anderson]

which is a 1-line proof on paper

[Aaron Anderson]

and it might be possible to get closer to that 1-line proof, and perhaps skip the induction, if you have both permutations represented as products of disjoint cycles which are represented as lists

[Yakov Pechersky]

Yeah, and a perm cycle should be representable as

def form_perm : equiv.perm α :=
(zip_with equiv.swap l (l.rotate 1)).tail.prod

[Yakov Pechersky]

Where it behave as expected if nodup l

[Yakov Pechersky]

(Or just define it with erase_dup in there)

[Yakov Pechersky]

Then disjointedness has to do with a statement about some sublists being disjoint or not

[Aaron Anderson]

I guess my question is

[Aaron Anderson]

If I give you two lists of disjoint cycles, with the cycles represented as lists, and the lists of the lengths of the cycles are the same, how hard might it be to define the equiv mapping from the ith element of the jth cycle of one list to the ith element of the jth cycle of the other list?

[Yakov Pechersky]

Do you know that each of the cycle elements are paired in length?

[Aaron Anderson]

Yes, but I did a bad job of describing that condition.

[Yakov Pechersky]

Then it's just a stacked zip_with

[Aaron Anderson]

I'm not sure I follow. list.zip_with seems to be a tool for applying a binary function pointwise to two lists to get a third list.

[Aaron Anderson]

I'm trying to find a permutation f such that when I apply list.map f to every cycle element in the first list, I get the second list

[Aaron Anderson]

Because list.map will correspond to conjugation for a given cycle, as in lemma conjugation_of_cycle at https://isabelle.in.tum.de/website-Isabelle2018/dist/library/HOL/HOL-Algebra/Cycles.html

[Yakov Pechersky]

My first question is when you say "list of cycles" you mean { l : list (equiv.perm α) // ∀ p ∈ l, is_cycle p }?

[Aaron Anderson]

I mean an element of that, yes, or else a list of lists, such that each element represents a disjoint cycle (so I suppose, a list such that if you concatenated all the elements it'd be nodup)

[Yakov Pechersky]

Right. So I think trying to map element to element will be wonky because of the rotational invariance

[Yakov Pechersky]

So, if you have to map element to element, then you have to escape the rotational invariance, probably via choosing the lexicographically smallest representation of that cycle

[Aaron Anderson]

I think we can get around that. I don't need this to be computable, although having a computable version under extra assumptions would potentially be useful.

[Yakov Pechersky]

Ah. My goal has precisely been computability here, which is why I've been building "bottom-up" from lists

[Aaron Anderson]

Yeah, I can tell... that's why I tried to phrase it in terms of assuming we already have two lists of lists, rather than two lists of cycles.

[Aaron Anderson]

Assuming we've already got past that choice hurdle.

[Aaron Anderson]

There's still going to have to be choice involved, in order to map the fixed points of one permutation to the other.

[Aaron Anderson]

One conclusion I have is that I should probably recall (or reduce the scope of) #7024

[Yakov Pechersky]

I'm not too familiar with HOL syntax. Is this describing that conjugating a [perm represented by disjoint cycles] by a perm is equal to [perm represented by disjoint cycles, [each trans that perm]]?

[Aaron Anderson]

I believe it’s more like [perm represented by disjoint cycles, [each list.mapped by that perm]

[Aaron Anderson]

Proving that should probably be easy enough, but proving sufficient conditions for there to exist a perm that does that particular conjugation is harder

[Yakov Pechersky]

Right, each of the disjoint cycles is conjugated by that perm, if I understand correctly

[Yakov Pechersky]

So can't you prove that it's the case for one, so it's the care for all?

[Yakov Pechersky]

(which is your "easy to prove" statement)

[Aaron Anderson]

Actually, I have an idea for how to do the harder statement. To construct such a permutation, we first concatenate both lists of lists, and then pad them both with all the fixed points (using list.filter or something) so that the domain of our permutations is listed out twice. Then, using fintype.equiv_fin.of_forall_mem_list, we can construct a permutation that sends the ith entry of one list to the ith entry of the other.

[Yakov Pechersky]

Why should perm.support be defined solely for fintype?

[Yakov Pechersky]

Because re-reading the code, I see that my commute lemma above works for non-fintype too.

[Thomas Browning]

@Yakov Pechersky In general, the support of a permutation won't be a finset. But I suppose you could try to refactor support to be a set.

[Yakov Pechersky]

Yes, agreed that it can often be nonfinite. I have already started on the refactor

[Aaron Anderson]

@Thomas Browning, I have just one sorry at branch#disjoint_conj required to prove that the same cycle type implies conjugacy.

[Aaron Anderson]

We just need to show that if the cycle type of a permutation is m1 + m2, then it can be expressed as a product of disjoint permutations with cycle types m1 and m2.

[Aaron Anderson]

Given as you wrote up cycle_type, do you have any insight into what kind of (possibly induction) we want to do?

[Thomas Browning]

Can you induct on sigma, after reverting m1 and m2?

[Aaron Anderson]

I think I’m finding that cycle_induction_on should allow you to assume that one of your two disjoint permutations is a cycle. I keep trying to use trunc_cycle_factors to get that...

[Thomas Browning]

Ah, so would changing the induction lemma to this be better:

@[elab_as_eliminator] lemma cycle_induction_on [fintype β] (P : perm β → Prop) (σ : perm β)
  (base_one : P 1) (base_cycles : ∀ σ : perm β, σ.is_cycle → P σ)
  (induction_disjoint : ∀ σ τ : perm β, σ.is_cycle → disjoint σ τ → P σ → P τ → P (σ * τ)) :
  P σ :=
begin
  suffices :
    ∀ l : list (perm β), (∀ τ : perm β, τ ∈ l → τ.is_cycle) → l.pairwise disjoint → P l.prod,
  { classical,
    let x := σ.trunc_cycle_factors.out,
    exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2) },
  intro l,
  induction l with σ l ih,
  { exact λ _ _, base_one },
  { intros h1 h2,
    rw list.prod_cons,
    refine induction_disjoint σ l.prod (h1 σ (l.mem_cons_self σ))
      (disjoint_prod_list_of_disjoint (list.pairwise_cons.mp h2).1)
      (base_cycles σ (h1 σ (l.mem_cons_self σ)))
      (ih (λ τ hτ, h1 τ (list.mem_cons_of_mem σ hτ)) (list.pairwise_of_pairwise_cons h2)) },
end

[Aaron Anderson]

Yeah, I think so.

[Yakov Pechersky]

I've made a lot of headway on constructable cycles via lists, like proving

lemma is_cycle_form_perm (x y : α) (xs : list α) (h : nodup (x :: y :: xs)) :
  is_cycle (form_perm (x :: y :: xs)) :=

https://github.com/leanprover-community/mathlib/commit/e7ffca5fffc981a097e0fdf1285977aae78216d9#diff-9c65c703978eccccaa9dcbcc614d775ffe4a39aac3347edb1f88c5c12b403cd4R784

[Yakov Pechersky]

As well as

lemma form_perm_reverse (l : list α) (h : nodup l) :
  form_perm l.reverse = (form_perm l)⁻¹ := sorry

lemma form_perm_rotate (l : list α) (h : nodup l) (n : ℕ) :
  form_perm (l.rotate n) = form_perm l := sorry

lemma support_form_perm_of_nodup (l : list α) (h : nodup l) (h' : ∀ (x : α), l ≠ [x]) :
  support (form_perm l) = l.to_finset := sorry