Zulip Chat Archive

Stream: new members

Topic: Schur lemma over algebraically closed fields


view this post on Zulip Antoine Labelle (Nov 30 2020 at 16:49):

Hi!
I would like to try starting to contribute to mathlib and I thought about doing a bit of representation theory. I saw that we have Schur's lemma proved in the generality of preadditive categories with kernels but not yet the corollary for algebraically closed fields that dim(Hom(X,Y))1\text{dim}(\text{Hom}(X,Y))\le 1. I thought that might be a good place to start but, in order to do it in the same level of generality than the Schur's lemma we have, I would need enriched categories over vectors spaces, which don't seem to be in mathlib.
I am therefore unsure where to start. Should I prove Schur's lemma only for representations of groups/algebras or should I try defining enriched categories? Also does my plan sounds reasonable for a first contribution?

view this post on Zulip Johan Commelin (Nov 30 2020 at 17:15):

@Antoine Labelle Welcome!
@Scott Morrison Has been working on getting enriched cats in mathlib. I'm afraid that it's quite tricky, and not really suited for a first project.
So it might be better to just prove it in the non-categorical fashion first.

view this post on Zulip Johan Commelin (Nov 30 2020 at 17:16):

Or choose a different topic (-; There's lots of low-hanging fruit out there.

view this post on Zulip Antoine Labelle (Nov 30 2020 at 17:55):

@Johan Commelin Thanks for your answer. Do you think it would still be useful to do it in the non-categorical fashion or is it a loss of time given it will be done in greater generality later? Also I would be happy to have some suggestions of other easier projects that would be suited for a beginner.

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 18:06):

My instinct is that if one wants e.g. representation theory of finite or compact groups there is plenty to do. Orthonormality of characters for a finite group would be a great thing to aim for.

view this post on Zulip Antoine Labelle (Dec 01 2020 at 01:35):

Thanks, for now I think I might try to aim at the density theorem, does that seems doable?

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 01:37):

What is the density theorem?

view this post on Zulip Antoine Labelle (Dec 01 2020 at 01:40):

Surjectivity of ρ:AEndk(V)\rho : A \to End_k(V) for an irreducible representation VV of a kk-algebra AA

view this post on Zulip Antoine Labelle (Dec 01 2020 at 02:02):

Also, I saw that there is a categorical definition a simple object but I found no specific definition of a simple module. Thus I suppose I have to use the categorical definition but I am unsure how to do that. Is there somewhere a definition of the category of modules over a ring?

view this post on Zulip Johan Commelin (Dec 01 2020 at 04:48):

We have the category of modules over a ring. See the directory src/algebra/category/ for "basic" categories in algebra.

view this post on Zulip Johan Commelin (Dec 01 2020 at 04:49):

But the first thing you might want to do is prove that a rep is a "categorically simple object" iff "statement in terms of subrepresentations"

view this post on Zulip Johan Commelin (Dec 01 2020 at 04:50):

There's also the whole business of viewing a rep as a map from G to GL(V), or as a module over k[G]. And we haven't really fleshed out this dictionary yet. In maths its a 1-liner. But for formalisation I'm afraid we'll want some explicit trivialities to make life easier.

view this post on Zulip Johan Commelin (Dec 01 2020 at 04:51):

This is also "very low hanging fruit". The problem with formalisation is: if you try to take shortcuts, and ignore the "very low hanging fruit", then suddenly the "low hanging fruit" will start to feel hard and out of reach.

view this post on Zulip Antoine Labelle (Dec 01 2020 at 19:00):

import tactic
import algebra.algebra.basic
import algebra.module.linear_map

variables {R : Type} [comm_semiring R] {A : Type} [semiring A] [algebra R A]

def module_to_map_to_endomophism_algebra
  (V : Type) [add_comm_monoid V] [semimodule R V] [semimodule A V] [is_scalar_tower R A V] :
  A →ₐ[R] (V →ₗ[R] V) :=
{ to_fun := λ a, {to_fun := () a,
                  map_add' := smul_add a,
                  map_smul' := smul_comm a},
  map_one' := by {ext, simp},
  map_mul' := by {intros a b, ext, simp, exact mul_smul _ _ _},
  map_zero' := by {ext, simp},
  map_add' := by {intros a b, ext, simp, exact add_smul _ _ _},
  commutes' := by {intro r, ext, simp} }

def map_to_endomorphism_algebra_to_module
  (V : Type) [add_comm_monoid V] [semimodule R V] (ρ : A →ₐ[R] (V →ₗ[R] V))  :
  (semimodule A V) × is_scalar_tower R A V :=
⟨{ smul := (λ a, (ρ.to_fun a)),
   one_smul := by {intro v, simp, rw ρ.map_one', exact rfl},
   mul_smul := by {intros a b v, simp, rw ρ.map_mul' a b, exact rfl},
   smul_add := by {simp},
   smul_zero := by {simp},
   add_smul := by {intros a b v, simp, rw ρ.map_add', exact rfl},
   zero_smul := by {intro v, simp, rw ρ.map_zero', exact rfl} },
  sorry

I began to work a bit on this and got a question. I want to define the A-module structure on V given a map (ρ : A →ₐ[R] (V →ₗ[R] V)). For this I need to output instances of both semimodule A V and is_scalar_tower R A V , but if I try to do it like this is_scalar_tower give me an error "failed to synthesize type class instance", I guess because is_scalar_tower does not "know" yet that we have an instance of semimodule A V. Is there a simple way to get around this problem?

view this post on Zulip Eric Wieser (Dec 01 2020 at 20:15):

You could use a sigma type instead of the product type

view this post on Zulip Eric Wieser (Dec 01 2020 at 20:17):

Something like \sigma [semimodule A V], is_scalar_tower ...

view this post on Zulip Reid Barton (Dec 01 2020 at 20:24):

Probably needs a by exactI as well

view this post on Zulip Frédéric Dupuis (Dec 01 2020 at 20:27):

Would this sigma type trick actually be useful when using it afterwards? I was going to suggest splitting it into two: first define the semimodule A V, and then have a definition of is_scalar_tower R A V assuming [semimodule A V] together with a proof that the smul is the one you want.

view this post on Zulip Antoine Labelle (Dec 02 2020 at 00:13):

@Frédéric Dupuis I think it would make more sense to keep it in a single definition, since it will be simpler then to prove that the two functions I defined are inverses of each other.

view this post on Zulip Antoine Labelle (Dec 02 2020 at 01:40):

I tried Σ [semimodule A V], (is_scalar_tower R A V) but I get the following error

failed to synthesize type class instance for
R : Type,
_inst_1 : comm_semiring R,
A : Type,
_inst_2 : semiring A,
_inst_3 : algebra R A,
V : Type,
_inst_4 : add_comm_monoid V,
_inst_5 : semimodule R V,
ρ : A →ₐ[R] V →ₗ[R] V,
_inst_6 : semimodule A V
 has_scalar A V

Why doesn't lean use the semimodule A Vinstance? Is it why I need exactI? What would be the syntax with exactI?

view this post on Zulip Kevin Buzzard (Dec 02 2020 at 01:47):

Σ [semimodule A V], by exactI (is_scalar_tower R A V) maybe?

view this post on Zulip Kevin Buzzard (Dec 02 2020 at 01:48):

Lean's type class inference system (the system whose job it is to supply the [] inputs) doesn't look in the local context, it only looks at stuff which happens before the colon. by exactI means "throw everything in the local context at this point into the type class inference system".

view this post on Zulip Reid Barton (Dec 02 2020 at 01:57):

I think the []s in Σ [semimodule A V], ... are unlikely to do anything helpful

view this post on Zulip Antoine Labelle (Dec 02 2020 at 02:10):

Hum with Σ [semimodule A V], by exactI (is_scalar_tower R A V) I get this error

invalid type ascription, term has type
  Prop : Type
but is expected to have type
  Type ? : Type (?+1)
state:
R : Type,
_inst_1 : comm_semiring R,
A : Type,
_inst_2 : semiring A,
_inst_3 : algebra R A,
V : Type,
_inst_4 : add_comm_monoid V,
_inst_5 : semimodule R V,
ρ : A →ₐ[R] V →ₗ[R] V,
_inst_6 : semimodule A V
 Type ?

Also I think that the brackets are indeed important because I get another error if I remove them.

view this post on Zulip Reid Barton (Dec 02 2020 at 02:11):

oh, you'll need a variable name like Σ (I : semimodule A V), by exactI (is_scalar_tower R A V) then, I suppose

view this post on Zulip Reid Barton (Dec 02 2020 at 02:11):

Ah, is_scalar_tower is a Prop so you'll need Σ' or a subtype

view this post on Zulip Antoine Labelle (Dec 02 2020 at 02:20):

Σ' works, thanks!


Last updated: May 06 2021 at 21:09 UTC