# Zulip Chat Archive

## Stream: new members

### Topic: Schur lemma over algebraically closed fields

#### 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 $\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 (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.

#### Johan Commelin (Nov 30 2020 at 17:16):

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

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

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

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

#### Kevin Buzzard (Dec 01 2020 at 01:37):

What is the density theorem?

#### Antoine Labelle (Dec 01 2020 at 01:40):

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

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

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

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

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

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

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

#### Eric Wieser (Dec 01 2020 at 20:15):

You could use a sigma type instead of the product type

#### Eric Wieser (Dec 01 2020 at 20:17):

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

#### Reid Barton (Dec 01 2020 at 20:24):

Probably needs a `by exactI`

as well

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

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

#### 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 V`

instance? Is it why I need `exactI`

? What would be the syntax with `exactI`

?

#### Kevin Buzzard (Dec 02 2020 at 01:47):

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

maybe?

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

#### Reid Barton (Dec 02 2020 at 01:57):

I think the `[]`

s in `Σ [semimodule A V], ...`

are unlikely to do anything helpful

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

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

#### Reid Barton (Dec 02 2020 at 02:11):

Ah, `is_scalar_tower`

is a Prop so you'll need `Σ'`

or a `subtype`

#### Antoine Labelle (Dec 02 2020 at 02:20):

`Σ'`

works, thanks!

Last updated: May 06 2021 at 21:09 UTC