Solvable groups

Stream: Berkeley Lean Seminar

[Patrick Lutz]

@Jordan Brown I just pushed a commit to the abel_ruffini branch that rearranges some stuff in abelianization.lean. In particular, I created sections for general_nth_commutator and commutator_map, made the group G an implicit rather than explicit argument of general_nth_commutator and changed some stuff to align with mathlib style. I also renamed general_nth_commutator_subgroup to general_nth_commutator_zero for consistency.

[Patrick Lutz]

Also, I thought it might be a good idea to start using separate topics for stuff because the Project Ideas thread is getting hard too long to easily find stuff from the past

[Patrick Lutz]

@Jordan Brown I tried refactoring your lemma quotient_something a bit and came up with this: https://github.com/leanprover-community/mathlib/blob/f9eb3be0b8feba369b0991856952ce67eb0fb4ea/src/group_theory/abelianization.lean#L412

[Patrick Lutz]

really, I split it into three lemmas: le_ker, nth_commutator_le_ker and nth_commutator_le_of_solvable_quotient, which are all near the line I linked to above

[Patrick Lutz]

and now I've also added a refactored version of short_exact_sequence_solvable here: https://github.com/leanprover-community/mathlib/blob/ce6eb692e5dad1c0f02b939442c4b2af2185b49a/src/group_theory/abelianization.lean#L420

[Patrick Lutz]

It turns out that the fact that if $G' \to G \to G''$ forms a short exact sequence with $G'$ and $G''$ solvable then $G$ is solvable does not depend on the first morphism being injective or on the second morphism being surjective, which I discovered when I refactored your proof

[Patrick Lutz]

@Jordan Brown Some of the stuff about solvable groups has now been merged into mathlib and some changes have occurred. For example, nth_commutator is now called derived_series and is_solvable is a class (though that shouldn't make a big difference). Also I moved everything from abelianization.lean to solvable.lean.

[Patrick Lutz]

@Thomas Browning What happened in this commit to the abel-ruffini branch? It seems to have deleted a lot of stuff from group_theory/solvable.lean

[Thomas Browning]

uh oh, I might have mucked up a merge

[Patrick Lutz]

no problem

[Patrick Lutz]

I just wasn't sure if I was confused about something

[Thomas Browning]

shall I add it back or will you?

[Thomas Browning]

looks like a few other files didn't quite get merged correctly

[Thomas Browning]

there seem to be some stray <<<<<<< HEAD, >>>>>>> master

[Patrick Lutz]

I'm adding it back now

[Patrick Lutz]

Actually, what was the context of that commit?

[Patrick Lutz]

you were trying to merge recent changes to mathlib right?

[Thomas Browning]

IIRC, the abel ruffini branch had several hundred "files changed" (rather than 10 or so), so I tried to do a "git merge master" to fix it.

[Patrick Lutz]

Thomas Browning said:

IIRC, the abel ruffini branch had several hundred "files changed" (rather than 10 or so), so I tried to do a "git merge master" to fix it.

How did that happen?

[Thomas Browning]

The several hundred "files changed"?

[Patrick Lutz]

yeah

[Thomas Browning]

not sure

[Thomas Browning]

this page does look weird though: https://github.com/leanprover-community/mathlib/compare/abel-ruffini

[Thomas Browning]

if you scroll to the bottom

[Thomas Browning]

there's a ton of commits that aren't part of a usual merge

[Patrick Lutz]

hmm, how about this: I can go back to this commit and then merge with mathlib master again

[Patrick Lutz]

assuming you didn't do any work in between that commit and now

[Thomas Browning]

I might have made a few changes since then though

[Patrick Lutz]

oh, hmm

[Patrick Lutz]

which commit?

[Thomas Browning]

well, the merge I think

[Patrick Lutz]

which files did you edit?

[Thomas Browning]

probably just files related to my PR

[Thomas Browning]

actually, not sure if I changed anything

[Thomas Browning]

none of my open VSCode tabs have anything

[Thomas Browning]

and I don't remember specifically making any changes

[Patrick Lutz]

Thomas Browning said:

probably just files related to my PR

do you just mean you were merging changes to mathlib from your PR?

[Thomas Browning]

oh, that might be right

[Thomas Browning]

but that's not important

[Thomas Browning]

I think it's fine to revert back to that old commit

[Patrick Lutz]

okay, let me try it

[Patrick Lutz]

sorry, this is sort of my fault. I did a rebase instead of a merge recently and it made things more confusing on the next merge

[Thomas Browning]

ah ok, no worries

[Thomas Browning]

are things fixed?

[Patrick Lutz]

I'm not quite done yet but I think it should be fine. But my computer crashed because I also had zoom open

[Patrick Lutz]

Patrick Lutz said:

sorry, this is sort of my fault. I did a rebase instead of a merge recently and it made things more confusing on the next merge

although this wasn't why merging solvable.lean was messy. For some reason git just had trouble figuring out how to merge that file

[Patrick Lutz]

Okay, everything should be okay now. And even if you did add some stuff during the merge you did it should still be there I think

[Patrick Lutz]

I think the solvable.lean merge was just pretty confusing

[Jordan Brown]

Is there a particular reason why the version of solvable currently in mathlib leaves out the general_nth_commutator things? I got the solvable_groups branch to compile correctly, but I needed to put in the general_nth_commutator results since they are used in the proof of the generalization of the short exact sequence implying solvability

[Jordan Brown]

I could just rewrite the proofs so they don't use the general_nth_commutator results but rather include the proofs directly if we don't want to keep the general_nth_commutator

[Jordan Brown]

also, if we do keep it, should I rename it to something like general_derived_series? @Patrick Lutz @Thomas Browning

[Patrick Lutz]

@Jordan Brown It's not in mathlib because I didn't PR it to mathlib so far but there's no deeper reason. I'm not sure whether general_nth_commutator should be included or not. It's the kind of design decision that PR reviewers can probably comment on. In some recent changes I pushed to the abel-ruffini branch, I added one proof that doesn't use general_nth_commutator (see the lemma short_exact_sequence_solvable_new in solvable.lean). I think if you do include general_nth_commutator in your PR you should probably change the name. general_derived_series sounds reasonable I guess.

[Aaron Anderson]

I haven't been following your work here closely, but I seem to recall that you (almost?) have a proof that S5 isn't solvable somewhere. Could you point me to it?

[Aaron Anderson]

I've been working on some adjacent topics (#6913, #6926) that may be helpful, but I don't want to duplicate too much work.

[Thomas Browning]

@Aaron Anderson Insolvability of S_5 is basically done, but isn't in mathlib yet (@Jordan Brown is working on it). However, our proof of insolvability of S_5 is very hacky (I've included the core of the proof at the end of this message, in case you want a flavor of what it's like). In particular, we haven't done anything with alternating groups or simple groups, so you don't need to worry about duplicating our work.

inductive weekday : Type
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday

open weekday

def g1 : weekday → weekday
| monday := monday
| tuesday := tuesday
| wednesday := thursday
| thursday := friday
| friday := wednesday

def g2 : weekday → weekday
| monday := monday
| tuesday := tuesday
| wednesday := friday
| thursday := wednesday
| friday := thursday

def g3 : weekday → weekday
| monday := thursday
| tuesday := friday
| wednesday := wednesday
| thursday := monday
| friday := tuesday

def g4 : weekday → weekday
| monday := wednesday
| tuesday := tuesday
| wednesday := friday
| thursday := thursday
| friday := monday

def g5 : weekday → weekday
| monday := friday
| tuesday := tuesday
| wednesday := monday
| thursday := thursday
| friday := wednesday

def σ1 : weekday ≃ weekday :=
{ to_fun := g1,
  inv_fun := g2,
  left_inv := λ x, by { cases x, all_goals { refl } },
  right_inv := λ x, by { cases x, all_goals { refl } } }

def σ2 : weekday ≃ weekday :=
{ to_fun := g3,
  inv_fun := g3,
  left_inv := λ x, by { cases x, all_goals { refl } },
  right_inv := λ x, by { cases x, all_goals { refl } } }

def σ3 : weekday ≃ weekday :=
{ to_fun := g4,
  inv_fun := g5,
  left_inv := λ x, by { cases x, all_goals { refl } },
  right_inv := λ x, by { cases x, all_goals { refl } } }

lemma alternating_stability (n : ℕ) : σ1 ∈ derived_series (equiv.perm weekday) n :=
begin
  induction n with n ih,
  { exact mem_top σ1 },
  rw (show σ1 = σ3 * ((σ2 * σ1 * σ2) * σ1 * (σ2 * σ1 * σ2⁻¹)⁻¹ * σ1⁻¹) * σ3⁻¹,
      by { ext, cases x, all_goals { refl } }),
  exact (derived_series_normal _ _).conj_mem _ (general_commutator_containment _ _ _
    ((derived_series_normal _ _).conj_mem _ ih _) _ ih) _,
end

lemma not_solvable_of_mem_derived_series {g : G} (h1 : g ≠ 1)
  (h2 : ∀ n : ℕ, g ∈ derived_series G n) : ¬ is_solvable G :=
mt (is_solvable_def _).mp (not_exists_of_forall_not (λ n, mt subgroup.ext'_iff.mp
  (mt set.ext_iff.mp (not_forall_of_exists_not
    ⟨g, λ h, (not_congr (iff.symm h)).mp (mt subgroup.mem_bot.mp h1) (h2 n)⟩))))

lemma weekday_perm_unsolvable : ¬ is_solvable (equiv.perm weekday) :=
 not_solvable_of_mem_derived_series (mt equiv.ext_iff.mp
  (not_forall_of_exists_not ⟨wednesday, by trivial⟩)) alternating_stability

[Thomas Browning]

@Aaron Anderson Let me know if you're moving in the direction of finding generating sets for A_n and S_n (e.g., that A_n is generated by 3-cycles, which can be used to prove simplicity). I've been working on generating sets for S_n (https://github.com/leanprover-community/mathlib/compare/perm_generation), so we should coordinate if you're moving in that direction.

[Aaron Anderson]

I only started working on this kind of group theory a few days ago, but I was considering working in that direction, to show that A_n is simple.

[Thomas Browning]

Great. My guess is that you might not be able to directly use the results I've got in https://github.com/leanprover-community/mathlib/compare/perm_generation, since those are for generating S_n, but some of your stuff might naturally fit in that file.

[Kevin Buzzard]

This code makes it clear that "there is more than one S_5", but I suspect that the "canonical" S_5 will be perm (fin 5)? This is just like universal properties isn't it -- should one prove theorems about "the canonical S_5" or about all S_5's? Is S_5 defined up to isomorphism or up to unique isomorphism? etc.

[Thomas Browning]

Our plan is to generalize to 5 ≤ cardinal.mk X

[Thomas Browning]

(using the existing result, plus an injective homomorphism perm weekday -> perm X)

[Aaron Anderson]

I've poked at this a bit, it seems as if most of the work (in the approach that occurs to me) is just the casework to show that the product of two swaps is generated by 3-cycles, and to show that f.card.support = 3 implies is_cycle

[Aaron Anderson]

Thomas Browning said:

Great. My guess is that you might not be able to directly use the results I've got in https://github.com/leanprover-community/mathlib/compare/perm_generation, since those are for generating S_n, but some of your stuff might naturally fit in that file.

I'm sorry, it looks like I missed some critical parts of this branch, and ended up duplicating some of it in #6951.

[Aaron Anderson]

I think the best move is to make #6951 depend on both #6968 and #6969, and I can change my notation as we go.

[Thomas Browning]

Actually, I've just added the duplicate stuff in the past day or two, so it's probably me who is duplicating you

[Thomas Browning]

The stuff that you've done in your PR looks better than mine, actually

[Thomas Browning]

@Aaron Anderson How does this sound: I'll close my PRs, and maybe make a few suggestions to yours?

[Aaron Anderson]

That's ok with me, I'll just leave everything be.

[Aaron Anderson]

You can push changes to those PRs if you'd like.

[Aaron Anderson]

I see that you've also added some stuff about cycle types since we last talked, so I will not work on that without starting a Zulip discussion. I'd like to show that equal cycle types implies conjugacy, but the ordinary simple proof seems hard to formalize...

[Thomas Browning]

@Jordan Brown #7453

[Thomas Browning]

@Jordan Brown If you want to take a stab at some of the remaining sorries at https://github.com/leanprover-community/mathlib/compare/polySn, you can do leanproject get mathlib:polySn to get a copy of the branch.

[Thomas Browning]

@Jordan Brown Johan found a much better way to work with explicit permutations:

lemma equiv.perm.fin_5_not_solvable : ¬ is_solvable (equiv.perm (fin 5)) :=
begin
  let x : equiv.perm (fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], dec_trivial, dec_trivial⟩,
  let y : equiv.perm (fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], dec_trivial, dec_trivial⟩,
  let z : equiv.perm (fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], dec_trivial, dec_trivial⟩,
  have x_ne_one : x ≠ 1,
  { refine λ h, not_forall_of_exists_not ⟨0, _⟩ (equiv.ext_iff.mp h),
    dec_trivial },
  have key : x = z * (x * (y * x * y⁻¹) * x⁻¹ * (y * x * y⁻¹)⁻¹) * z⁻¹,
  { ext a,
    dec_trivial! },
  refine not_solvable_of_mem_derived_series x_ne_one (λ n, _),
  induction n with n ih,
  { exact mem_top x },
  { rw key,
    exact (derived_series_normal _ _).conj_mem _
      (general_commutator_containment _ _ ih ((derived_series_normal _ _).conj_mem _ ih _)) _ },
end

lemma equiv.perm.not_solvable (X : Type*) (hX : 5 ≤ cardinal.mk X) :
  ¬ is_solvable (equiv.perm X) :=
begin
  introI h,
  have key : nonempty (fin 5 ↪ X),
  { rwa [←cardinal.lift_mk_le, cardinal.mk_fin, cardinal.lift_nat_cast,
    nat.cast_bit1, nat.cast_bit0, nat.cast_one, cardinal.lift_id] },
  exact equiv.perm.fin_5_not_solvable (solvable_of_solvable_injective
    (equiv.perm.via_embedding_hom_injective (nonempty.some key))),
end

[Yakov Pechersky]

With form_perm:

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]

[Johan Commelin]

@Yakov Pechersky That looks really great!

[Yakov Pechersky]

Thanks. I'm hoping to make cyclic permutation notation a la matrix notation

[Yakov Pechersky]

With something like

notation `cl` l := (l : cycle \a).to_perm dec_trivial

[Yakov Pechersky]

So one can write

cl [1, 3, 5]

and have that automatically be the permutation corresponding to (1 3 5), with Lean knowing that it is exactly equal to cl [3, 5, 1]

[Yakov Pechersky]

Additionally, some of the work I've been trying to do with changing cycle_factors to a finset should lead us to be able to make #eval (p : perm (fin n)) be able to have a way to display it -- since it is fintype, we can factor it out into its cycles, then each cyclic permutation can be associated precisely with a single cycle, and since fin n has an order, we can choose what to display for that cycle