## Stream: new members

### Topic: Representation Theory

#### Jineon Baek (Oct 17 2019 at 01:39):

I was reading through a Representation Theory textbook and a question came to my mind: Have the theory been implemented in any LEAN library?

#### Scott Morrison (Oct 17 2019 at 01:59):

No, there's essentially no representation theory at this point (although there is some commutative algebra).

#### Jineon Baek (Oct 17 2019 at 02:36):

Thank you for answering. If so, how much it will be worth (for this community) to implement the theory in a library? It's a classical theory, but the fact that it is not yet implemented seems to somewhat imply that there are more urgent needs for other theories now. I want to know the context if any exists.

#### Johan Commelin (Oct 17 2019 at 02:42):

@Jineon Baek It only somewhat implies that we don't have enough people power. It's a relatively small group of contributors, and they just hack on whatever they think is fun.

#### Johan Commelin (Oct 17 2019 at 02:43):

There are several people on this chat that think that representation theory is extremely important. But we just haven't got round to doing anything so far.

#### Johan Commelin (Oct 17 2019 at 02:43):

At some point @Ben McDonnell started working on some rep.theory. Maybe he can share what he's got so far somewhere.

#### Scott Morrison (Oct 17 2019 at 03:02):

Yes, I'd love to see some! A lot depends on what generality you want to do things in, and often for mathlib the answer is "a lot of generality".

#### Scott Morrison (Oct 17 2019 at 03:03):

The theory of abelian categories is on the horizon, and might be useful to have in place, so if someone wants to work on that I'd be happy to provide some pointers (and get around to doing some of the things I promised to do).

#### Scott Morrison (Oct 17 2019 at 03:04):

But generally --- pick a (good) book, and have a go. :-)

#### Scott Morrison (Oct 17 2019 at 03:05):

I'd love to see someone start on Etingof's Representation Theory: http://www-math.mit.edu/~etingof/repb.pdf

#### Jineon Baek (Oct 17 2019 at 04:15):

Thanks for the input everyone! I'm a newbie both in this lean game and representation theory, so I'm thinking of learning both by implementing theorems in a textbook as I learn them like the 'intro to proof' course project.

#### Jineon Baek (Oct 17 2019 at 04:20):

Full generality is definitely what standard library should aim for though. If my own little project works out well I'll share. Would happy to hear pointers for a starting point. I'm wondering if I should give it a try for finite group rep. with finite dimensional vector space first, or in a bit more generality.

#### Scott Morrison (Oct 17 2019 at 04:24):

Why not try to prove the first interesting thing about finite group representations: averaging over the group is the projection onto the trivial isotypic component?

#### Scott Morrison (Oct 17 2019 at 04:25):

1. define the operator 1/|G| \Sigma_g g
2. prove that it is idempotent
3. prove that anything in its image is fixed by the group
4. prove that if you are fixed by every group element you are fixed by this operator

#### Scott Morrison (Oct 17 2019 at 04:27):

You'll need to see how to work with linear operators, and use finset.sum to handle the summations.

@Seewoo Lee

#### Johan Commelin (Oct 17 2019 at 05:50):

@Jineon Baek But certainly you will make your Lean life a lot easier by not putting those finiteness assumptions in your definition

#### Johan Commelin (Oct 17 2019 at 05:50):

1. prove that the subset of elements fixed by the group is a sub-vectorspace.

#### Kevin Buzzard (Oct 17 2019 at 06:46):

Representation theory is one of the many things on my list of stuff we need to get done at some point. It's a beautiful theory, and essentially self-contained. The first part of Serre's book would be the kind of goal we'd need

#### Kenny Lau (Oct 17 2019 at 08:04):

inb4 it's a special case of L^2(G) and Peter--Weyl theorem

#### Tim Daly (Oct 17 2019 at 19:59):

@Kevin Buzzard When we developed Axiom at IBM Research there was an effort made to invite and actively support people who worked in areas where we needed implementations, for example, in finite fields. It might be interesting to "talent search" among mathematicians and actively recruit their participation. Perhaps Microsoft could be convinced to do a "Microsoft Summer of Code", providing a summer support program for mathematicians with proposals for lean development.

#### Kevin Buzzard (Oct 18 2019 at 07:50):

I don't think we need a "person who works in representation theory" -- all we need is an intelligent undergraduate who is trained in type theory and is interested, and I'm sure I'll find one in the end.

#### Patrick Stevens (Mar 15 2020 at 09:22):

I've collected together some of the bits and pieces of mathlib that I will require to define linear representations, but I'm still too new to be able to assemble them into a definition. I think the following is all the component parts, but it's just a heap of nonsense at the moment. Would some kind soul be able to align them into something I can start expressing lemmas about? (I'll probably only need a few of this kind of really basic question before I can answer such trivia myself.)

One particular question I don't know the answer to: should I be expressing "linear representation" as a typeclass or merely a record?

Alternatively, is there some kind of Lean walkthrough of how to assemble a definition like this?

import algebra.field
import linear_algebra.finite_dimensional

universes u v w x
variables {U : Type u} {V : Type v}
variables [F : field]
variables [X : Set]
variables [V : vector_space F X]

-- Definition. Let V be a finite-dimensional vector space over F. A (linear) repre-
-- sentation of G on V is a homomorphism ρ = ρ_V : G → GL(V).

--def general_linear_group := units (M →ₗ[R] M)
--class is_group_hom [group α] [group β] (f : α → β) extends is_mul_hom f : Prop


#### Mario Carneiro (Mar 15 2020 at 09:28):

The variables are quite right. The variables are the underlying types, and the structures are anonymous typeclass variables. Like so:

variables {F : Type u} {V : Type v}
variables [field F]
variables [vector_space F V]


#### Mario Carneiro (Mar 15 2020 at 09:29):

Similarly, G is a group means variables {G : Type*} [group G]

#### Mario Carneiro (Mar 15 2020 at 09:30):

and then a linear representation would be an element of G ->* units (V ->l[F] V)

#### Patrick Stevens (Mar 15 2020 at 09:47):

Thanks. The way I had previously expected this to look was something like def linear_representation (p : G -> general_linear_group F (n -> F)) := is_monoid_hom p, but I suspect my mental model is wrong in a way that I don't understand (that line certainly doesn't compile). Is it clear to you what I've misunderstood?

#### Patrick Stevens (Mar 15 2020 at 09:50):

to be clear, I currently have:

import algebra.field
import linear_algebra.finite_dimensional
import linear_algebra.basic
import algebra.module

open linear_map

universes u v
variables {F : Type u} {V : Type v}
variables [discrete_field F]
variables (n : Type u) [fintype n] [decidable_eq n]
variables [field F]
variables {G : Type*} [add_comm_group G]
variables [vector_space F G]

def linear_representation (p : G -> general_linear_group F (n -> F)) := is_monoid_hom p


#### Mario Carneiro (Mar 15 2020 at 10:18):

You have two instances on F, one a field and one a discrete_field, that's definitely wrong. That is saying that F has two independent field structures. (In the latest version of lean/mathlib discrete_field has been renamed to field, replacing the original field.)

#### Mario Carneiro (Mar 15 2020 at 10:19):

It's true that I didn't say anything about the finite dimensionality in the version I gave. That could be a predicate on V, something like dim V < omega, although perhaps there's a typeclass for this now

#### Mario Carneiro (Mar 15 2020 at 10:20):

But in your version, vector_space F G means that G is the F-vector space

#### Mario Carneiro (Mar 15 2020 at 10:21):

which could be what you mean but doesn't match the math text in the comment

#### Mario Carneiro (Mar 15 2020 at 10:23):

The way you have set up linear_representation p is as a predicate on functions from G asserting that they are a linear representation, whereas the approach I gave takes linear representations to be the entire type G ->* units (V ->l[F] V), which bundles together the function with the proof that it is a group hom

#### Patrick Stevens (Mar 15 2020 at 10:24):

Mario Carneiro said:

which could be what you mean but doesn't match the math text in the comment

Ah, you're quite right - I don't know how I could have made that mistake :P

#### Mario Carneiro (Mar 15 2020 at 10:24):

mathlib is slowly moving away from unbundled homs like is_monoid_hom in favor of bundled homs like G ->+ H

#### Patrick Stevens (Mar 15 2020 at 10:24):

OK, that makes sense - thanks

#### Patrick Stevens (Mar 15 2020 at 10:41):

The flood of my questions should decay exponentially, but in the meantime: the following doesn't compile because "type expected at linear_representation" in the last line. How can I pass a linear representation into the function dimension?

import algebra.field
import linear_algebra.finite_dimensional
import linear_algebra.basic
import algebra.module
import algebra.group.hom

open linear_map

universes u
variables {F : Type u}
variables [discrete_field F]
variables (n : Type u) [fintype n] [decidable_eq n]
variables {V : Type*} [add_comm_group V]
variables {G : Type*} [group G]
variables [vector_space F V]

def linear_representation := monoid_hom G (general_linear_group F (n -> F))

noncomputable def dimension (p : linear_representation) := vector_space.dim V


#### Patrick Massot (Mar 15 2020 at 10:45):

Have a look at #check linear_representation

#### Patrick Massot (Mar 15 2020 at 10:46):

Maybe you don't quite understand how variable works yet.

#### Patrick Massot (Mar 15 2020 at 10:48):

Also try #check @linear_representation, and try to think about what is V at the very end of your code, and how it relates to p.

#### Patrick Stevens (Mar 15 2020 at 10:48):

Patrick Massot said:

Maybe you don't quite understand how variable works yet.

Ah right - again, I've been misled by Agda, which tends to do this via parameterised modules

#### Patrick Massot (Mar 15 2020 at 10:49):

There is also a problem which is completely independent of language differences.

#### Patrick Massot (Mar 15 2020 at 10:49):

Your V in the body of the definition has no relation whatsoever with p.

#### Patrick Massot (Mar 15 2020 at 10:50):

Your p obviously has dimension n by definition.

#### Patrick Stevens (Mar 15 2020 at 10:52):

Patrick Massot said:

Your p obviously has dimension n by definition.

You're right, I actually want the n from the body of linear_representation - but I am happy to leave questions like "have I got the definition correct" for the moment (I'll discover they're wrong as soon as I come to formulate any theorems) while I learn how to use Lean

#### Mario Carneiro (Mar 15 2020 at 10:53):

You have V and also n -> F as vector spaces. Which do you want?

#### Patrick Massot (Mar 15 2020 at 10:53):

In case this isn't clear: Mario's question is about the same topic as mine.

#### Mario Carneiro (Mar 15 2020 at 10:53):

linear_representation has too many implicit variables

#### Patrick Stevens (Mar 15 2020 at 10:54):

n -> F - but I can almost certainly work out how to do that by myself, once I've correctly passed a linear representation into dimension. I'll rejig it so that the right variables are explicit and then it'll probably all just fall out

Thanks

#### Mario Carneiro (Mar 15 2020 at 10:54):

you need to make the type variables explicit, and then write e.g. p : linear_representation F G V

#### Mario Carneiro (Mar 15 2020 at 10:54):

or linear_representation F G n if you want that version

#### Patrick Massot (Mar 15 2020 at 10:55):

That's why I wrote a bunch of #check

#### Mario Carneiro (Mar 15 2020 at 10:56):

If the definition has the form linear_representation F G n, then the dimension is n, and there is no need for a definition dimension. This is what patrick is saying

#### Patrick Massot (Mar 15 2020 at 10:56):

Because in this situation Lean will typically complain it cannot synthesize a term of typeType u without telling which implicit variable it wasn't able to synthesize and this is not easy to debug without #check

#### Kevin Buzzard (Mar 15 2020 at 11:36):

@Patrick Stevens field means different things in Lean 3.4.2 (the officially sanctioned version of Lean, which is frozen, as is mathlib support) and 3.6.1 (the community version, which current mathlib compiles with). I guess I'd recommend you use 3.6.1 but I just wanted to flag this now.

#### Kevin Buzzard (Mar 15 2020 at 11:53):

-- working with Lean 3.6.1 and current mathlib
-- don't need all of these imports for group_module
import algebra.field
import linear_algebra.finite_dimensional
import linear_algebra.basic
import algebra.module
import algebra.group.hom

class group_module (G : Type*) [group G] (M : Type*) [add_comm_group M]
extends  has_scalar G M :=
(one_smul : ∀ m : M, (1 : G) • m = m)
(smul_smul : ∀ g h : G, ∀ m : M, g • (h • m) = (g * h) • m)
(smul_add : ∀ g : G, ∀ m n : M, g • (m + n) = g • m + g • n)

attribute [simp] one_smul smul_smul smul_add -- I think?

namespace group_module

variables {G : Type*} [group G] {M : Type*} [add_comm_group M] [group_module G M]

@[simp] lemma smul_neg (g : G) (m : M) : g • (-m) = -(g • m) :=
begin
sorry
end

@[simp] lemma smul_zero (g : G) : g • (0 : M) = 0 :=
begin
sorry
end

@[simp] lemma smul_sub (g : G) (m n : M) : g • (m - n) = g • m - g • n :=
begin
sorry
end

end group_module

-- new file with more imports

class group_representation (G : Type*) [group G] (F : Type*) [field F]
(V : Type*) [add_comm_group V] [module F V] [group_module G V] :=
(smul_comm : ∀ (g : G) (μ : F) (v : V), g • (μ • v) = μ • (g • v) )

namespace group_representation

variables {G : Type*} [group G] {F : Type*} [field F]
{V : Type*} [add_comm_group V] [module F V] [group_module G V]

noncomputable def dim (p : group_representation G F V) := vector_space.dim V

end group_representation


There's my effort, but definitions are not my strong point.

#### Kevin Buzzard (Mar 15 2020 at 11:53):

There should really be a bunch of lemmas about group_module first, because this is a simpler object (no field involved)

#### Kevin Buzzard (Mar 15 2020 at 11:54):

furthermore the definitions should be in two different files really, because someone interested in group cohomology might not want to import the representation theory stuff.

#### Patrick Stevens (Mar 15 2020 at 11:58):

The following doesn't compile because "maximum class-instance resolution depth has been reached" on the last line for monoid_hom; presumably that means Lean can't figure out that I've specified a homomorphism, so I need to supply an instance of is_monoid_hom to go with the lambda-term.

import algebra.field
import linear_algebra.finite_dimensional
import linear_algebra.basic
import algebra.module
import algebra.group.hom

open linear_map

universes u v
variables (F : Type u)
variables [discrete_field F]

def linear_representation
(G : Type*) [group G]
(V : Type*) [add_comm_group V] [vector_space F V]
(n : Type v) [fintype n] [decidable_eq n]
:=
monoid_hom G (general_linear_group F (n -> F))

def trivial_representation {G : Type*} [group G] : linear_representation F G F (fin 1) :=
monoid_hom.of (λ g, general_linear_group.of_linear_equiv (linear_equiv.refl (fin 1 -> F)))


But my best attempt at that instance is the following, which doesn't compile ("don't know how to synthesize placeholder" on general_linear_group):

instance identity_is_hom (G : Type*) [monoid G] : is_monoid_hom (λ (g : G), general_linear_group.of_linear_equiv (linear_equiv.refl (fin 1 -> F))
by sorry


This problem persists even if I supply F as well (i.e. prepend the arguments (F : Type*) [discrete_field F] to identity_is_hom). It's not clear to me that I can supply any more information to Lean here; what have I missed?

#### Patrick Stevens (Mar 15 2020 at 11:59):

Kevin Buzzard said:

There should really be a bunch of lemmas about group_module first, because this is a simpler object (no field involved)

Fair enough - I'm using this more as a "learn Lean" exercise than a "produce something to go into mathlib" at the moment, so am happy just playing around with the definitions at the moment

#### Kevin Buzzard (Mar 15 2020 at 12:00):

OK I'll take a look at your version.

#### Kevin Buzzard (Mar 15 2020 at 12:02):

Which version of Lean are you using?

#### Kevin Buzzard (Mar 15 2020 at 12:05):

Your def of linear_representation has a V as an input which is never used

#### Patrick Stevens (Mar 15 2020 at 12:05):

Kevin Buzzard said:

Which version of Lean are you using?

leanprover-community/lean:3.5.1, according to my leanpkg.toml

#### Kevin Buzzard (Mar 15 2020 at 12:06):

You should probably upgrade because I just noticed that it's a pain to look at your code because of all this deprecated discrete_field stuff. There will be a painless way to do it with leanproject I suspect.

#### Patrick Stevens (Mar 15 2020 at 12:06):

Kevin Buzzard said:

You should probably upgrade because I just noticed that it's a pain to look at your code because of all this deprecated discrete_field stuff. There will be a painless way to do it with leanproject I suspect.

OK, thanks - I'll do that before anything else

#### Kevin Buzzard (Mar 15 2020 at 12:06):

@Mario Carneiro what do you think of my version by the way? Once we have the definitions right the lemmas should be fun, but the definitions are a minefield.

#### Mario Carneiro (Mar 15 2020 at 12:11):

I think it should be a monoid rather than a group

#### Mario Carneiro (Mar 15 2020 at 12:11):

it also looks suspiciously like a group action

#### Patrick Stevens (Mar 15 2020 at 12:11):

It is a group action

#### Kevin Buzzard (Mar 15 2020 at 12:11):

A group module is a group action by module homs

#### Kevin Buzzard (Mar 15 2020 at 12:11):

Mario is pointing out that it could extend group actions

#### Mario Carneiro (Mar 15 2020 at 12:13):

You also get a bunch of theorems for free if you don't define this at all and use the high level characterization instead

#### Kevin Buzzard (Mar 15 2020 at 12:14):

I'm not sure what you mean, but whatever you mean I suspect people will want this in practice.

#### Mario Carneiro (Mar 15 2020 at 12:14):

Don't you get all this if you just say linear_representation := G ->* units (V ->l[F] V)?

Yes absolutely

#### Mario Carneiro (Mar 15 2020 at 12:15):

it's not clear to me what the tradeoffs are here

#### Kevin Buzzard (Mar 15 2020 at 12:15):

Is that a high-level characterisation? There is another one -- there's a ring G ->_0 F called the group ring, and a group representation is the same thing as a module over that ring

#### Mario Carneiro (Mar 15 2020 at 12:16):

sure, any of those sound good to me

#### Kevin Buzzard (Mar 15 2020 at 12:16):

You're a computer scientist so can see advantages in the compactness

#### Kevin Buzzard (Mar 15 2020 at 12:16):

It's less clear to me

#### Mario Carneiro (Mar 15 2020 at 12:16):

Isn't this usually how the mathematicians do it?

#### Kevin Buzzard (Mar 15 2020 at 12:16):

I would prefer clarity

#### Mario Carneiro (Mar 15 2020 at 12:17):

I feel like we've swapped sides of this argument

#### Kevin Buzzard (Mar 15 2020 at 12:17):

If you define it as a module over the group ring then all of a sudden you don't have g \bub v you have \u g \bub v etc

#### Kevin Buzzard (Mar 15 2020 at 12:17):

and these invisible functions can cause confusion, make rewriting harder etc

#### Mario Carneiro (Mar 15 2020 at 12:18):

remind me who is playing the role of the CS guy again

#### Kevin Buzzard (Mar 15 2020 at 12:18):

With your approach there are coercions to fun etc, whereas sometimes g \bub v is just the thing you want.

#### Kevin Buzzard (Mar 15 2020 at 12:19):

My understanding here is that there is no perfect solution.

#### Mario Carneiro (Mar 15 2020 at 12:19):

That's certainly going to be the case

#### Kevin Buzzard (Mar 15 2020 at 12:19):

how about you CS guys make the system we want then ;-)

#### Mario Carneiro (Mar 15 2020 at 12:19):

Like I said, there is a tradeoff here and I don't have a good grasp of it

#### Kevin Buzzard (Mar 15 2020 at 12:20):

because you don't know what mathematicians actually use group representations for. This is why we need the area to get bigger, we need people who are experts at everything at once.

#### Kevin Buzzard (Mar 15 2020 at 12:21):

Mathematicians just invoke the invisible function machine and pass seamlessly from one concept to the other

#### Mario Carneiro (Mar 15 2020 at 12:21):

I have already argued that DTT is the problem but you're already bought in so ¯\_(ツ)_/¯

#### Kevin Buzzard (Mar 15 2020 at 12:21):

and we don't check the diagrams commute because this is trivial

#### Mario Carneiro (Mar 15 2020 at 12:21):

in set theory it really is that easy to pass between representations

#### Kevin Buzzard (Mar 15 2020 at 12:21):

I'm not going back to assembly language now

#### Mario Carneiro (Mar 15 2020 at 12:22):

to use a rust analogy, I don't want assembly language, I want unsafe blocks

#### Kevin Buzzard (Mar 15 2020 at 12:24):

You lost me :-/ but I'm happy to hear more.

#### Mario Carneiro (Mar 15 2020 at 12:24):

I want the ability to get around the type system without it getting mad at me forever

#### Mario Carneiro (Mar 15 2020 at 12:24):

In set theory if x \in A and A = B then x \in B

#### Mario Carneiro (Mar 15 2020 at 12:25):

in type theory this will cause the proof assistant to hate you forever

#### Kevin Buzzard (Mar 15 2020 at 12:25):

@Patrick Stevens the problem with your code, I guess, is that you've defined a function j from G to general_linear_group F (fin 1 → F) but Lean has no particular reason to know that this function has the property that j(g*h)=j(g)*j(h).

#### Kevin Buzzard (Mar 15 2020 at 12:26):

Mario Carneiro said:

in type theory this will cause the proof assistant to hate you forever

In type theory we have to insert an invisible coercion from A to B and then coerce x over.

#### Mario Carneiro (Mar 15 2020 at 12:26):

it's not invisible

I wish it was

#### Mario Carneiro (Mar 15 2020 at 12:27):

we try very hard to make it not too annoying with mixed success

#### Kevin Buzzard (Mar 15 2020 at 12:27):

Sure -- I just meant "invisible to mathematicians"

#### Kevin Buzzard (Mar 15 2020 at 12:27):

and we have a rather liberal notion of =

#### Mario Carneiro (Mar 15 2020 at 12:28):

I think that lean is a great system, probably the best among all systems I know at the user experience. I also think that this property has almost nothing to do with the fact that it implements DTT

#### Kevin Buzzard (Mar 15 2020 at 12:29):

We understand the concept of an equivalence of categories, but all these structures on one vector space V (a linear action of a group, a group hom to the automorphisms, a module for the group ring) are all equal because they are simply different ways of packing up precisely the same information. They are a tedious implementation issue which we cunningly avoid by seamlessly changing our implementation decisions mid-proof.

#### Mario Carneiro (Mar 15 2020 at 12:30):

in lean, we can do this with equivs of various kinds, and maybe this will eventually be packed into some category machinery

#### Mario Carneiro (Mar 15 2020 at 12:31):

but I do think it is essential to be able to do concrete work in any of those representations

#### Kevin Buzzard (Mar 15 2020 at 12:31):

#check @monoid_hom.of
/-
monoid_hom.of :
Π {M : Type u_3} {N : Type u_4} [mM : monoid M] [mN : monoid N] (f : M → N) [h : is_monoid_hom f], M →* N
-/


Patrick -- this definition of monoid_hom.of says "you give me a map f and I will then use type class inference to find a term h of type is_monoid_hom f. Once I've found it I'll give you back a monoid homomorphism (which is essentially the pair consisting of f and h).

#### Patrick Stevens (Mar 15 2020 at 12:31):

Yep, I'd got that far - I'm struggling to construct that term though

#### Kevin Buzzard (Mar 15 2020 at 12:31):

The type class inference system is a bunch of lemmas of the form "a ring homomorphism is a monoid homomorphism" etc.

#### Patrick Stevens (Mar 15 2020 at 12:32):

The following doesn't compile, for example, because "don't know how to synthesize placeholder" at general_linear_group:

instance identity_is_hom (F : Type*) [discrete_field F] (G : Type*) [monoid G] : is_monoid_hom (λ (g : G), general_linear_group.of_linear_equiv (linear_equiv.refl (fin 1 -> F))) :=
by sorry


#### Kevin Buzzard (Mar 15 2020 at 12:34):

It will probably know that general_linear_group X Y is a group and hence a monoid but it won't know that your map is a monoid hom.

#### Kevin Buzzard (Mar 15 2020 at 12:34):

The issue with the synthesizing placeholder will be that Lean can't figure out which ring you're working over.

#### Patrick Stevens (Mar 15 2020 at 12:34):

I was hoping to tell it this was a hom, in the bit where I currently have sorry

#### Kevin Buzzard (Mar 15 2020 at 12:35):

Before the sorry Lean is failing to elaborate the term.

#### Kevin Buzzard (Mar 15 2020 at 12:35):

It can't figure out the type of linear_equiv.refl (fin 1 -> F)

#### Kevin Buzzard (Mar 15 2020 at 12:36):

The type is that (fin 1 -> F) is isomorphic to itself as a module over...some metavariable.

#### Kevin Buzzard (Mar 15 2020 at 12:37):

instance identity_is_hom (F : Type*) [discrete_field F] (G : Type*) [monoid G] :
is_monoid_hom (λ (g : G), @general_linear_group.of_linear_equiv F _ _ _ _ (linear_equiv.refl (fin 1 -> F))) :=
by sorry


#### Kevin Buzzard (Mar 15 2020 at 12:39):

The variable inputs in {} brackets are ones which are supposed to be inferred by unification, but we're claiming that the identity map fin 1 -> F is R-linear where R is a ring acting on fin 1 -> F and we give no indication as to what this ring is. Whatever R is, this theorem is still true. My gut feeling is that your problem has come from a possibly questionable design decision to make the R input implicit.

#### Patrick Stevens (Mar 15 2020 at 12:39):

Ooh, yuck - thanks; in Agda you can supply any particular implicit variable, like f {A = B} arg1 {C = C} arg2 where A and C were implicit args. It looks like in Lean you can only "make all args explicit"?

#### Kevin Buzzard (Mar 15 2020 at 12:39):

PS I am now talking to you as if you were an expert. Let me know if I'm going over your head.

#### Kevin Buzzard (Mar 15 2020 at 12:40):

Yes, you can make all args explicit or none of them! That is a really cool agda thing, I wish we had that in Lean.

#### Patrick Stevens (Mar 15 2020 at 12:40):

Yep, I see what you mean

#### Kevin Buzzard (Mar 15 2020 at 12:40):

@Mario Carneiro can you just pop that into 3.7.2 for us?

#### Mario Carneiro (Mar 15 2020 at 12:41):

there is a concrete syntax for this in lean 4 but I forget what it is

#### Mario Carneiro (Mar 15 2020 at 12:42):

if we used that notation it would get confused with passing a singleton of an equality to f

#### Kevin Buzzard (Mar 15 2020 at 12:43):

MS should employ an intern who gets an email whenever an issue like this comes up, and solves it manually

#### Kevin Buzzard (Mar 15 2020 at 12:43):

Oh here's a better idea -- just use a new kind of bracket.

#### Mario Carneiro (Mar 15 2020 at 12:43):

Even if it did exist, the name of the argument could only possibly be the name of the binder, and typeclass args always have ugly names like _inst_1

#### Kevin Buzzard (Mar 15 2020 at 12:43):

Why are we using {} for both implicit variable and set notation anyway?

#### Kevin Buzzard (Mar 15 2020 at 12:44):

Here we were missing R not some typeclass thing. The issue here was with unification failing, not type class inference.

#### Mario Carneiro (Mar 15 2020 at 12:44):

Binders are always distinguishable because they come after binding notation tokens

#### Mario Carneiro (Mar 15 2020 at 12:44):

but implicit function args are just in regular expression position

#### Kevin Buzzard (Mar 15 2020 at 12:45):

Mathematicians got {} first for sets, you just need some wacky unicode for your implicit instances and then we're all set.

#### Mario Carneiro (Mar 15 2020 at 12:46):

there is no problem with binders because they only come after \lam and stuff

#### Mario Carneiro (Mar 15 2020 at 12:46):

\lam {x | x > 0} doesn't make any sense

#### Kevin Buzzard (Mar 15 2020 at 12:46):

I don't know what a binder is. I thought that was forall etc.

yes

#### Mario Carneiro (Mar 15 2020 at 12:46):

\Pi, \forall, \lam, \sum, etc

#### Kevin Buzzard (Mar 15 2020 at 12:46):

linear_equiv.refl :
Π {R : Type u_3} (M : Type u_4) [_inst_1 : ring R] [_inst_2 : add_comm_group M] [_inst_5 : module R M], M ≃ₗ[R] M


Should R be explicit here?

I think so

#### Kevin Buzzard (Mar 15 2020 at 12:47):

I am confused about what binders have to do with the fact that I just had to write @foo F _ _ _ _

#### Mario Carneiro (Mar 15 2020 at 12:47):

There are no binders involved in the expression @foo F _ _ _ _

#### Kevin Buzzard (Mar 15 2020 at 12:47):

whereas I wanted to write foo {R = F}

#### Mario Carneiro (Mar 15 2020 at 12:48):

but {R = F} is actually a valid expression, of type set Prop

#### Kevin Buzzard (Mar 15 2020 at 12:48):

and that's why I'm saying you should keep your grubby implicit variable hands off our set notation and come up with some different bracket system.

#### Mario Carneiro (Mar 15 2020 at 12:48):

which is kind of nonsense, but foo might nevertheless have type set Prop -> T and then foo {R = F} is valid

#### Mario Carneiro (Mar 15 2020 at 12:49):

Oh, if the notation is something other than @foo {R = F} then we're fine probably

#### Kevin Buzzard (Mar 15 2020 at 12:49):

or treat us like dirt, like you usually do, and make us use different weird brackets so as to confuse the regular mathematicians

#### Mario Carneiro (Mar 15 2020 at 12:49):

I mean we already have those funny unicode brackets that are a pain to type for semi implicit

#### Kevin Buzzard (Mar 15 2020 at 12:49):

You wouldn't believe how many times I've been asked why 2 | 4 throw up wacky errors

#### Kevin Buzzard (Mar 15 2020 at 12:50):

when it works in LaTeX

#### Mario Carneiro (Mar 15 2020 at 12:50):

2 \mid 4 is the way to do it in latex

#### Kevin Buzzard (Mar 15 2020 at 12:50):

(actually it doesn't even work in LaTeX, the glue is incorrect and the user should use \mid ;-) )

#### Mario Carneiro (Mar 15 2020 at 12:51):

Because of the possibility of conflict, it seems pretty sensitive what notation is used for passing implicit arguments like this. I should see what lean 4 picked

#### Mario Carneiro (Mar 15 2020 at 12:52):

but yes, if it's some foo {<<R = F>>} thing then we're fine

#### Mario Carneiro (Mar 15 2020 at 12:52):

then again, typing that may become annoying

syntax is hard

#### Kevin Buzzard (Mar 15 2020 at 12:53):

You all seem to be happy with all that >=-+ monad stuff

#### Patrick Stevens (Mar 15 2020 at 12:53):

This is a feature that isn't meant to be used very often

#### Kevin Buzzard (Mar 15 2020 at 12:54):

So what you're saying is that instead of all this bracket banter I should just be making a PR changing {R} to (R)? :-)

#### Kevin Buzzard (Mar 15 2020 at 12:54):

unfortuately it won't work for 3.4.2 ;-)

#### Kevin Buzzard (Mar 15 2020 at 12:56):

instance identity_is_hom (F : Type*) [discrete_field F] (G : Type*) [monoid G] :
is_monoid_hom (λ (g : G), @general_linear_group.of_linear_equiv F _ _ _ _ (linear_equiv.refl (fin 1 -> F))) :=
{ map_mul := sorry,
map_one := sorry }


is how to make the instance, in case you didn't know Lean syntax

#### Kevin Buzzard (Mar 15 2020 at 12:57):

I got this in VS Code by writing ... := {! !} and then clicking on the little lightbulb which appeared and selecting "create a skeleton"

#### Patrick Stevens (Mar 15 2020 at 18:44):

It's really hard to Google for the example keyword :P is it possible for me to name an example, or do I have to make it a def if I want to refer to it? Currently I have a definition which works, and now I want to run it through #check but I can't work out how to refer to it.

-- Trivial representation
example {G : Type*} [group G] : linear_representation F G F :=
{
to_fun := λ g, general_linear_group.of_linear_equiv (linear_equiv.refl _),
map_one' := by exact rfl,
map_mul' := by
begin
intros g h,
exact rfl,
end
}


#### Daniel Keys (Mar 15 2020 at 18:51):

You can try giving it a name, like so: def even (n : ℤ) := 2 ∣ n

#### Patrick Stevens (Mar 15 2020 at 18:51):

Daniel Keys said:

You can try giving it a name, like so: def even (n : ℤ) := 2 ∣ n

Sure, I was just wondering if I could use the example syntax to name an example, or whether I was forced to use def

#### Daniel Keys (Mar 15 2020 at 18:52):

I think you need to make it a lemma or theorem in order to give it a name.

#### Patrick Stevens (Mar 21 2020 at 09:52):

Here's a stupid question: I've defined some stuff, and I want to #eval it to see whether it looks right (before I start going to the effort of proving things about it). For example, I've defined the dimension of a representation, and I want to check that the dimension of a certain representation is in fact 2 when I expect it to be. But for the life of me I can't find any actual examples of groups in mathlib (and so I have nothing to pass into #eval): the cyclic groups seem not to have been defined, Q and R appear not to have been endowed with group structures, etc. Are there actually any groups anywhere? And how should I be trying to find them in mathlib?

#### Johan Commelin (Mar 21 2020 at 09:54):

Hmm... such examples are certain there.

#### Johan Commelin (Mar 21 2020 at 09:54):

Q and R are both endowed with the structure of a linearly ordered field, so in particular they are additive groups

#### Johan Commelin (Mar 21 2020 at 09:55):

But #eval cannot compute a dimension for you

#### Johan Commelin (Mar 21 2020 at 09:55):

(It would have to cook up a basis, etc...)

#### Patrick Stevens (Mar 21 2020 at 09:55):

My current problem is simply an inability to synthesise a typeclass instance for group R, for example

#### Johan Commelin (Mar 21 2020 at 09:55):

On the other hand, there is certainly a theorem in mathlib saying that K^n has dimension n over K.

#### Johan Commelin (Mar 21 2020 at 09:56):

Because it's not a group. It's an add_group.

#### Johan Commelin (Mar 21 2020 at 09:56):

This is very unfortunate.

#### Patrick Stevens (Mar 21 2020 at 09:56):

Oh, that's very upsetting

#### Johan Commelin (Mar 21 2020 at 09:56):

But in the current setup, we need to duplicate groups to distinguish between multiplicative and additive groups

#### Johan Commelin (Mar 21 2020 at 09:56):

If we don't do that, we cannot have nice notation.

#### Johan Commelin (Mar 21 2020 at 09:57):

On the other hand, this is mostly done completely automatically. You prove things for multiplicative groups, and you are done.

#### Johan Commelin (Mar 21 2020 at 09:57):

So you get monoid R and add_group R in your case.

#### Patrick Stevens (Mar 21 2020 at 09:57):

So it's just a matter of taste whether you want to use add_group or group in a particular theory?

#### Johan Commelin (Mar 21 2020 at 09:59):

Well, mostly yes.

#### Johan Commelin (Mar 21 2020 at 10:00):

But the machinery can turn generate an additive version of a multiplicative definition/theorem, but not the other way round.

#### Johan Commelin (Mar 21 2020 at 10:00):

So all the generalities are developed using multiplicative notation.

#### Johan Commelin (Mar 21 2020 at 10:00):

But stuff like modules and representations assumes additive groups

#### Patrick Stevens (Mar 21 2020 at 10:01):

Was that a mistake? Should they not use the phrasing that affords more generality, i.e. multiplicative?

#### Johan Commelin (Mar 21 2020 at 10:07):

No, because of the notation.

#### Johan Commelin (Mar 21 2020 at 10:07):

If M is an R-module, you want to me able to write $r \cdot (x + y)$ for r : R and x y : M

#### Johan Commelin (Mar 21 2020 at 10:08):

I agree that it's confusing. (The mathematician in me is still unhappy about it.) But in practice it works quite well.

#### Johan Commelin (Mar 21 2020 at 10:09):

So, the magic command to make a multiplicative theorem additive is

@[to_additive]
theorem my_multiplicative_thm ...


#### Johan Commelin (Mar 21 2020 at 10:09):

Besides that, if G is a group, then additive G is an add_group. (The only thing this does is switch notation.)
Analogously multiplicative A turns an additive group into a multiplicative one.

#### Johan Commelin (Mar 21 2020 at 10:10):

Together, this gives a system that's quite flexible, and has nice notation.

#### Patrick Stevens (Mar 21 2020 at 11:09):

The following code doesn't compile because I haven't defined a relation: the type is not X -> X -> Prop because the type of is_isomorphic here is linear_representation _ _ V1 -> linear_representation _ _ V2 -> Prop. I could solve this by splitting the definition into two: linear_representation_over_a_specific_vector_space (name TBD), and convert linear_representation to being instead a dependent pair of (vector space, representation on that vector space), but this seems a little sad. Can anyone see anything nicer I could do?

import algebra.field
import linear_algebra.finite_dimensional
import linear_algebra.basic
import algebra.module
import algebra.group.hom

open linear_map

universes u v
variables (F : Type u)
variables [field F]

def linear_representation
(G : Type*) [group G]
(V : Type*) [add_comm_group V] [vector_space F V]
:=
monoid_hom G (general_linear_group F V)

-- is_intertwining_map is the same as "being a G-homomorphism"
def is_intertwining_map
{G : Type*} [group G]
{V1 : Type*} [add_comm_group V1] [vector_space F V1]
{V2 : Type*} [add_comm_group V2] [vector_space F V2]
(p1 : linear_representation F G V1)
(p2 : linear_representation F G V2)
(φ : linear_map F V1 V2)
:=
∀ (g : G), ∀ (x : V1),
linear_map.to_fun φ (units.val (monoid_hom.to_fun p1 g) x) = (units.val (monoid_hom.to_fun p2 g)) (linear_map.to_fun φ x)

def is_isomorphism
{G : Type*} [group G]
{V1 : Type*} [add_comm_group V1] [vector_space F V1]
{V2 : Type*} [add_comm_group V2] [vector_space F V2]
(p1 : linear_representation F G V1)
(p2 : linear_representation F G V2)
(φ : linear_map F V1 V2)
:=
is_intertwining_map F p1 p2 φ ∧ function.bijective (linear_map.to_fun φ)

def is_isomorphic
{G : Type*} [group G]
{V1 : Type*} [add_comm_group V1] [vector_space F V1]
{V2 : Type*} [add_comm_group V2] [vector_space F V2]
(p1 : linear_representation F G V1)
(p2 : linear_representation F G V2)
:=
∃ φ, is_isomorphism F p1 p2 φ

lemma isomorphism_rel_is_reflexive
{G : Type*} [group G]
{V1 : Type*} [add_comm_group V1] [vector_space F V1]
{V2 : Type*} [add_comm_group V2] [vector_space F V2]
: reflexive (@is_isomorphic F _ G _ V1 _ _ V2 _ _) -- doesn't compile
:=
by sorry
end


#### Patrick Stevens (Mar 21 2020 at 12:06):

I restructured in that way and it does work, of course, although it's a bit gross

#### Mario Carneiro (Mar 21 2020 at 13:26):

An example of an actual group in mathlib would be units. For example units (zmod 42) is an interesting, nontrivial and computable finite multiplicative group

#### Kevin Buzzard (Mar 21 2020 at 13:31):

The way this would be usually done in mathlib is that first you define a bunded intertwining_map, and then you would define the identity intertwining map, and a composition of intertwining maps, and you would define an isomorphism to be an intertwining map with an inverse. I don't think I understand your question about reflexive. Surely the assertion that the relation is reflexive is that V1 is isomorphic to V1, I don't see the role of V2.

#### Kevin Buzzard (Mar 21 2020 at 13:33):

But here you don't really want to use equivalence relations anyway, because they lose track of data. A mathematician would say "if V1 is isomorphic to V2 then V2 is isomorphic to V1" but this is less than what they mean. They mean "if you have an isomorphism V1 -> V2 then I can give you an isomorphism V2 -> V1, namely its inverse", and you would to well to capture this stronger statement.

#### Kevin Buzzard (Mar 21 2020 at 13:38):

You should look at how it is set up for modules. Because a group representation is just a module for the group ring, you are just re-doing that theory anyway. Here are module homomorphisms in mathlib. Instead of making the predicate on a homomorphism of additive abelian groups, they bundle everything up in a structure and then define id and comp -- these are the fundamental things you need to make everything into a category.

#### Kevin Buzzard (Mar 21 2020 at 13:44):

The reason that you don't see statements such as isomorphism being reflexive, symmetric etc is that everything like that is already done in some huge generality in files like this. This is a definition, not a theorem, it's the construction of the identity map and the proof that it preserves multiplication on any type with a multiplication. This is some abstract theory of "mul-equiv"s, which means bijections between two sets X and Y with multiplication, such that the bijection preserves the multiplication. Things like that get set up in huge generality and then the idea is that it will apply to your situation if you need it.

#### Patrick Stevens (Mar 21 2020 at 13:52):

Kevin Buzzard said:

But here you don't really want to use equivalence relations anyway, because they lose track of data. A mathematician would say "if V1 is isomorphic to V2 then V2 is isomorphic to V1" but this is less than what they mean. They mean "if you have an isomorphism V1 -> V2 then I can give you an isomorphism V2 -> V1, namely its inverse", and you would to well to capture this stronger statement.

Ah, again this is a habit imported from Agda, where to say that A is iso to B is to exhibit an isomorphism

#### Patrick Stevens (Mar 21 2020 at 13:52):

There is an awful lot to unlearn here :P

#### Johan Commelin (Mar 21 2020 at 13:53):

In Lean, you say that A and B are equiv, which is also an explicit iso.

#### Kevin Buzzard (Mar 21 2020 at 14:08):

@Patrick Stevens your definition of is_isomorphism is a Prop, so when you prove the isomorphism you'll have to exhibit the map, but the moment the proof has compiled the map will be forgotten, because Lean's Prop is...umm..I think it's called impredicative.

#### Patrick Stevens (Mar 21 2020 at 14:12):

Fair enough - I just need to get much more clear about what is constructive and what isn't

#### Patrick Massot (Mar 21 2020 at 14:33):

Kevin Buzzard said:

because Lean's Prop is...umm..I think it's called impredicative.

No, that's not what impredicative means. https://en.wikipedia.org/wiki/Impredicativity

#### Kevin Buzzard (Mar 21 2020 at 14:34):

well, Lean's prop is forgetful

#### Mario Carneiro (Mar 21 2020 at 14:34):

that would be proof irrelevance

#### Kevin Buzzard (Mar 21 2020 at 14:34):

There is no generally accepted precise definition of what it means to be predicative or impredicative

#### Kevin Buzzard (Mar 21 2020 at 14:34):

that's the last time I'm using that word. It's as bad as canonical.

#### Mario Carneiro (Mar 21 2020 at 14:34):

we can say that Prop is a proof irrelevant universe

#### Mario Carneiro (Mar 21 2020 at 14:36):

I don't think I agree with the wikipedia statement. The meaning of impredicativity is context dependent but precise in most places where it appears

#### Mario Carneiro (Mar 21 2020 at 14:37):

Almost all the uses you are likely to have seen are using the same meaning. Alternate meanings are mostly historical and philosophical uses like avoiding self reference in the liar's paradox

#### Patrick Massot (Mar 21 2020 at 14:39):

And this meaning is somehow orthogonal to proof irrelevance, right?

#### Mario Carneiro (Mar 21 2020 at 14:40):

they are related by a paradox that makes one of the possible permutations inconsistent

#### Scott Morrison (Mar 21 2020 at 19:10):

@Patrick Stevens , could you have a look at #2121, as a "rather bundled" suggestion for the basics of representation theory?

#### Alex J. Best (Mar 22 2020 at 02:08):

Mario Carneiro said:

An example of an actual group in mathlib would be units. For example units (zmod 42) is an interesting, nontrivial and computable finite multiplicative group

You can also do units of a general linear group to get some fun non-abelian computable groups.

#### Floris van Doorn (Apr 13 2020 at 18:22):

I'm planning to do some representation theory with @Michael R Douglas. Do you think that is helpful, or are we then stepping on someone's toes? (@Scott Morrison and @Patrick Stevens might be working on the same or similar stuff)?

#### Johan Commelin (Apr 13 2020 at 18:24):

The basic definitions will be the same as for group cohomology. @Kevin Buzzard and some of his students have done a bunch there.

#### Kevin Buzzard (Apr 13 2020 at 18:51):

The reason this never gets done is the usual (see graphs, or Cauchy's integral formula, or ...): people haven't yet decided on what the definition should be.

#### Kevin Buzzard (Apr 13 2020 at 18:52):

Should one just define a representation of a group to be, by definition, a module over the group ring? Or should one make a new class of a vector space (or more generally module -- please set it up over modules over a commutative ring rather than vector spaces over a field) equipped with an action of G?

#### Kevin Buzzard (Apr 13 2020 at 18:54):

https://github.com/Shenyang1995/M4R/blob/66f1450f206dc05c3093bc4eaa1361309bf8633b/src/G_module/basic.lean#L10-L14 I need advice about whether this is the best idea. I don't have enough experience to know. Mario and I talked about this a week or two ago, I'll find the link. I'm not sure we came to any conclusions though, just like when we talk about what generality to define a contour integral in...

#### Kevin Buzzard (Apr 13 2020 at 18:57):

(oh, it's just earlier in this thread)

#### Scott Morrison (Apr 14 2020 at 00:50):

I did do a little, but got distracted trying to fix up monoid_algebra and its associated theorems. There's a lot still missing there.

#### Scott Morrison (Apr 14 2020 at 00:51):

I think it's best to have separate notions for a group acting on something, and for a module for the group ring.

#### Scott Morrison (Apr 14 2020 at 00:51):

You really need both points of view, and the ability to move between them.

#### Scott Morrison (Apr 14 2020 at 01:57):

I started proving this equivalence in my GroupModule_2 (rather experimental!) branch: https://github.com/leanprover-community/mathlib/blob/519a49d74154cee3d23dc45978a4a0e9e5274f37/src/group_theory/Rep.lean#L118

#### Patrick Stevens (Apr 14 2020 at 06:34):

Floris van Doorn said:

I'm planning to do some representation theory with Michael R Douglas. Do you think that is helpful, or are we then stepping on someone's toes? (Scott Morrison and Patrick Stevens might be working on the same or similar stuff)?

I am certainly not devoting that much effort to it - I'm a complete Lean noob and can't really spare the time to become good at the moment!

#### Kevin Buzzard (Apr 14 2020 at 14:33):

@Floris van Doorn I think this would be a good time to experiment with the github projects feature. There is a clear path with the basic theory: (1) definition of a representation of a group on an R-module (2) Maschke's theorem (G finite, order invertible in R) (3) Uniqueness of decomposition into irreducible factors (R a field, V fin dim), Schur's Lemma etc (4) [from now on G is finite of order invertible in the alg closed field k and V is fin dim] character of a representation (5) orthonormality of irred chars, and the fact that a rep is determined by its character (6) characters are a basis for the class functions (7) induction and restriction, Frobenius reciprocity.

I think we should use projects more. People come along and say "I am an undergrad mathematician, this all looks interesting, what can I do?" and if we can show them 5 undergraduate-level projects they might find a place to drop in.

#### Kevin Buzzard (Apr 14 2020 at 14:35):

Representation theory is one of these areas where every few months someone pops up and asks if it's done, and with a project we can indicate its current state.

#### orlando (Apr 14 2020 at 15:20):

@Kevin Buzzard : a little maths question : perhaps we can take $R[\text{Card}(G)^{-1}] [X ] / \langle \Phi_{\text{Card}(G)} (X) \rangle$ as " algebraic closed field " , with $\Phi$ the cyclotomic polynomial, :innocent:

Maybe :-)

#### Kevin Buzzard (Apr 14 2020 at 15:20):

But maybe you can only prove that after you have set up the theory? :-/

#### Floris van Doorn (Apr 14 2020 at 23:46):

That is a nice overview Kevin. It has been too long since I studied representation theory myself to remember the order to build up the theory, but I made a project by putting everything you said on a card.

#### Ashwin Iyengar (Apr 16 2020 at 01:08):

Hi @Floris van Doorn ! I'd like to contribute to this if it's convenient: it seems like someone's already started defining a representation but happy to do Maschke's theorem, or character theory/class functions etc, so should I wait until the file with the definition has been uploaded to start writing code?

#### Ashwin Iyengar (Apr 16 2020 at 01:14):

Ashwin Iyengar said:

Hi Floris van Doorn ! I'd like to contribute to this if it's convenient: it seems like someone's already started defining a representation but happy to do Maschke's theorem, or character theory/class functions etc, so should I wait until the file with the definition has been uploaded to start writing code?

On the other hand, if I'm treading on your toes let me know and I'll find something else to work on!

#### Kevin Buzzard (Apr 16 2020 at 01:16):

Ashvni wants to start working on local fields :-)

#### Floris van Doorn (Apr 16 2020 at 06:19):

Hi @Ashwin Iyengar: yes, you can join. I made a very small start here: https://github.com/fpvandoorn/group-representations
What is your Github username, then I can give you write access.

#### Johan Commelin (Apr 16 2020 at 07:21):

It seems that there are 4 interesting definitions:

1. G →* general_linear_group R M
2. group_module (G : Type*) [group G] (M : Type*) [add_comm_group M] extends has_scalar G M :=
3. linear_group_module like above, but with modules over R
4. module (monoid_algebra R G) M

Approaches (1), (3), and (4) lead to equivalent categories, and (2) is the specialization R = int.
The benefit of (3) is that it gives nice notation. It is so to speak the least bundled version.

#### David Wärn (Apr 16 2020 at 08:01):

Shouldn't (4) give the same notation as (3) if you define something like this?

instance [module (monoid_algebra R G) M] : module R M
instance [module (monoid_algebra R G) M] : has_scalar G M


#### Johan Commelin (Apr 16 2020 at 08:05):

Yes, I think that could work.

#### Johan Commelin (Apr 16 2020 at 08:06):

Ooh, maybe not... because R does not occur in has_scalar G M. So it will apply "too often".

#### Ashwin Iyengar (Apr 16 2020 at 08:51):

Great @Floris van Doorn my github name is ashwiniyengar

#### Scott Morrison (Apr 16 2020 at 10:04):

Oh, I've also got something. I just made a PR as #2431 to make it public.

#### Scott Morrison (Apr 16 2020 at 10:04):

I went the route of extending distrib_mul_action, so it gives the • notation (but may suffer from the problem Johan mentions; so far I haven't seen it).

#### Scott Morrison (Apr 16 2020 at 10:05):

My PR proves the equivalence between

1. representation k G M
2. G →* (M →ₗ[k] M)
3. module (monoid_algebra k G) M

#### Scott Morrison (Apr 16 2020 at 10:05):

but is stacked on top of #2366 and #2417, neither of which compile at the moment ... :-)

#### Scott Morrison (Apr 16 2020 at 10:05):

(I think it's minor for both.)

#### Scott Morrison (Apr 16 2020 at 10:11):

(hopefully all three compile now)

#### Johan Commelin (Apr 16 2020 at 10:20):

Yes, I'm afraid we tried enabling the \bu notation before with little representation theory projects, but ran into trouble...

#### Floris van Doorn (Apr 16 2020 at 17:22):

David Wärn said:

Shouldn't (4) give the same notation as (3) if you define something like this?

instance [module (monoid_algebra R G) M] : module R M
instance [module (monoid_algebra R G) M] : has_scalar G M


These two instances are likely causing looping behavior. For the second one, whenever Lean needs to find any has_scalar A B instance, is now has to look for instances module (monoid_algebra ?M A) B, which might cause looping because of the metavariable.

Option (1) and (3) both seem good. The question is really which notation we want to use: ρ g x or g • x.
The latter notation is nicer, but also more ambiguous. I think it makes it hard to state results about two representations of the same group in the same vector space. I think those results occur quite frequently in representation theory (right?). Or maybe that's the wrong way of stating it in Lean; maybe the Lean way is to have the representations on different (but isomorphic?) vector spaces.

#### Kevin Buzzard (Apr 16 2020 at 17:37):

I guess that for any continuous group homomorphism $G\to\mathbb{C}^\times$ one gets a character which traditionally would commonly be realised as a action of $G$ on the vector space $\mathbb{C}$.

#### Kevin Buzzard (Apr 16 2020 at 17:39):

This whole business is going to be pretty interesting to formalise actually. One would ideally get as far as the characters of a finite group (over an alg closed field of char 0, say) as being a basis for the class functions, but I always felt like I was treating a character as "the same as" a representation, whereas given a character one is going to have to make some kind of choice for the representation when actually proving things about it, and perhaps if $\chi(1)=n$ the natural choice for $V$ is $k^n$? Although then there's no natural choice for the action $\ldots$

#### David Wärn (Apr 16 2020 at 18:33):

Characters are the decategorification of representations!

#### Patrick Massot (Apr 16 2020 at 19:13):

My standard contribution: Feit-Thompson uses representation theory so, if you are serious about formalizing it, you should at least have a look at mathcomp. Or ask @Assia Mahboubi and @Cyril Cohen

#### orlando (Apr 18 2020 at 01:56):

Hello, i do i little exercice with the file of here of @Floris van Doorn ! I just try to define a sub representation when a subspace is $\rho$-stable ! here

#### Scott Morrison (Apr 18 2020 at 03:09):

Hi @orlando, it's a bit hard to comment on the whole thing at once, as many things are going on in your file.

#### Scott Morrison (Apr 18 2020 at 03:10):

I've also been thinking about a different approach to defining representations (and in a branch I have the outline of a proof of Maschke's theorem).

#### Scott Morrison (Apr 18 2020 at 03:10):

It's in the PR #2431, under the branch name representation.

#### Scott Morrison (Apr 18 2020 at 03:11):

Your file has a lot of preparatory lemmas, whose purpose I'm pretty unclear on.

#### orlando (Apr 18 2020 at 09:03):

Hi Scott.

I try to explain at the outset the definition refers to groups of units. And I would do things by looking at linear endomophisms. If i understand, you take endomorphism definition !

I use the notation \ oo for composition (and I realized that there is a notion * so \ oo is not useful I think). The preparatory lemma a just some formula to simplify a little. (and for fun :grinning_face_with_smiling_eyes:).

ohh ,it's cool if you have outline of Maschke Theorem !

Ps : I just make :

def new_groupe_representation :
( group_representation G R M)  →  G →* (M →ₗ[R] M) := λ ρ, ⟨has_coe_to ρ, rmap_one ρ,rmap_mul ρ⟩


So i thinck that glue the two definitions. But perhaps there is a quicker way to do., using  general_linear_equiv : general_linear_group R M ≃* (M ≃ₗ[R] M)  in the file linear algebra basic :joy:

#### orlando (Apr 23 2020 at 08:43):

Hello @Scott Morrison I redo all my stuff.

I have problem with conversion ↑ ⇑ erw  etc i think it's more clear but not perfect and it's a good project for me to learn ! I have show just the Schur lemma from Serre book and construct some stuff. Next step use character hum hum !

If you are some comment for a better programming ?
here

#### Kevin Buzzard (Apr 23 2020 at 10:23):

The computer scientists will tell you to change [group G] to [monoid G] in the definition, because you do not use inverses :-)

#### Kevin Buzzard (Apr 23 2020 at 10:35):

@orlando did you see the representation theory project?

#### orlando (Apr 23 2020 at 10:52):

Yes Kevin, i start with the first file of @Floris van Doorn but i change the definition because (conversion big problem) !

I'm happy cause i understand i little more rfl  :innocent:

#### Kevin Buzzard (Apr 23 2020 at 10:54):

With this project, I feel like the hardest part is choosing the correct initial definition.

#### Mario Carneiro (Apr 23 2020 at 10:57):

ooh, I didn't know we have a kanban board (or whatever the kids call it these days)

#### orlando (May 14 2020 at 09:43):

@Scott Morrison @Floris van Doorn

I don't know if you continue about representation. But a question : do you have a version of the decomposition of representation in irreducible representation ? I have the orthogonality of character (i have just a little problem with a formula  trace rho g \-1 = complex.conj trace rho g  i don't know if it's decisive for the moment).

I think just a little about the decomposition for the moment ! So if you have a version tell me :slight_smile:

#### Kevin Buzzard (May 14 2020 at 12:25):

Wow the proof I know of that trace fact uses a lot

#### Kevin Buzzard (May 14 2020 at 12:26):

g is in a finite group so the order is finite (else it's false)

#### Kevin Buzzard (May 14 2020 at 12:26):

There is something called eigenvalues of a matrix

#### Kevin Buzzard (May 14 2020 at 12:26):

Each eigenvalue is a root of the min poly

#### Kevin Buzzard (May 14 2020 at 12:27):

Each eigenvalue is a root of unity

Wait

#### Kevin Buzzard (May 14 2020 at 12:27):

Perhaps what I'm missing is the theory of unitary matrices

#### Kevin Buzzard (May 14 2020 at 12:28):

Trace of inverse = trace of conjugate = conjugate of trace by transport

#### Kevin Buzzard (May 14 2020 at 12:29):

So maybe prove that the image is in the unitary matrices wrt some R-structure made using the averaged inner form trick?

#### orlando (May 14 2020 at 12:38):

hum the problem is what is easy to make in lean  for the moment ! Perhaps the root of unity it's difficult for the moment, ??? Perhaps with unitary representation !

Yes it's the average trick ! All the basic theory is the average trick :grinning_face_with_smiling_eyes:

#### Johan Commelin (May 14 2020 at 14:32):

@orlando You really need to start writing PRs :rofl:

#### orlando (May 14 2020 at 16:42):

@Johan Commelin I'm really noob with git hub, i just understand  git add , git commit, git push  :sweat_smile: so first i finish with  math / lean  and next i try too understand  PR's story  :grinning:

#### Johan Commelin (May 14 2020 at 16:53):

Those three commands are enough (-;

#### Johan Commelin (May 14 2020 at 16:54):

Ooh, maybe add git checkout for switching branches.

#### Johan Commelin (May 14 2020 at 16:54):

I really fear that otherwise you'll end up with 5000 lines of code, and it will just sit in some repo, and never get PR'd

#### Floris van Doorn (May 14 2020 at 19:43):

@orlando We're definitely not there yet. We're still working on Maschke's Theorem, but we're making good progress.

#### Floris van Doorn (May 14 2020 at 19:51):

@Kevin Buzzard Can you elaborate a bit on what you mean by Maschke's theorem for an R-module (instead of a vector space)? Given a submodule of a module, there doesn't necessarily even have to exist a complementary submodule, so if Maschke's theorem guarantees an invariant complementary submodule, then it is false. I think we can prove that if a submodule has a complementary submodule, it also has an invariant one.

theorem maschke2 [fintype G] (ρ : group_representation G R M) (N N' : submodule R M)
(h : complementary N N') (hN : invariant_subspace ρ N) (hG : is_unit (fintype.card G : R)) :
∃ N', invariant_subspace ρ N' ∧ complementary N N'


https://github.com/fpvandoorn/group-representations/blob/da8dfe6c436ec15abeefb73040e31f19d197e11b/src/group_theory/representation/basic.lean#L501
Is this the statement you had in mind?

Also, is there any source that does representation theory in modules (not in vector spaces)? We're kind of trying to figure out what holds for R-modules as we go, and sometimes have to reformulate results to only hold for vector spaces in the middle of a proof.

#### Kevin Buzzard (May 14 2020 at 20:05):

Yes, it seems to me that you're right, I think the theorems are the following:
1) If G is finite and 1/|G| is in R, and if there exists a complementary submodule (possibly not G-invariant) to your G-invariant one, then there exists a G-invariant complementary submodule.
2) If R is a field then there always exists a complementary submodule

#### Kevin Buzzard (May 14 2020 at 20:06):

The FLT proof contains a whole bunch of representation theory to arbitrary rings, but it doesn't need anything like Maschke, it needs representability theorems. Here is an example of a theorem that it uses (and I'm sure @Johan Commelin knows about this stuff too):

#### Kevin Buzzard (May 14 2020 at 20:07):

(oh, dinner time)

#### Kevin Buzzard (May 14 2020 at 20:07):

(universal deformation rings)

#### Johan Commelin (May 14 2020 at 20:08):

Kevin Buzzard said:

(oh, dinner time)

Yup, I know that one.

#### orlando (May 14 2020 at 20:10):

@Floris van Doorn :

I'm ok with you're theorem you have to put the hypothesis  h  for module. But perhaps in a first time we have to use field, for ring i think there is very complicated thing !

#### Floris van Doorn (May 14 2020 at 21:23):

Ah good, we have already proven (2), using Zorn's Lemma.
Then we're going to finish this version of Maschke's Theorem.

#### Reid Barton (May 14 2020 at 21:38):

Hmm, I'm surprised that I couldn't find any kind of representation theory in Bourbaki with my google searches.

#### orlando (May 14 2020 at 21:55):

@Reid Barton i think it's in this volume :here

#### Reid Barton (May 14 2020 at 21:57):

oh, yes! I only found Algebra I (chapters 1-3) and Algebra II (chapters 4-7)

#### orlando (May 14 2020 at 21:57):

i don't have the book :frown:

#### orlando (May 14 2020 at 21:58):

But there is 400 page before :  representation lineaire sur les nombres complexes  i have to learn and read i little :grinning_face_with_smiling_eyes:

#### Reid Barton (May 14 2020 at 22:04):

I see, so this entire book of nearly 500 pages is "chapter 8"

#### Reid Barton (May 14 2020 at 22:14):

I found the page on Maschke's theorem on Google Books but I don't know what the standing assumptions on "$K$" are.

#### Reid Barton (May 14 2020 at 22:16):

I found one place that says "if $K$ is a field [division algebra]" and others "a commutative field" though, so I assume the standing assumption is that $K$ is just a ring...

#### orlando (May 14 2020 at 22:29):

Oh thx i don't use google book, it's good !

#### Scott Morrison (May 15 2020 at 01:28):

I will try to get back to this soon, but I have a proof of Maschke's theorem in Maschke.

#### Johan Commelin (May 15 2020 at 03:20):

@Floris van Doorn :up:

#### Scott Morrison (May 20 2020 at 15:11):

I made #2762, with my proof of Maschke's theorem. It's still a bit messy, but all the sorries are gone!

#### Scott Morrison (May 20 2020 at 15:13):

The thing that it is missing still is the fact that any k-linear inclusion has a retraction, but this is hopefully done somewhere in the existing linear algebra library, and I can plug it in. For now the final statement includes an extra hypothesis for this fact.

#### Johan Commelin (May 20 2020 at 16:07):

I think that fact isn't done yet, but it should be trivial once Yury's PRs on complementary submodules are merged.

#### Johan Commelin (May 20 2020 at 16:07):

Great work with Maschke's theorem. It's one of those things that every self-respecting library ought to have (-;

#### Yury G. Kudryashov (May 20 2020 at 16:08):

Scott doesn't need continuous version, and projection PR is already merged.

#### Yury G. Kudryashov (May 20 2020 at 16:09):

What exactly do you need?

#### Yury G. Kudryashov (May 20 2020 at 16:10):

E.g., we have exists_left_inverse_of_injective and exists_right_inverse_of_surjective in linear_algebra/basis.lean.

#### orlando (May 21 2020 at 08:31):

Hello, That good @Scott Morrison , i have also a version of Maschke theorem.

But for me the big step is really to make the application over $\mathbb{C}$ !

For example, the decomposition of a representation in irreducible representation.

I think the decomposition in irrducible part is ok for field (not algebraically closed).

#### Patrick Massot (May 21 2020 at 10:42):

Could we move this thread to the math stream?

#### Notification Bot (May 21 2020 at 16:18):

This topic was moved by Mario Carneiro to #maths > Representation Theory

Last updated: May 14 2021 at 23:14 UTC