groups (bundling etc)

Stream: maths

[Kevin Buzzard]

I was just looking through what we have on group theory.

1) The definition of simple_group is incorrect -- the trivial group is not simple, for the same reason that 1 is not a prime number. I was going to fix this but then I realised I didn't know the idiomatic way to say "I am not the trivial group". How about demanding the existence of an element which is not the identity? Any better ideas? This is in group_theory/subgroup.lean.

2) We still only have Sylow 1? @Chris Hughes are you going to PR Sylow 2 and 3?

3) Do we have the canonical bijection of lattices (or whatever they are) between the lattice of subgroups of G containing the normal subgroup N, and the lattice of subgroups of G/N? And how best to say that this lattice preserves normal subgroups?

[Kevin Buzzard]

I've just looked a bit more (and changed the title). I would like to put some lattice structure on the subgroups of G and prove things such as (3) above (is that the 3rd or 4th isomorphism theorem or something)? Having looked at how this is done for submodules I realise that one difference is that...I think "submodules are bundled and subgroups are not". Is that the right lingo? Can I bundle subgroups? What would the definition be?

structure subgroup (G : Type*) [group G] :=
(carrier : set G)
(is_subgroup : is_subgroup carrier)

?

And then I can prove they're a semisubinfbot-lattice or whatever?

[Kevin Buzzard]

@Chris Hughes are groups bundled already? Is this how to bundle them?

[Kenny Lau]

groups are not bundled and not to be bundled

[Kenny Lau]

subgroups are to be bundled using something similar to your code

[Kenny Lau]

and you can then prove that they form a complete lattice (because it has galois insertion/connection using subgroup span)

[Kevin Buzzard]

Right. I was going to tell the student to copy submodules and bundle subgroups

[Kevin Buzzard]

(and yes sorry, I'm not talking about bundling groups)

[Kevin Buzzard]

So bundling subgroups and add_subgroups would be an appropriate PR?

[Kenny Lau]

I believe so

[Johan Commelin]

@Kevin Buzzard I'm not sure if you should give that to a student.

[Johan Commelin]

It doesn't have any mathematical content, and it will likely be a very painful refactor of mathlib.

[Kevin Buzzard]

We'll do it together. We're doing something else really, some lemmas in finite group theory.

[Kevin Buzzard]

But I now believe that the natural way to state that there's a bijection between the subgroups of G/N and the subgroups of G containing N is using this lattice stuff, which forces me to bundle subgroups.

[Kevin Buzzard]

Why do I need to refactor anything? We just bundle them and leave the unbundled stuff there.

[Johan Commelin]

Hmmm... that feels like bad library design to me.

[Johan Commelin]

It's fine to just bundle them in some project... but I'm not sure if it should be added to mathlib...

[Kevin Buzzard]

That's fine.

[Kevin Buzzard]

I am trying to understand Assia's paper about Zassenhaus.

[Kevin Buzzard]

She makes a lot of fuss about making all groups subgroup of a big group, and this felt to me very much like the glueing sheaves thing.

[Kevin Buzzard]

I figured that the best way to get to the bottom of it was to get a summer student to do Zassenhaus in Lean.

[Kevin Buzzard]

Hmmm... that feels like bad library design to me.

I don't really understand this stuff. So there is already is_subgroup. I am proposing to make subgroup, using is_subgroup. Then we have the best of both worlds. Are you (@Johan Commelin ) saying that if I were to bundle subgroup then is_subgroup should be completely removed from mathlib? But then I can't define subgroup using is_subgroup. So is my proposed definition not right?

[Chris Hughes]

I'm in favour of bundling subgroups.

[Johan Commelin]

There is no is_submodule either.

[Johan Commelin]

The point is, you can't easily apply lemma's using one version in a setup using the other. So we should use only one of the two.

[Kevin Buzzard]

So a better definition would just be to copy the definition of a subgroup to a bundled definition without using is_subgroup, and then to slowly remove every occurrence of is_subgroup?

[Kevin Buzzard]

And can this be done slowly, i.e. make the bundled subgroups, leave is_subgroup, put a comment by it saying it's deprecated, and then over the course of the next few months remove all occurrences of it?

[Johan Commelin]

I'm not sure if that will work... but I'm a refactor newbie

[Kevin Buzzard]

You're less of a newbie than me -- I've just regarded all this refactoring stuff as tedious implementation issues because I've not been able to learn everything at once. Give me a tonne of proofs to do in tactic mode and I'm in heaven. Give me a simple object to make and I need help.

[Kevin Buzzard]

one reason we still don't know that Spa(perfectoid field) is a perfectoid space is that I keep looking at the maths definition of a perfectoid field and thinking "crap, I really don't know the best way to write this in Lean".

[Kevin Buzzard]

I am really bad at making definitions. This is why I'm asking these dumb questions. I need to learn this stuff now and it's kind of getting to the top of the pile.

[Mario Carneiro]

It can be done gradually, but that tends to be more total work than doing everything in one chunk

[Mario Carneiro]

so I try to do refactors all in one go if I can budget the time

[Kevin Buzzard]

So both Chris and Kenny think that subgroups should be bundled. And the longer they're not bundled, the harder it will be to bundle them. And is_subgroup extends is_submonoid so presumably submonoids should also be bundled.

[Kevin Buzzard]

so I try to do refactors all in one go if I can budget the time

The thing about that approach is that then you end up with a huge PR which needs to be merged really quickly.

[Kevin Buzzard]

I am trying to see a path to bundling subgroups. @Sian Carey and I are going to try it this summer just to see how it works.

[Mario Carneiro]

You are absolutely right. It requires a lot of global coordination in a short time, so this becomes less attractive the larger the project gets

[Kevin Buzzard]

So perhaps doing it slowly is a more viable solution for this particular case?

[Patrick Massot]

Maybe you can setup a PR appointment? You ask Mario how much time he would need to review such a PR, and when he'll have that much time, and try to fire up the PR at that point in time

[Kevin Buzzard]

What's wrong with just doing it slowly? I have very little experience with this kind of code management.

[Mario Carneiro]

The problem with doing things slowly is they take longer