Zulip Chat Archive

Stream: new members

Topic: Representation Theory


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Oct 17 2019 at 01:59):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:04):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jineon Baek (Oct 17 2019 at 04:29):

@Seewoo Lee

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 17 2019 at 05:50):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 17 2019 at 08:04):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip Mario Carneiro (Mar 15 2020 at 09:29):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 09:30):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 10:20):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 10:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Stevens (Mar 15 2020 at 10:24):

OK, that makes sense - thanks

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:45):

Have a look at #check linear_representation

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:46):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:49):

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

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:49):

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

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:50):

Your p obviously has dimension n by definition.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 10:53):

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

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:53):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 10:53):

linear_representation has too many implicit variables

view this post on Zulip 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

view this post on Zulip Patrick Stevens (Mar 15 2020 at 10:54):

Thanks

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 10:54):

or linear_representation F G n if you want that version

view this post on Zulip Patrick Massot (Mar 15 2020 at 10:55):

That's why I wrote a bunch of #check

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:00):

OK I'll take a look at your version.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:02):

Which version of Lean are you using?

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:05):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:11):

I think it should be a monoid rather than a group

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:11):

it also looks suspiciously like a group action

view this post on Zulip Patrick Stevens (Mar 15 2020 at 12:11):

It is a group action

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:11):

A group module is a group action by module homs

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:11):

Mario is pointing out that it could extend group actions

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:12):

(then you get a bunch of theorems for free)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:14):

Yes absolutely

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:15):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:16):

sure, any of those sound good to me

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:16):

they are already very compact

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:16):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:16):

It's less clear to me

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:16):

Isn't this usually how the mathematicians do it?

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:16):

I would prefer clarity

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:17):

I feel like we've swapped sides of this argument

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:17):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:18):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:19):

My understanding here is that there is no perfect solution.

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:19):

That's certainly going to be the case

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:19):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:21):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:21):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:21):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:21):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:21):

I'm not going back to assembly language now

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:22):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:24):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:24):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:25):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:26):

it's not invisible

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:26):

I wish it was

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:27):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:27):

Sure -- I just meant "invisible to mathematicians"

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:27):

and we have a rather liberal notion of =

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Patrick Stevens (Mar 15 2020 at 12:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:35):

Before the sorry Lean is failing to elaborate the term.

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:35):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Stevens (Mar 15 2020 at 12:40):

Yep, I see what you mean

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:40):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:43):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:43):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:44):

Binders are always distinguishable because they come after binding notation tokens

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:44):

but implicit function args are just in regular expression position

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:46):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:46):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:46):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:46):

yes

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:46):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:47):

I think so

view this post on Zulip 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 _ _ _ _

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:47):

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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:47):

whereas I wanted to write foo {R = F}

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:48):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:49):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:50):

when it works in LaTeX

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:50):

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

view this post on Zulip 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 ;-) )

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:52):

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

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:52):

then again, typing that may become annoying

view this post on Zulip Mario Carneiro (Mar 15 2020 at 12:53):

syntax is hard

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:53):

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

view this post on Zulip Patrick Stevens (Mar 15 2020 at 12:53):

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

view this post on Zulip 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)? :-)

view this post on Zulip Kevin Buzzard (Mar 15 2020 at 12:54):

unfortuately it won't work for 3.4.2 ;-)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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
  }

view this post on Zulip Daniel Keys (Mar 15 2020 at 18:51):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:54):

Hmm... such examples are certain there.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:55):

But #eval cannot compute a dimension for you

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:55):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:56):

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

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:56):

This is very unfortunate.

view this post on Zulip Patrick Stevens (Mar 21 2020 at 09:56):

Oh, that's very upsetting

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:56):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:57):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 21 2020 at 09:59):

Well, mostly yes.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 21 2020 at 10:00):

So all the generalities are developed using multiplicative notation.

view this post on Zulip Johan Commelin (Mar 21 2020 at 10:00):

But stuff like modules and representations assumes additive groups

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 21 2020 at 10:07):

No, because of the notation.

view this post on Zulip Johan Commelin (Mar 21 2020 at 10:07):

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

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 21 2020 at 10:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Stevens (Mar 21 2020 at 13:52):

There is an awful lot to unlearn here :P

view this post on Zulip Johan Commelin (Mar 21 2020 at 13:53):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:34):

well, Lean's prop is forgetful

view this post on Zulip Mario Carneiro (Mar 21 2020 at 14:34):

that would be proof irrelevance

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:34):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 14:34):

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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 14:34):

we can say that Prop is a proof irrelevant universe

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 21 2020 at 14:39):

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

view this post on Zulip Mario Carneiro (Mar 21 2020 at 14:40):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 18:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 14 2020 at 00:51):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip orlando (Apr 14 2020 at 15:20):

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 15:20):

Maybe :-)

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 15:20):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 01:16):

Ashvni wants to start working on local fields :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 16 2020 at 08:05):

Yes, I think that could work.

view this post on Zulip 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".

view this post on Zulip Ashwin Iyengar (Apr 16 2020 at 08:51):

Great @Floris van Doorn my github name is ashwiniyengar

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 16 2020 at 10:05):

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

view this post on Zulip Scott Morrison (Apr 16 2020 at 10:05):

(I think it's minor for both.)

view this post on Zulip Scott Morrison (Apr 16 2020 at 10:11):

(hopefully all three compile now)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 17:37):

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

view this post on Zulip 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 χ(1)=n\chi(1)=n the natural choice for VV is knk^n? Although then there's no natural choice for the action \ldots

view this post on Zulip David Wärn (Apr 16 2020 at 18:33):

Characters are the decategorification of representations!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Apr 18 2020 at 03:10):

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

view this post on Zulip Scott Morrison (Apr 18 2020 at 03:11):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 10:35):

@orlando did you see the representation theory project?

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 10:54):

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

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:25):

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

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:26):

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

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:26):

There is something called eigenvalues of a matrix

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:26):

Each eigenvalue is a root of the min poly

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:27):

Each eigenvalue is a root of unity

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:27):

Wait

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:27):

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

view this post on Zulip Kevin Buzzard (May 14 2020 at 12:28):

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

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip Johan Commelin (May 14 2020 at 14:32):

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

view this post on Zulip 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:

view this post on Zulip Johan Commelin (May 14 2020 at 16:53):

Those three commands are enough (-;

view this post on Zulip Johan Commelin (May 14 2020 at 16:54):

Ooh, maybe add git checkout for switching branches.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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):

view this post on Zulip Kevin Buzzard (May 14 2020 at 20:07):

(oh, dinner time)

view this post on Zulip Kevin Buzzard (May 14 2020 at 20:07):

(universal deformation rings)

view this post on Zulip Johan Commelin (May 14 2020 at 20:08):

Kevin Buzzard said:

(oh, dinner time)

Yup, I know that one.

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip orlando (May 14 2020 at 21:55):

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

view this post on Zulip Reid Barton (May 14 2020 at 21:57):

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

view this post on Zulip orlando (May 14 2020 at 21:57):

i don't have the book :frown:

view this post on Zulip 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:

view this post on Zulip Reid Barton (May 14 2020 at 22:04):

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

view this post on Zulip 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 "KK" are.

view this post on Zulip Reid Barton (May 14 2020 at 22:16):

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

view this post on Zulip orlando (May 14 2020 at 22:29):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 15 2020 at 03:20):

@Floris van Doorn :up:

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 (-;

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 16:08):

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

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 16:09):

What exactly do you need?

view this post on Zulip 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.

view this post on Zulip 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 C\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).

view this post on Zulip Patrick Massot (May 21 2020 at 10:42):

Could we move this thread to the math stream?

view this post on Zulip 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