Zulip Chat Archive

Stream: maths

Topic: zero group


view this post on Zulip Kevin Buzzard (May 31 2019 at 10:16):

Do we have the trivial group? Or should I just make one myself? What is the underlying type?

view this post on Zulip Mario Carneiro (May 31 2019 at 10:16):

unit

view this post on Zulip Chris Hughes (May 31 2019 at 10:17):

I vaguely remember Kenny doing this.

view this post on Zulip Mario Carneiro (May 31 2019 at 10:17):

I thought there were instances for it

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:17):

We're looking for the trivial additive group

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:17):

It's not hard to make, I just don't want to duplicate stuff in mathlib

view this post on Zulip Mario Carneiro (May 31 2019 at 10:18):

it's not in mathlib

view this post on Zulip Mario Carneiro (May 31 2019 at 10:19):

maybe the PR stalled?

view this post on Zulip Neil Strickland (May 31 2019 at 10:20):

I think we should have lots of structures on unit in algebra/pi_instances.lean

view this post on Zulip Mario Carneiro (May 31 2019 at 10:20):

that was where I expected to find it

view this post on Zulip Mario Carneiro (May 31 2019 at 10:21):

and it was done, and it's somewhere, but I'm not sure where

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:22):

There is no mention of unit in algebra/pi_instances?

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:22):

Oh I see -- we should have it there!

view this post on Zulip Mario Carneiro (May 31 2019 at 10:22):

like I said, it's not in mathlib

view this post on Zulip Mario Carneiro (May 31 2019 at 10:23):

it's in a PR or something

view this post on Zulip Mario Carneiro (May 31 2019 at 10:23):

or maybe just on Zulip in a code block

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:24):

OK I don't want to get this wrong.

def zero_add_comm_group := unit

namespace zero_add_comm_group

def add : zero_add_comm_group -> zero_add_comm_group -> zero_add_comm_group
| _ _ := punit.star

Is it something like that?

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:24):

Should punit.star get another name?

view this post on Zulip Mario Carneiro (May 31 2019 at 10:25):

I think it was just instance : add_group unit := { add := \lam _ _, (), ... }

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:25):

Aah, () is better than punit.star?

view this post on Zulip Mario Carneiro (May 31 2019 at 10:25):

no type renames

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:25):

Aah, we really want the zero module for an arbitrary group

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:25):

so we need to rename a type

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:26):

We want zero_module G for G a group

view this post on Zulip Mario Carneiro (May 31 2019 at 10:26):

?

view this post on Zulip Mario Carneiro (May 31 2019 at 10:26):

that's just module unit G

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:26):

OK I see

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:26):

I'm glad I asked!

view this post on Zulip Mario Carneiro (May 31 2019 at 10:27):

this puts a bunch of structure on unit so now we can write () + () and 37 : unit and so on but I don't think this is a big problem

view this post on Zulip Mario Carneiro (May 31 2019 at 10:31):

Wouldn't zero_module G require G to be an add_comm_group?

view this post on Zulip Mario Carneiro (May 31 2019 at 10:33):

wait, wouldn't module unit G require G to be the trivial group?

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:33):

no

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:33):

like unit can be a vector space over any field

view this post on Zulip Mario Carneiro (May 31 2019 at 10:33):

because 0 * g = 0 and 1 * g = g

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:33):

G is agroup

view this post on Zulip Mario Carneiro (May 31 2019 at 10:34):

is this something other than module then?

view this post on Zulip Mario Carneiro (May 31 2019 at 10:34):

module needs a ring and an add_comm_group

view this post on Zulip Mario Carneiro (May 31 2019 at 10:34):

and unit is a ring, but it will force the add_comm_group to be trivial

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:35):

We're doing G-modules, it's something else

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:35):

t's not modules

view this post on Zulip Mario Carneiro (May 31 2019 at 10:36):

oh, well if you put a G in front...

view this post on Zulip Mario Carneiro (May 31 2019 at 10:36):

that's not overloaded notation at all

view this post on Zulip Mario Carneiro (May 31 2019 at 10:36):

carry on then

view this post on Zulip Keeley Hoek (May 31 2019 at 10:37):

actually, is there any representation theory in mathlib?

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:37):

Not yet.

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:37):

It will be really interesting to do

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:38):

I am currently sitting with an UG doing G-modules

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:38):

Aah, we really want the zero module for an arbitrary group

Obviously I meant the zero G-module ;-)

view this post on Zulip Keeley Hoek (May 31 2019 at 10:40):

That sounds fun

view this post on Zulip Johan Commelin (May 31 2019 at 10:48):

@Kevin Buzzard There is a file algebra/punit_instances

view this post on Zulip Johan Commelin (May 31 2019 at 10:49):

@Ben McDonnell Is doing some representation theory

view this post on Zulip Johan Commelin (May 31 2019 at 10:49):

He just proved Schur's lemma yesterday (-;

view this post on Zulip Johan Commelin (May 31 2019 at 10:49):

But there is nothing in mathlib

view this post on Zulip Kevin Buzzard (May 31 2019 at 10:50):

We're doing G-modules, so it's something else

view this post on Zulip Johan Commelin (May 31 2019 at 10:50):

Sure, we'll sort out the overlap later

view this post on Zulip Keeley Hoek (May 31 2019 at 10:50):

Schur's lemma is the second best lemma


Last updated: May 12 2021 at 07:17 UTC