PR

Stream: general

[Scott Morrison]

@Mario Carneiro, I've fixed all your suggestions on https://github.com/leanprover/mathlib/pull/94. Thanks!

[Kenny Lau]

@Mario Carneiro how come you didn't notice that subgroup is already there =P

[Mario Carneiro]

I assumed that scott would have noticed :P

[Mario Carneiro]

You should move all this stuff from the group folder to group_theory

[Mario Carneiro]

Speaking of two developments, I think I prefer Scott's definition of subgroup to the one that's there (Kenny's?), which is being clever combining two axioms into one. That's the sort of thing you do in an auxiliary constructor theorem, not in the definition

[Kenny Lau]

that isn't mine

[Kenny Lau]

I would never do such things :P

[Kenny Lau]

it's johoelzl's work

[Kenny Lau]

@Johannes Hölzl someone is challenging your style

[Mario Carneiro]

looks like it

[Johannes Hölzl]

I don't mind changing the definition of is_subgroup. I guess now we want to have is_submonoid and than is_subgroup as an extension? @Kenny Lau did you find some time to work on your free groups? As I remember the were submonoids involved?

[Kenny Lau]

there's no submonoid in my free group

[Kenny Lau]

there are monoids with involutions, maybe that's what confuses you

[Kenny Lau]

there are also monoid homomorphisms

[Johannes Hölzl]

Ah, okay. I think the monoid homomorphism confused me.

[Johannes Hölzl]

Now I found it, is_submonoid is already in algebra/group.lean. I will do some cleanup.

[Kenny Lau]

aha!

[Kenny Lau]

that's indeed my work for the localization isn't it

[Kenny Lau]

https://github.com/leanprover/mathlib/commit/c852939f5fcb3a1f0ebe38d8eebc6aede22b9e25#diff-52b9e281e7667f88f8203fb617843d93

[Kenny Lau]

yes it is

[Scott Morrison]

@Johannes Hölzl, in my group theory PR I just added a commit modifying your subgroup.lean. You said higher in the thread that you would do some cleanup --- if possible could we coordinate to avoid having merge issues later?

[Scott Morrison]

(Sorry, all for not noticing Johannes work. Mitchell did his work back in January, and I didn't noticed Johannes' work being committed in the meantime.)

[Johannes Hölzl]

Would be good, mostly I changed is_subgroup to extend is_submonoid and moved is_submonoid, also I'm adding gpowers.

[Scott Morrison]

It sounds like everyone agrees that the "3 axiom" version of is_subgroup is better than the "2 axiom" version, so maybe we could switch that as well?

[Scott Morrison]

I'm curious also about the naming. I (or rather, Mitchell) had written just subgroup, where you have is_subgroup.

[Scott Morrison]

Is is_subgroup obviously better?

[Scott Morrison]

Somehow when I think of it as a typeclass rather than a predicate subgroup seems more natural to me.

[Johannes Hölzl]

is_subgroup is not (yet) a type class. I'm not sure if it is a good idea to make structures like this type classes, for me sets and functions are to fluid in some sense to be nice type classes. This is also a reason why I don't like morphism predicates like is_group_hom etc to be type classes. But on the other hand they mostly work well, so maybe we should stay with this approach.

[Scott Morrison]

Ah, I hadn't even realised that we might not want is_subgroup to be a type class, although I should have from the mere fact that you didn't do this!

[Johannes Hölzl]

The other thing is that we might want to use subgroup := {s // is_subgroup s}. for the bundled type

[Scott Morrison]

I guess I was anticipating the naming convention was Subgroup := { s // subgroup s}.

[Johannes Hölzl]

True. There might be also Group := sigma A : Type, group A, and then Subgroup could be over Group. But I guess we don't need this yet. And in the worst case it could be in its own namespace.

For the current PR: can you revert your changes on group_theory/subgroup? Then I will push my changes, as far as I see it you don't use it yet.

[Johannes Hölzl]

Or would this be work for you?

[Johannes Hölzl]

Also the is_ convention is also coming from is_commutative etc. which is a Prop and talks about operators and not types. This is another reason why I slightly prefer is_subgroup for this kind of type classes.

[Scott Morrison]

Okay, I will work out how to revert my changes to group_theory/subgroup.

[Scott Morrison]

Okay, I've done this. Just let me know once you've pushed yours.

[Johannes Hölzl]

@Kenny Lau @Mario Carneiro I moved is_submonoid from algebra/group to its own file group_theory/submonoid.lean. Maybe it should be in algebra after all, but I think it shouldn't be part of the base, i.e. it shouldn't be part of what most theories import.

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(Silly question, sorry)

[Scott Morrison]

Okay, I've successfully combined Mitchell's and Johannes' work on subgroups, and my PR <https://github.com/leanprover/mathlib/pull/94> looks mostly good to me --- there are a few TODOs where I need help, in particular the typeclass resolution problem I was having earlier is still there; unfortunately Mario's suggestions don't seem to have helped.

[Scott Morrison]

Thanks, @Johannes Hölzl for merging that and making some final stylistic changes.

[Scott Morrison]

There's one change that I'd like to disagree with, however. I saw that you changed a number of group G to group α.

[Scott Morrison]

I know this is according to style.

[Scott Morrison]

I think @Kevin Buzzard and @Patrick Massot have already asked about this, but I want to add my vote too --- could we please consider changing the style rule so that types for which mathematicians would always use some particular letters for, can use those letters, rather than lower case greek letters?

[Scott Morrison]

I'm just not going to be taken seriously if I call a group α.

[Scott Morrison]

(As an aside, for a long time I've been making fun of (/exasperated by) physicists for using standard notations in the place of proper definitions --- just knowing that Z is a partition function, etc. I now feel properly chastised and sorry for my past bad behaviour, realising that I can't cope with groups that aren't called G.)

[Johannes Hölzl]

Hm, slightly prefer α as it is a type and not a group, i.e. it is only the groups support type. What I prefer in following this style is that I don't need to think how to call certain elements I just follow the general rules. Btw, I will change more, I simplified most of the proofs and generalized some statement.s

[Patrick Massot]

Really, groups should be called G. It only helps readability, especially since you also insist on separating the carrier type and the instance in (α : Type*) (β : Type*) [group α] [group β] instead of (α : Type*) [group α] (β : Type*) [group β]

[Mario Carneiro]

I don't see what the ordering of variables has to do with naming here. The idea is that greek letters label types (or "underlying sets" of things), while Groups would be labeled with G or H or whatever; it's just that these never come up because we don't use Group (the bundled one) in mathlib currently.

[Johan Commelin]

Patrick's point is that it is even less clear that one should think of \alpha and \beta as groups, because the place where they are introduced is visually not located next to the fact that you have an instance of group

[Johan Commelin]

Does it make sense what I am saying?

[Johan Commelin]

If it were ordered as (α : Type*) [group α] (β : Type*) [group β] that would improve readability, because one does not have to scan very far ahead to figure out that α is a group.

[Kevin Buzzard]

Is this really normal in computer science to demand that every variable of a certain type must be called one of three characters and that's the end of it?

[Kevin Buzzard]

From my point of view this is crazy.

[Patrick Massot]

Does this kind of convention exist in Isabelle? I checked it isn't use in Coq's Feit-Thompson stuff.

[Scott Morrison]

It's just going to make mathematicians' heads explode if groups aren't called G, rings R, categories 𝒞, manifolds M, etc. I've been convinced that typeclasses really are nice (after initially being very dubious), but if the expense is that the actual names of the things we're talking about never get mentioned (because it's rarely necessary to write [G : Group α]) then I'm going back to dubious.

[Scott Morrison]

Given that typeclass arguments rarely receive names, I think a good convention is just that, like in the usual mathematicians' convention, we use the same name for the "underlying thing" (i.e. the type) and the "extra structure on it". I agree that if they were being referred to separately it would be more correct to name the typeclass G and the type α, but when they're not I want to keep the name G.

[Kevin Buzzard]

It's not just that, it's just going to make arguments harder to follow. It's as simple as that.

[Johannes Hölzl]

In Isabelle type variables get a prime at the start, i.e. they are all names 'a, 'b, ... sometimes people are more specific and use 'state. But at least 'a, etc refer to alpha etc.

If we look now into group_theory.coset, the name $\alpha$ gets introduced at the beginning, and only occasionally refers to groups. So it doesn't make sense to call it G anymore. At least not globally in the file. We can give it different names in different section of that theory.