Representation Theory

Stream: new members

[Jineon Baek]

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]

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

[Jineon Baek]

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]

@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]

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]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Jineon Baek]

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]

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]

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]

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]

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

[Jineon Baek]

@Seewoo Lee

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Tim Daly]

@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]

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]

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]

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]

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

[Mario Carneiro]

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

[Patrick Stevens]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Patrick Stevens]

OK, that makes sense - thanks

[Patrick Stevens]

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]

Have a look at #check linear_representation

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

Your p obviously has dimension n by definition.

[Patrick Stevens]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

linear_representation has too many implicit variables

[Patrick Stevens]

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

[Patrick Stevens]

Thanks

[Mario Carneiro]

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

[Mario Carneiro]

or linear_representation F G n if you want that version

[Patrick Massot]

That's why I wrote a bunch of #check

[Mario Carneiro]

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]

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]

@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]

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

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

[Kevin Buzzard]

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]

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]

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]

OK I'll take a look at your version.

[Kevin Buzzard]

Which version of Lean are you using?

[Kevin Buzzard]

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

[Patrick Stevens]

Kevin Buzzard said:

Which version of Lean are you using?

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

[Kevin Buzzard]

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]

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]

@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]

I think it should be a monoid rather than a group

[Mario Carneiro]

it also looks suspiciously like a group action

[Patrick Stevens]

It is a group action

[Kevin Buzzard]

A group module is a group action by module homs

[Kevin Buzzard]

Mario is pointing out that it could extend group actions

[Kevin Buzzard]

(then you get a bunch of theorems for free)

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Yes absolutely

[Mario Carneiro]

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

[Kevin Buzzard]

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]

sure, any of those sound good to me

[Mario Carneiro]

they are already very compact

[Kevin Buzzard]

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

[Kevin Buzzard]

It's less clear to me

[Mario Carneiro]

Isn't this usually how the mathematicians do it?

[Kevin Buzzard]

I would prefer clarity

[Mario Carneiro]

I feel like we've swapped sides of this argument

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

My understanding here is that there is no perfect solution.

[Mario Carneiro]

That's certainly going to be the case

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I'm not going back to assembly language now

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

@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]

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]

it's not invisible

[Mario Carneiro]

I wish it was

[Mario Carneiro]

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

[Kevin Buzzard]

Sure -- I just meant "invisible to mathematicians"

[Kevin Buzzard]

and we have a rather liberal notion of =

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

[Patrick Stevens]

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]

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]

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

[Patrick Stevens]

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

[Kevin Buzzard]

Before the sorry Lean is failing to elaborate the term.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

Yep, I see what you mean

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Binders are always distinguishable because they come after binding notation tokens

[Mario Carneiro]

but implicit function args are just in regular expression position

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

I think so

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

whereas I wanted to write foo {R = F}

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

when it works in LaTeX

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

then again, typing that may become annoying

[Mario Carneiro]

syntax is hard

[Kevin Buzzard]

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

[Patrick Stevens]

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

[Kevin Buzzard]

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]

unfortuately it won't work for 3.4.2 ;-)

[Kevin Buzzard]

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]

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

[Patrick Stevens]

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]

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

[Patrick Stevens]

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]

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

[Patrick Stevens]

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]

Hmm... such examples are certain there.

[Johan Commelin]

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

[Johan Commelin]

But #eval cannot compute a dimension for you

[Johan Commelin]

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

[Patrick Stevens]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

This is very unfortunate.

[Patrick Stevens]

Oh, that's very upsetting

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Stevens]

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

[Johan Commelin]

Well, mostly yes.

[Johan Commelin]

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

[Johan Commelin]

So all the generalities are developed using multiplicative notation.

[Johan Commelin]

But stuff like modules and representations assumes additive groups

[Patrick Stevens]

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

[Johan Commelin]

No, because of the notation.

[Johan Commelin]

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]

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

[Johan Commelin]

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

@[to_additive]
theorem my_multiplicative_thm ...

[Johan Commelin]

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]

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

[Patrick Stevens]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

There is an awful lot to unlearn here :P

[Johan Commelin]

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

[Kevin Buzzard]

@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]

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

[Patrick Massot]

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]

well, Lean's prop is forgetful

[Mario Carneiro]

that would be proof irrelevance

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

we can say that Prop is a proof irrelevant universe

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Alex J. Best]

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]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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]

@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]

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]

@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:

[Kevin Buzzard]

Maybe :-)

[Kevin Buzzard]

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

[Floris van Doorn]

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]

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]

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]

Ashvni wants to start working on local fields :-)

[Floris van Doorn]

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]

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]

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]

Yes, I think that could work.

[Johan Commelin]

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

[Ashwin Iyengar]

Great @Floris van Doorn my github name is ashwiniyengar

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

(I think it's minor for both.)

[Scott Morrison]

(hopefully all three compile now)

[Johan Commelin]

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

[Floris van Doorn]

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]

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]

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]

Characters are the decategorification of representations!

[Patrick Massot]

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]

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]

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]

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]

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

[Scott Morrison]

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

[orlando]

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]

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]

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

[Kevin Buzzard]

@orlando did you see the representation theory project?

[orlando]

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]

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

[Mario Carneiro]

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

[orlando]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

There is something called eigenvalues of a matrix

[Kevin Buzzard]

Each eigenvalue is a root of the min poly

[Kevin Buzzard]

Each eigenvalue is a root of unity

[Kevin Buzzard]

Wait

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[orlando]

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]

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

[orlando]

@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]

Those three commands are enough (-;

[Johan Commelin]

Ooh, maybe add git checkout for switching branches.

[Johan Commelin]

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]

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

[Floris van Doorn]

@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]

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]

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]

(oh, dinner time)

[Kevin Buzzard]

(universal deformation rings)

[Johan Commelin]

Kevin Buzzard said:

(oh, dinner time)

Yup, I know that one.

[orlando]

@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]

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]

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

[orlando]

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

[Reid Barton]

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

[orlando]

i don't have the book :frown:

[orlando]

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]

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

[Reid Barton]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

@Floris van Doorn :up:

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

What exactly do you need?

[Yury G. Kudryashov]

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

[orlando]

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]

Could we move this thread to the math stream?

[Notification Bot]

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