Schur lemma over algebraically closed fields

Stream: new members

[Antoine Labelle]

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 $\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?

[Johan Commelin]

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

[Johan Commelin]

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

[Antoine Labelle]

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

[Kevin Buzzard]

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.

[Antoine Labelle]

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

[Kevin Buzzard]

What is the density theorem?

[Antoine Labelle]

Surjectivity of $\rho : A \to End_k(V)$ for an irreducible representation $V$ of a $k$-algebra $A$

[Antoine Labelle]

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?

[Johan Commelin]

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

[Johan Commelin]

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"

[Johan Commelin]

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.

[Johan Commelin]

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.

[Antoine Labelle]

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?

[Eric Wieser]

You could use a sigma type instead of the product type

[Eric Wieser]

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

[Reid Barton]

Probably needs a by exactI as well

[Frédéric Dupuis]

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.

[Antoine Labelle]

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

[Antoine Labelle]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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".

[Reid Barton]

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

[Antoine Labelle]

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.

[Reid Barton]

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

[Reid Barton]

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

[Antoine Labelle]

Σ' works, thanks!