zero group

Stream: maths

[Kevin Buzzard]

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

[Mario Carneiro]

unit

[Chris Hughes]

I vaguely remember Kenny doing this.

[Mario Carneiro]

I thought there were instances for it

[Kevin Buzzard]

We're looking for the trivial additive group

[Kevin Buzzard]

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

[Mario Carneiro]

it's not in mathlib

[Mario Carneiro]

maybe the PR stalled?

[Neil Strickland]

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

[Mario Carneiro]

that was where I expected to find it

[Mario Carneiro]

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

[Kevin Buzzard]

There is no mention of unit in algebra/pi_instances?

[Kevin Buzzard]

Oh I see -- we should have it there!

[Mario Carneiro]

like I said, it's not in mathlib

[Mario Carneiro]

it's in a PR or something

[Mario Carneiro]

or maybe just on Zulip in a code block

[Kevin Buzzard]

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?

[Kevin Buzzard]

Should punit.star get another name?

[Mario Carneiro]

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

[Kevin Buzzard]

Aah, () is better than punit.star?

[Mario Carneiro]

no type renames

[Kevin Buzzard]

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

[Kevin Buzzard]

so we need to rename a type

[Kevin Buzzard]

We want zero_module G for G a group

[Mario Carneiro]

?

[Mario Carneiro]

that's just module unit G

[Kevin Buzzard]

OK I see

[Kevin Buzzard]

I'm glad I asked!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

no

[Kevin Buzzard]

like unit can be a vector space over any field

[Mario Carneiro]

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

[Kevin Buzzard]

G is agroup

[Mario Carneiro]

is this something other than module then?

[Mario Carneiro]

module needs a ring and an add_comm_group

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

t's not modules

[Mario Carneiro]

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

[Mario Carneiro]

that's not overloaded notation at all

[Mario Carneiro]

carry on then

[Keeley Hoek]

actually, is there any representation theory in mathlib?

[Kevin Buzzard]

Not yet.

[Kevin Buzzard]

It will be really interesting to do

[Kevin Buzzard]

I am currently sitting with an UG doing G-modules

[Kevin Buzzard]

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

Obviously I meant the zero G-module ;-)

[Keeley Hoek]

That sounds fun

[Johan Commelin]

@Kevin Buzzard There is a file algebra/punit_instances

[Johan Commelin]

@Ben McDonnell Is doing some representation theory

[Johan Commelin]

He just proved Schur's lemma yesterday (-;

[Johan Commelin]

But there is nothing in mathlib

[Kevin Buzzard]

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

[Johan Commelin]

Sure, we'll sort out the overlap later

[Keeley Hoek]

Schur's lemma is the second best lemma