## Stream: maths

### Topic: group theory game

#### Filippo A. E. Nuccio (May 12 2020 at 12:08):

Can someone explain what is going on with central_subgroup? It looks to me to be at the same time a definition (all its elements are central) and to be a theorem (the center-or centre?- is a subgroup).

#### Jason KY. (May 12 2020 at 12:21):

Ah yes, here is the right place

#### Jason KY. (May 12 2020 at 12:21):

Right, I made its carrier to be the center set, but to prove its indeed a subgroup I had to prove the axioms

#### Filippo A. E. Nuccio (May 12 2020 at 12:22):

Can you explain a bit the syntax of the def central_subgroup? I guess I don't know what the " carrier" is. Because the first line of the def seems to me to be saying "let H be any subset of G, then it is a subgroup"

#### Jason KY. (May 12 2020 at 12:23):

Right, that was a mistake, I've fixed it now, it should say def central_subgroup (G : Type) [group G] : subgroup G :=

#### Filippo A. E. Nuccio (May 12 2020 at 12:24):

But why do you want it to be a def? It seems to me that the centre has already been def'd (in the definition file in group folder)

#### Filippo A. E. Nuccio (May 12 2020 at 12:24):

So why don't you want a "lemma" (saying: the subset called centre/center there is in fact a sbgrp)?

#### Kevin Buzzard (May 12 2020 at 12:25):

https://github.com/ImperialCollegeLondon/group-theory-game is what we're talking about

#### Jason KY. (May 12 2020 at 12:26):

Right but I would like it to have type subgroup G. The center G has type set G if I am not mistaken

#### Kevin Buzzard (May 12 2020 at 12:27):

https://github.com/ImperialCollegeLondon/group-theory-game/blob/c8f0330486b606a0013013cd3a7990ea23ce7d0f/src/group/definitions.lean#L51

#### Jason KY. (May 12 2020 at 12:27):

And if we make a lemma saying is_subgroup (center G) then we are no longer working with the bundled subgroups but the proposition is_subgroup

#### Kevin Buzzard (May 12 2020 at 12:27):

Yes, center G has type set G, the type of subsets of G. So center G is a subset, not a subgroup.

#### Kevin Buzzard (May 12 2020 at 12:28):

This {g : G | ∀ k : G, k * g = g * k} is notation for a constructor for set G.

#### Filippo A. E. Nuccio (May 12 2020 at 12:29):

Ah, ok, I see. So the point is now to "upgrade" this subset to a subgroup, and this is what central_subgroup does. Is that right?

#### Jason KY. (May 12 2020 at 12:30):

Yeah, tbh I don't think I needed to define center at all but instead just define the central subgroup as a subgroup with {g : G | ∀ k : G, k * g = g * k} as the carrier

#### Jason KY. (May 12 2020 at 12:30):

Maybe thats less confusing :)

#### Filippo A. E. Nuccio (May 12 2020 at 12:32):

I am sorry, I am really a beginner; but the "carrier" is the underlying subset (in old-fashioned terminology....)?

#### Jason KY. (May 12 2020 at 12:32):

Yes, that's what it is

#### Filippo A. E. Nuccio (May 12 2020 at 12:33):

But then this is the definition of the centre... I am perplexed. To me, a "central subgroup" is one which is contained in the centre, non necessarily the whole centre.

#### Kevin Buzzard (May 12 2020 at 12:34):

I agree that this is the standard usage. Jason is a 1st year maths undergraduate, he is just learning the theory himself right now (in fact he probably just took an exam on it!)

#### Filippo A. E. Nuccio (May 12 2020 at 12:34):

Oh, I am really sorry. I really did not mean to be rude in any way-Jason, all my apologies!

#### Filippo A. E. Nuccio (May 12 2020 at 12:35):

I am very novel to lean and I can't yet understand what you mean by
And if we make a lemma saying is_subgroup (center G) then we are no longer working with the bundled subgroups but the proposition is_subgroup
Could you please explain this a bit?

#### Kevin Buzzard (May 12 2020 at 12:36):

Sorry, I now understand the confusion :-) Yes, there are two things: firstly the centre as a subset and as a subgroup (the sort of thing which I try and explain here, and secondly the standard usage of central subgroup.

#### Filippo A. E. Nuccio (May 12 2020 at 12:38):

Yes, I thought that the "invisible" map was under the rug. But what I thought I understood from your blog was that Lean is able to apply this invisible map. But Jason seems to say that "if we make a lemma saying is_subgroup (center G) then we are no longer working with the bundled subgroups but the proposition is_subgroup", and unfortunately I am still unable to understand what it is meant by this.

#### Jason KY. (May 12 2020 at 12:38):

My english might not be good enought. What does "Can you then may be just speculate a bit about your comment" mean?

#### Kevin Buzzard (May 12 2020 at 12:39):

There are two ways that you can tell Lean "this is a subgroup". Firstly, you can define a type subgroup G such that a term of type subgroup G "is" a subgroup of G, in the sense that to make a term of this type is to give a subgroup of G in the sense that any mathematician would understand it.

#### Kevin Buzzard (May 12 2020 at 12:39):

i.e. you give a subset and the proof that it satisfies some axioms

#### Filippo A. E. Nuccio (May 12 2020 at 12:40):

Jason KY. said:

My english might not be good enought. What does "Can you then may be just speculate a bit about your comment" mean?

Modified!

#### Kevin Buzzard (May 12 2020 at 12:40):

Secondly, you can define a function called is_subgroup from the type of subsets of G to the type of true/false statements, and given a subset X of G you could construct a proof of is_subgroup X

#### Filippo A. E. Nuccio (May 12 2020 at 12:40):

Kevin Buzzard said:

There are two ways that you can tell Lean "this is a subgroup". Firstly, you can define a type subgroup G such that a term of type subgroup G "is" a subgroup of G, in the sense that to make a term of this type is to give a subgroup of G in the sense that any mathematician would understand it.

OK: and this is what Jason did in the def central_subgroup as it is now, right?

#### Kevin Buzzard (May 12 2020 at 12:40):

So here you have separated out the subset, namely X, and the proof that it's a subgroup, namely the proof of is_subgroup X

#### Jason KY. (May 12 2020 at 12:41):

Filippo A. E. Nuccio said:

Kevin Buzzard said:

There are two ways that you can tell Lean "this is a subgroup". Firstly, you can define a type subgroup G such that a term of type subgroup G "is" a subgroup of G, in the sense that to make a term of this type is to give a subgroup of G in the sense that any mathematician would understand it.

OK: and this is what Jason did in the def central_subgroup as it is now, right?

Yes, central_subgroup G will have type subgroup G

#### Kevin Buzzard (May 12 2020 at 12:42):

The computer science terminology for the type subgroup G is "bundled subgroups" and the terminology for the function, which separates the data from the proofs, is "unbundled subgroups". Yes, this is what Jason was doing with the centre, he was bundling it.

#### Filippo A. E. Nuccio (May 12 2020 at 12:42):

Kevin Buzzard said:

So here you have separated out the subset, namely X, and the proof that it's a subgroup, namely the proof of is_subgroup X

Very well: this looks more like "applying the invisible function but making it visible"... but are the two approaches equivalent at the end of the day?

#### Kevin Buzzard (May 12 2020 at 12:42):

Whether subgroups should be bundled or unbundled is not a mathematical question.

#### Kevin Buzzard (May 12 2020 at 12:42):

As you rightly point out, to a mathematician they are equivalent. They are the same. They are equal!

#### Jason KY. (May 12 2020 at 12:42):

Bundled are cooler!

#### Filippo A. E. Nuccio (May 12 2020 at 12:42):

Kevin Buzzard said:

As you rightly point out, to a mathematician they are equivalent. They are the same. They are equal!

That's great news! So, in particular, since the def of centre (as subset) was already given, wouldn't it have been more natural (no criticism here, of course!) to simply upgrade it to a subgroup rather than re-defining it?

#### Kevin Buzzard (May 12 2020 at 12:43):

To a computer scientist they are far from equal, because they are two different data types, and there are functions which map one data type to the other in a bijective way

#### Mario Carneiro (May 12 2020 at 12:43):

Kevin Buzzard said:

bijective injective

#### Kevin Buzzard (May 12 2020 at 12:44):

but if you want to make some algorithm which e.g. attempts to solve the word problem in a finitely-generated group, then you care a lot about exactly which data type you want to use

#### Kevin Buzzard (May 12 2020 at 12:44):

Mario I mean subgroup G bijects with {X : subset G // is_subgroup X}

#### Kevin Buzzard (May 12 2020 at 12:44):

or equivs with it, as you would say

#### Mario Carneiro (May 12 2020 at 12:44):

ah, well that could even be an equality

#### Mario Carneiro (May 12 2020 at 12:45):

but you still have to deal with the injection from subgroup G, or {X : subset G // is_subgroup X}, to subset G

#### Kevin Buzzard (May 12 2020 at 12:46):

So the question of how to set up subgroups is not at all mathematical, but actually a question about implementation issues, and people who understand these things far better than I have decided that if mathematicians want to talk about subgroups of G, Lean 3 would prefer that they talked about terms of type subgroup G rather than a pair consisting of a subset of G and a proof that it's a subgroup, even though to us they look like the same thing

#### Jason KY. (May 12 2020 at 12:47):

Filippo A. E. Nuccio said:

Kevin Buzzard said:

As you rightly point out, to a mathematician they are equivalent. They are the same. They are equal!

That's great news! So, in particular, since the def of centre (as subset) was already given, wouldn't it have been more natural (no criticism here, of course!) to simply upgrade it to a subgroup rather than re-defining it?

What does "upgrade it to a subgroup" mean in this context?

#### Filippo A. E. Nuccio (May 12 2020 at 12:47):

Oh, great .This makes perfect sense to me and I am very happy to follow them, if they so advise us.

#### Kevin Buzzard (May 12 2020 at 12:48):

The only way this affects mathematicians is that they need to be informed of this when they are formalising mathematical statements; they should use the conventions which make Lean 3 happier.

#### Filippo A. E. Nuccio (May 12 2020 at 12:49):

OK, and I will certainly follow the rule. But then it seems to me that the def of centre given in the group/definitions file should not be there, only the other one should exist. No?

#### Jason KY. (May 12 2020 at 12:49):

I agree that I should remove that definitely

#### Filippo A. E. Nuccio (May 12 2020 at 12:49):

Jason KY. said:

Filippo A. E. Nuccio said:

Kevin Buzzard said:

As you rightly point out, to a mathematician they are equivalent. They are the same. They are equal!

That's great news! So, in particular, since the def of centre (as subset) was already given, wouldn't it have been more natural (no criticism here, of course!) to simply upgrade it to a subgroup rather than re-defining it?

What does "upgrade it to a subgroup" mean in this context?

As far as I undestand from Kevin, some unbundling=some evil thing (a suggestion which I now retract, in light of Kevin's comments)

#### Filippo A. E. Nuccio (May 12 2020 at 12:51):

Jason KY. said:

I agree that I should remove that definitely

Ah, perfect. Then I undestand. And can I also suggest that we call the definition def centre rather than central_subgroup (for the reasons discussed with Kevin before, and that you'll soon learn about the existence of "central subgroups" more general than the centre itself)?

#### Jason KY. (May 12 2020 at 12:53):

Yes, I will change it to

def center (G : Type) [group G] : subgroup G :=
{ carrier  := {g : G | ∀ k : G, k * g = g * k},
one_mem' := λ k, by simp,
mul_mem' := λ x y hx hy k, by rw [←group.mul_assoc, hx, group.mul_assoc, hy, ←group.mul_assoc],
inv_mem' := λ x hx k,
begin
apply group.mul_left_cancel x,
iterate 2 {rw ←group.mul_assoc},
rw [←hx, group.mul_right_inv, group.mul_assoc, group.mul_right_inv], simp
end
}


And make central subgroups something else (a subgroup of the center ?)

#### Jason KY. (May 12 2020 at 12:53):

I will come back to it once I learn it fully of course

#### Filippo A. E. Nuccio (May 12 2020 at 12:54):

Exactly, central subgroups are subgroups of the centre (btw: do you prefer centre or center?) Great.

#### Filippo A. E. Nuccio (May 12 2020 at 12:55):

Also, am I correct in understanding that this is part of your work with Kevin about your studies? I don't want to jump into the project and destroy all its pedagogical aims... Kevin, what is your position?

#### Jason KY. (May 12 2020 at 12:56):

Filippo A. E. Nuccio said:

Exactly, central subgroups are subgroups of the centre (btw: do you prefer centre or center?) Great.

I don't personally have a preference but I normally use center :)

#### Mario Carneiro (May 12 2020 at 12:57):

I think that's a british spelling thing

#### Filippo A. E. Nuccio (May 12 2020 at 12:57):

Jason KY. said:

Filippo A. E. Nuccio said:

Exactly, central subgroups are subgroups of the centre (btw: do you prefer centre or center?) Great.

I don't personally have a preference but I normally use center :)

I believe centre is British Eng, center is American Eng.

#### Johan Commelin (May 12 2020 at 12:57):

So, for central subgroups, you have to choose again:

subgroup (center G)


or

(H : subgroup G) (h : is_central H)
-- where
def is_central (H : subgroup G) := \forall g h : G, h \in H → g * h = h * g


#### Jason KY. (May 12 2020 at 12:58):

I prefer this first subgroup (center G)

#### Johan Commelin (May 12 2020 at 12:58):

If you want to prove something about structure on the "set" of all central subgroups, then the first approach would be best. But I guess we don't. So I actually prefer the second.

#### Johan Commelin (May 12 2020 at 12:59):

Because it will make it easier to view central subgroups as just ordinary subgroups satisfying an extra condition.

#### Mario Carneiro (May 12 2020 at 13:00):

my preference would be to skip the definition is_central H and replace it with H <= center G

#### Johan Commelin (May 12 2020 at 13:00):

Otherwise we'll get a lot of invisible maps, and I don't know if they help us with anything. For a g : G you want to be able to write g \in H if H is a central subgroup. But with H : subgroup (center G) you will have to work harder to make this possible.

#### Johan Commelin (May 12 2020 at 13:00):

What Mario says is even better.

#### Jason KY. (May 12 2020 at 13:01):

What is the notation <= ?

less-equal

Oh!

#### Mario Carneiro (May 12 2020 at 13:01):

not subset because subgroup G is a lattice

#### Jason KY. (May 12 2020 at 13:02):

That is definitely an elegant way of approaching this

#### Filippo A. E. Nuccio (May 12 2020 at 13:09):

I see much better now. I still have the "pedagogical" question (what's the general approach here? Everybody does whatever they want, is there an organiser of each project?) and would also like to understand how to use git: should I create a branch and commit, copy-paste in the online file? Something else?

#### Johan Commelin (May 12 2020 at 13:10):

There is a group of maintainers of mathlib, see the README. Beyond that, everyone just does random stuff (-;

#### Johan Commelin (May 12 2020 at 13:10):

To use git is a different thing (-; There are good tutorials online.

#### Johan Commelin (May 12 2020 at 13:11):

Once you have stuff that you would like to PR to mathlib, you need an account at github, and give us your username there. Then we can give you the right to create branches on the mathlib repo, and push to them.

#### Kevin Buzzard (May 12 2020 at 13:16):

The group theory game repository is just an experiment. It might turn into a game, like the natural number game, it might turn into teaching material for either groups or lean, it might turn into something else, it will definitely not go into mathlib because mathlib already has groups.

#### Kevin Buzzard (May 12 2020 at 13:24):

I formalised the definition of complex numbers in Lean, so that did go into mathlib, but then a lot of people worked on the code and now the rest of the file looks nothing like what I originally wrote. I re-read it last week and wrote this "remix" of it, which will probably turn into a section of this pre-book which is slowly turning into a book, but which you Filippo might find interesting. It makes a type ($\mathbb{C}$) with a very simple definition, and then shows how you can prove it is a commutative ring by proving about 50 lemmas each with one-line proofs.

#### Kevin Buzzard (May 12 2020 at 13:25):

As you can see, this is pretty random, as Johan says. I'm interested in making random Lean things and then showing them beginners and trying to figure out what works. The natural number game came from this blog post which got a very positive response from my undergraduates.

#### Kevin Buzzard (May 12 2020 at 13:28):

I encourage beginners to choose a theorem statement/proof/definition and just formalise it, and make a little repo containing what they did -- for example I link to some here (in section "What?"). Jason is formalising group theory as he learns it, and also learning about bundling structures. Although he now has a mathlib PR under his belt, bundling submonoids, so it's more accurate to say that he has learnt about bundling structures.

#### Kevin Buzzard (May 12 2020 at 13:33):

For example @Filippo A. E. Nuccio if you wanted to do a trickier group thing you could try formalising some random piece of maths yourself (and then tell Daniel that you formalised his proof :-) )

#### Kevin Buzzard (May 12 2020 at 13:34):

Oh -- if you want to do the exercises in the complex number file, you could try the complex number game but you'd be better off cutting and pasting into Lean running on your own machine.

#### Filippo A. E. Nuccio (May 12 2020 at 14:25):

All clear. I will have a look at your implementation of \mathbb{C} and then I will try to do something on my own. Are number fields (either as Q(\alpha) or as splitting fields of irred. monic pol.'s in Z[x] already in mathlib?

#### Kevin Buzzard (May 12 2020 at 14:26):

Not as far as I know! I wrote some plan https://github.com/leanprover-community/mathlib/projects/3 but didn't start on it yet. I believe we have fractional ideals though.

#### Kevin Buzzard (May 12 2020 at 14:27):

Before we do number fields it might be best to prove that ideals factor into prime ideals in Dedekind domains, and then prove that the integers of a number field (we have integral closure) is an integral domain.

#### Filippo A. E. Nuccio (May 12 2020 at 14:28):

I agree. But are you saying that we already have Dedekind domains or should we introduce dimension theory, noetherianity, int. closedness?

#### Filippo A. E. Nuccio (May 12 2020 at 14:28):

If they're there, I can try my luck.

#### Johan Commelin (May 12 2020 at 14:29):

@Filippo A. E. Nuccio We do have splitting fields

#### Kevin Buzzard (May 12 2020 at 14:29):

We have Noetherian rings and integral closure. I don't think we have dimension theory or Dedekind domains. You might want to check with @Johan Commelin

#### Kevin Buzzard (May 12 2020 at 14:29):

who just beat me to it

#### Johan Commelin (May 12 2020 at 14:29):

No Dedekind domains yet, no number fields. But this is really just waiting for someone to come along and do it.

#### Kevin Buzzard (May 12 2020 at 14:30):

Formalising the proof that ideals factor into prime ideals will be a real baptism of fire, I would definitely do the exercises at the end of the complex number game first :-)

#### Filippo A. E. Nuccio (May 12 2020 at 14:30):

Ah perfect. I might venture out in the forest. So, the plan would be to define the ring of integers as the integral closure of Z in the splitting field and then prove every non-zero prime is max'l?

#### Filippo A. E. Nuccio (May 12 2020 at 14:31):

I'll certainly go for that, but it is also nice to have a further (furtheeeeeer) goal in mind.

#### Kevin Buzzard (May 12 2020 at 14:31):

I would formalise the definition of a Dedekind domain first, and then prove that integers of a number field are a Dedekind domain. That would be a nice place to start.

#### Johan Commelin (May 12 2020 at 14:31):

Re Fillipo: Well, I don't know if you want to do it in such a specific setup. But something like that.

#### Kevin Buzzard (May 12 2020 at 14:31):

Your goal is to prove that the class group of a global field is finite and the unit group is finitely-generated :-)

#### Filippo A. E. Nuccio (May 12 2020 at 14:32):

Through log-embeddings, though, I guess. Like introducing Minkowski convex-body?

#### Kevin Buzzard (May 12 2020 at 14:32):

That's what we prove in our UG course at Imperial and one mathlib plan is to get it to cover all the pure maths in a typical undergraduate degree.

#### Kevin Buzzard (May 12 2020 at 14:32):

Yes, via logs. We have logs :-)

#### Filippo A. E. Nuccio (May 12 2020 at 14:32):

Ah, that's cool. Do we also have a bit of integrals?

#### Filippo A. E. Nuccio (May 12 2020 at 14:33):

(for volumes, I mean)

#### Mario Carneiro (May 12 2020 at 14:33):

emphasis on "bit"

#### orlando (May 12 2020 at 16:25):

@Kevin Buzzard it's a nice project !

Last updated: May 18 2021 at 08:14 UTC