Zulip Chat Archive

Stream: maths

Topic: group theory game


view this post on Zulip 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).

view this post on Zulip Jason KY. (May 12 2020 at 12:21):

Ah yes, here is the right place

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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 :=

view this post on Zulip 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)

view this post on Zulip 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)?

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:25):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jason KY. (May 12 2020 at 12:30):

Maybe thats less confusing :)

view this post on Zulip 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....)?

view this post on Zulip Jason KY. (May 12 2020 at 12:32):

Yes, that's what it is

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip 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!

view this post on Zulip Jason KY. (May 12 2020 at 12:35):

Ah, sorry. I should definitely read more maths about this :)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:39):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:42):

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

view this post on Zulip 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!

view this post on Zulip Jason KY. (May 12 2020 at 12:42):

Bundled are cooler!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 12 2020 at 12:43):

Kevin Buzzard said:

bijective injective

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:44):

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

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:44):

or equivs with it, as you would say

view this post on Zulip Mario Carneiro (May 12 2020 at 12:44):

ah, well that could even be an equality

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Jason KY. (May 12 2020 at 12:49):

I agree that I should remove that definitely

view this post on Zulip 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)

view this post on Zulip 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)?

view this post on Zulip 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 ?)

view this post on Zulip Jason KY. (May 12 2020 at 12:53):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 :)

view this post on Zulip Mario Carneiro (May 12 2020 at 12:57):

I think that's a british spelling thing

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jason KY. (May 12 2020 at 12:58):

I prefer this first subgroup (center G)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 12 2020 at 13:00):

What Mario says is even better.

view this post on Zulip Jason KY. (May 12 2020 at 13:01):

What is the notation <= ?

view this post on Zulip Mario Carneiro (May 12 2020 at 13:01):

less-equal

view this post on Zulip Jason KY. (May 12 2020 at 13:01):

Oh!

view this post on Zulip Mario Carneiro (May 12 2020 at 13:01):

not subset because subgroup G is a lattice

view this post on Zulip Jason KY. (May 12 2020 at 13:02):

That is definitely an elegant way of approaching this

view this post on Zulip 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?

view this post on Zulip 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 (-;

view this post on Zulip Johan Commelin (May 12 2020 at 13:10):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 (C\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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-) )

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 14:28):

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

view this post on Zulip Johan Commelin (May 12 2020 at 14:29):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 12 2020 at 14:29):

who just beat me to it

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 14:32):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 12 2020 at 14:32):

Yes, via logs. We have logs :-)

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 14:32):

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

view this post on Zulip Filippo A. E. Nuccio (May 12 2020 at 14:33):

(for volumes, I mean)

view this post on Zulip Mario Carneiro (May 12 2020 at 14:33):

emphasis on "bit"

view this post on Zulip orlando (May 12 2020 at 16:25):

@Kevin Buzzard it's a nice project !


Last updated: May 18 2021 at 08:14 UTC