## Stream: maths

### Topic: zero group

#### 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?

unit

#### Chris Hughes (May 31 2019 at 10:17):

I vaguely remember Kenny doing this.

#### Mario Carneiro (May 31 2019 at 10:17):

I thought there were instances for it

#### Kevin Buzzard (May 31 2019 at 10:17):

We're looking for the trivial additive group

#### Kevin Buzzard (May 31 2019 at 10:17):

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

#### Mario Carneiro (May 31 2019 at 10:18):

it's not in mathlib

#### Mario Carneiro (May 31 2019 at 10:19):

maybe the PR stalled?

#### Neil Strickland (May 31 2019 at 10:20):

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

#### Mario Carneiro (May 31 2019 at 10:20):

that was where I expected to find it

#### Mario Carneiro (May 31 2019 at 10:21):

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

#### Kevin Buzzard (May 31 2019 at 10:22):

There is no mention of unit in algebra/pi_instances?

#### Kevin Buzzard (May 31 2019 at 10:22):

Oh I see -- we should have it there!

#### Mario Carneiro (May 31 2019 at 10:22):

like I said, it's not in mathlib

#### Mario Carneiro (May 31 2019 at 10:23):

it's in a PR or something

#### Mario Carneiro (May 31 2019 at 10:23):

or maybe just on Zulip in a code block

#### Kevin Buzzard (May 31 2019 at 10:24):

OK I don't want to get this wrong.

def zero_add_comm_group := unit

| _ _ := punit.star


Is it something like that?

#### Kevin Buzzard (May 31 2019 at 10:24):

Should punit.star get another name?

#### Mario Carneiro (May 31 2019 at 10:25):

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

#### Kevin Buzzard (May 31 2019 at 10:25):

Aah, () is better than punit.star?

no type renames

#### Kevin Buzzard (May 31 2019 at 10:25):

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

#### Kevin Buzzard (May 31 2019 at 10:25):

so we need to rename a type

#### Kevin Buzzard (May 31 2019 at 10:26):

We want zero_module G for G a group

?

#### Mario Carneiro (May 31 2019 at 10:26):

that's just module unit G

OK I see

#### 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

#### Mario Carneiro (May 31 2019 at 10:31):

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

#### Mario Carneiro (May 31 2019 at 10:33):

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

no

#### Kevin Buzzard (May 31 2019 at 10:33):

like unit can be a vector space over any field

#### Mario Carneiro (May 31 2019 at 10:33):

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

G is agroup

#### Mario Carneiro (May 31 2019 at 10:34):

is this something other than module then?

#### Mario Carneiro (May 31 2019 at 10:34):

module needs a ring and an add_comm_group

#### Mario Carneiro (May 31 2019 at 10:34):

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

#### Kevin Buzzard (May 31 2019 at 10:35):

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

t's not modules

#### Mario Carneiro (May 31 2019 at 10:36):

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

#### Mario Carneiro (May 31 2019 at 10:36):

that's not overloaded notation at all

carry on then

#### Keeley Hoek (May 31 2019 at 10:37):

actually, is there any representation theory in mathlib?

Not yet.

#### Kevin Buzzard (May 31 2019 at 10:37):

It will be really interesting to do

#### Kevin Buzzard (May 31 2019 at 10:38):

I am currently sitting with an UG doing G-modules

#### 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 ;-)

That sounds fun

#### Johan Commelin (May 31 2019 at 10:48):

@Kevin Buzzard There is a file algebra/punit_instances

#### Johan Commelin (May 31 2019 at 10:49):

@Ben McDonnell Is doing some representation theory

#### Johan Commelin (May 31 2019 at 10:49):

He just proved Schur's lemma yesterday (-;

#### Johan Commelin (May 31 2019 at 10:49):

But there is nothing in mathlib

#### Kevin Buzzard (May 31 2019 at 10:50):

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

#### Johan Commelin (May 31 2019 at 10:50):

Sure, we'll sort out the overlap later

#### 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