group theory game

Stream: maths

[Filippo A. E. Nuccio]

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.]

Ah yes, here is the right place

[Jason KY.]

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]

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.]

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]

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]

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

[Kevin Buzzard]

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

[Jason KY.]

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]

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

[Jason KY.]

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]

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

[Kevin Buzzard]

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

[Filippo A. E. Nuccio]

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.]

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.]

Maybe thats less confusing :)

[Filippo A. E. Nuccio]

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

[Jason KY.]

Yes, that's what it is

[Filippo A. E. Nuccio]

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]

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]

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

[Jason KY.]

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

[Filippo A. E. Nuccio]

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]

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]

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.]

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

[Kevin Buzzard]

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]

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

[Filippo A. E. Nuccio]

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]

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]

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]

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.]

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]

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]

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]

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

[Kevin Buzzard]

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

[Jason KY.]

Bundled are cooler!

[Filippo A. E. Nuccio]

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]

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]

Kevin Buzzard said:

bijective injective

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

or equivs with it, as you would say

[Mario Carneiro]

ah, well that could even be an equality

[Mario Carneiro]

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

[Kevin Buzzard]

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.]

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]

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

[Kevin Buzzard]

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]

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.]

I agree that I should remove that definitely

[Filippo A. E. Nuccio]

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]

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.]

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.]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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.]

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]

I think that's a british spelling thing

[Filippo A. E. Nuccio]

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]

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.]

I prefer this first subgroup (center G)

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

What Mario says is even better.

[Jason KY.]

What is the notation <= ?

[Mario Carneiro]

less-equal

[Jason KY.]

Oh!

[Mario Carneiro]

not subset because subgroup G is a lattice

[Jason KY.]

That is definitely an elegant way of approaching this

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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 :-) )

Here’s a nice thread giving a very intense and non-constructive proof sketch of the following fact: if G is a finitely-presented group, then *any* set of generators require only finitely many relations. Here’s a simple proof 1/n https://twitter.com/schala163/status/1259957142674604032

- Daniel Litt (@littmath)

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

who just beat me to it

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

Yes, via logs. We have logs :-)

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

(for volumes, I mean)

[Mario Carneiro]

emphasis on "bit"

[orlando]

@Kevin Buzzard it's a nice project !