Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: Solvable groups


Patrick Lutz (Jan 02 2021 at 23:18):

@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 (Jan 02 2021 at 23:18):

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 (Jan 03 2021 at 08:38):

@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 (Jan 03 2021 at 08:39):

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 (Jan 03 2021 at 09:46):

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 (Jan 03 2021 at 09:48):

It turns out that the fact that if GGGG' \to G \to G'' forms a short exact sequence with GG' and GG'' solvable then GG 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 (Jan 07 2021 at 11:12):

@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 (Jan 07 2021 at 22:24):

@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 (Jan 07 2021 at 22:31):

uh oh, I might have mucked up a merge

Patrick Lutz (Jan 07 2021 at 22:31):

no problem

Patrick Lutz (Jan 07 2021 at 22:31):

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

Thomas Browning (Jan 07 2021 at 22:32):

shall I add it back or will you?

Thomas Browning (Jan 07 2021 at 22:34):

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

Thomas Browning (Jan 07 2021 at 22:34):

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

Patrick Lutz (Jan 07 2021 at 22:36):

I'm adding it back now

Patrick Lutz (Jan 07 2021 at 22:37):

Actually, what was the context of that commit?

Patrick Lutz (Jan 07 2021 at 22:37):

you were trying to merge recent changes to mathlib right?

Thomas Browning (Jan 07 2021 at 22:38):

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 (Jan 07 2021 at 22:38):

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 (Jan 07 2021 at 22:39):

The several hundred "files changed"?

Patrick Lutz (Jan 07 2021 at 22:39):

yeah

Thomas Browning (Jan 07 2021 at 22:39):

not sure

Thomas Browning (Jan 07 2021 at 22:39):

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

Thomas Browning (Jan 07 2021 at 22:40):

if you scroll to the bottom

Thomas Browning (Jan 07 2021 at 22:40):

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

Patrick Lutz (Jan 07 2021 at 22:40):

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

Patrick Lutz (Jan 07 2021 at 22:40):

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

Thomas Browning (Jan 07 2021 at 22:40):

I might have made a few changes since then though

Patrick Lutz (Jan 07 2021 at 22:40):

oh, hmm

Patrick Lutz (Jan 07 2021 at 22:40):

which commit?

Thomas Browning (Jan 07 2021 at 22:41):

well, the merge I think

Patrick Lutz (Jan 07 2021 at 22:41):

which files did you edit?

Thomas Browning (Jan 07 2021 at 22:41):

probably just files related to my PR

Thomas Browning (Jan 07 2021 at 22:41):

actually, not sure if I changed anything

Thomas Browning (Jan 07 2021 at 22:42):

none of my open VSCode tabs have anything

Thomas Browning (Jan 07 2021 at 22:42):

and I don't remember specifically making any changes

Patrick Lutz (Jan 07 2021 at 22:42):

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 (Jan 07 2021 at 22:42):

oh, that might be right

Thomas Browning (Jan 07 2021 at 22:42):

but that's not important

Thomas Browning (Jan 07 2021 at 22:42):

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

Patrick Lutz (Jan 07 2021 at 22:42):

okay, let me try it

Patrick Lutz (Jan 07 2021 at 22:51):

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 (Jan 07 2021 at 22:59):

ah ok, no worries

Thomas Browning (Jan 07 2021 at 22:59):

are things fixed?

Patrick Lutz (Jan 07 2021 at 23:00):

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 (Jan 07 2021 at 23:10):

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 (Jan 07 2021 at 23:38):

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 (Jan 07 2021 at 23:39):

I think the solvable.lean merge was just pretty confusing

Jordan Brown (Jan 12 2021 at 01:01):

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 (Jan 12 2021 at 01:02):

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 (Jan 12 2021 at 01:02):

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

Patrick Lutz (Jan 12 2021 at 05:31):

@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 (Mar 28 2021 at 21:30):

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 (Mar 28 2021 at 21:31):

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 (Mar 28 2021 at 21:47):

@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 (Mar 28 2021 at 21:51):

@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 (Mar 28 2021 at 22:03):

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 (Mar 28 2021 at 22:05):

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 (Mar 28 2021 at 22:22):

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 (Mar 28 2021 at 22:26):

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

Thomas Browning (Mar 28 2021 at 23:30):

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

Aaron Anderson (Mar 28 2021 at 23:44):

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 (Mar 30 2021 at 22:56):

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 (Mar 30 2021 at 22:58):

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 (Mar 30 2021 at 23:00):

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 (Mar 30 2021 at 23:03):

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

Thomas Browning (Mar 30 2021 at 23:06):

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

Aaron Anderson (Mar 31 2021 at 00:29):

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

Aaron Anderson (Mar 31 2021 at 00:30):

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

Aaron Anderson (Mar 31 2021 at 00:31):

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 (May 03 2021 at 22:58):

@Jordan Brown #7453

Thomas Browning (May 04 2021 at 05:05):

@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 (May 06 2021 at 23:10):

@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 (May 07 2021 at 00:45):

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 (May 07 2021 at 05:58):

@Yakov Pechersky That looks really great!

Yakov Pechersky (May 07 2021 at 05:58):

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

Yakov Pechersky (May 07 2021 at 06:00):

With something like

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

Yakov Pechersky (May 07 2021 at 06:01):

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 (May 07 2021 at 06:09):

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


Last updated: Dec 20 2023 at 11:08 UTC