## Stream: maths

### Topic: groups (bundling etc)

#### Kevin Buzzard (Jul 08 2019 at 07:22):

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 (Jul 08 2019 at 10:04):

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 (Jul 08 2019 at 10:05):

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

#### Kenny Lau (Jul 08 2019 at 10:13):

groups are not bundled and not to be bundled

#### Kenny Lau (Jul 08 2019 at 10:13):

subgroups are to be bundled using something similar to your code

#### Kenny Lau (Jul 08 2019 at 10:13):

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

#### Kevin Buzzard (Jul 08 2019 at 10:20):

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

#### Kevin Buzzard (Jul 08 2019 at 10:21):

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

#### Kevin Buzzard (Jul 08 2019 at 10:22):

So bundling subgroups and add_subgroups would be an appropriate PR?

I believe so

#### Johan Commelin (Jul 08 2019 at 10:27):

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

#### Johan Commelin (Jul 08 2019 at 10:28):

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

#### Kevin Buzzard (Jul 08 2019 at 10:29):

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

#### Kevin Buzzard (Jul 08 2019 at 10:29):

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 (Jul 08 2019 at 10:30):

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

#### Johan Commelin (Jul 08 2019 at 10:33):

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

#### Johan Commelin (Jul 08 2019 at 10:34):

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

That's fine.

#### Kevin Buzzard (Jul 08 2019 at 10:44):

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

#### Kevin Buzzard (Jul 08 2019 at 10:45):

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 (Jul 08 2019 at 10:45):

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 (Jul 08 2019 at 12:07):

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 (Jul 08 2019 at 12:08):

I'm in favour of bundling subgroups.

#### Johan Commelin (Jul 08 2019 at 12:08):

There is no is_submodule either.

#### Johan Commelin (Jul 08 2019 at 12:08):

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 (Jul 08 2019 at 12:10):

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 (Jul 08 2019 at 12:11):

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 (Jul 08 2019 at 12:12):

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

#### Kevin Buzzard (Jul 08 2019 at 12:15):

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 (Jul 08 2019 at 12:16):

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 (Jul 08 2019 at 12:17):

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 (Jul 08 2019 at 12:24):

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

#### Mario Carneiro (Jul 08 2019 at 12:24):

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

#### Kevin Buzzard (Jul 08 2019 at 12:25):

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 (Jul 08 2019 at 12:25):

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 (Jul 08 2019 at 12:26):

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 (Jul 08 2019 at 12:28):

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 (Jul 08 2019 at 12:30):

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

#### Patrick Massot (Jul 08 2019 at 12:31):

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 (Jul 08 2019 at 14:02):

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

#### Mario Carneiro (Jul 08 2019 at 14:07):

The problem with doing things slowly is they take longer

Last updated: May 18 2021 at 08:14 UTC