Schur's lemma

Stream: maths

[Pierre-Alexandre Bazin]

I'm wanting to formalise Schur's lemma (https://en.wikipedia.org/wiki/Schur%27s_lemma) in mathlib but I'm not sure at what level of generalisation I should do it.

1. Proving just the lemma about group representations

2. Proving the lemma that every non-zero morphism between simple modules is an isomorphism (and then view group representations as modules over the group ring)

3. Generalise even further by viewing it as a category theory lemma (that would encompass for example both the case of simple modules and the case of simple groups - I'm not 100% sure how to do it)

[Johan Commelin]

@Pierre-Alexandre Bazin I think (3) has been done.

[Johan Commelin]

But the specialization to (1) isn't completely trivial. One would need to show that the categorical assumptions apply.

[Johan Commelin]

Here's a dump:

$ rg Schur
docs/undergrad.yaml
70:    Schur's lemma: 'https://en.wikipedia.org/wiki/Schur%27s_lemma'
115:    orthogonality of irreducible characters: 'https://en.wikipedia.org/wiki/Schur_orthogonality_relations'

src/group_theory/schur_zassenhaus.lean
12:# The Schur-Zassenhaus Theorem
14:In this file we prove the Schur-Zassenhaus theorem.
18:- `exists_right_complement'_of_coprime` : The **Schur-Zassenhaus** theorem:
21:- `exists_left_complement'_of_coprime`  The **Schur-Zassenhaus** theorem:
183:/-! ## Proof of the Schur-Zassenhaus theorem
185:In this section, we prove the Schur-Zassenhaus theorem.
331:/-- **Schur-Zassenhaus** for normal subgroups:
339:/-- **Schur-Zassenhaus** for normal subgroups:
364:/-- **Schur-Zassenhaus** for normal subgroups:
372:/-- **Schur-Zassenhaus** for normal subgroups:

src/ring_theory/simple_module.lean
21:  * Schur's Lemma: `bijective_or_eq_zero` shows that a linear map between simple modules
26:  * Unify with the work on Schur's Lemma in a category theory context
118:/-- **Schur's Lemma** for linear maps between (possibly distinct) simple modules -/
134:/-- Schur's Lemma makes the endomorphism ring of a simple module a division ring. -/

src/algebra/algebra/spectrum.lean
317:-- We will use this both to show eigenvalues exist, and to prove Schur's lemma.

src/category_theory/preadditive/schur.lean
13:# Schur's lemma
14:We first prove the part of Schur's Lemma that holds in any preadditive category with kernels,
18:Second, we prove Schur's lemma for `𝕜`-linear categories with finite dimensional hom spaces,
38:The part of **Schur's lemma** that holds in any preadditive category with kernels:
49:As a corollary of Schur's lemma for preadditive categories,
67:Part of **Schur's lemma** for `𝕜`-linear categories:
94:An auxiliary lemma for Schur's lemma.
123:**Schur's lemma** for endomorphisms in `𝕜`-linear categories.
136:**Schur's lemma** for `𝕜`-linear categories:

[Pierre-Alexandre Bazin]

Oh, I'll look at this

[Pierre-Alexandre Bazin]

Also how do you do this term search over all the mathlib ?

[Floris van Doorn]

In VSCode you can click the magnifying class in the top-left of the screen (or press ctrl+shift+F) to search all files in your current project.

[Alex J. Best]

rg is ripgrep (https://github.com/BurntSushi/ripgrep) which just searches for text in files in a sensible way, it works pretty well in mathlib

[Alex J. Best]

But it relies a bit on theorems being labelled with their common names in doc-strings which isn't always the case, adding more docstrings with human recognizable names is very welcome :smile:

[Kevin Buzzard]

I would like to make progress here. This is on the UG list and it's also related to group cohomology. We have the category of R-modules for R a ring IIRC. Do we have the category of G-modules for G a group or are we supposed to use monoid_algebra ulift int G or some nonsense like this?

Here is a concrete question. If 3 is done then can we cross Schur's lemma off the UG list? If not, what is the precise Lean form of the lemma which needs to be proved before we can? @Patrick Massot do you have an opinion about this? I think it's time we finished the algebra and group theory parts of the UG curriculum

[Patrick Massot]

We want something like https://en.wikipedia.org/wiki/Schur%27s_lemma#Statement_and_Proof_of_the_Lemma

[Johan Commelin]

I'm trying to write a Lean sketch of the statement

[Pierre-Alexandre Bazin]

Actually, it seems a group representation is never defined explicitly in mathlib - maybe we should define it as a k-linear action of G over a k-vector space and then prove it's in fact a module over the group ring of k ?

[Pierre-Alexandre Bazin]

Or we could directly define it as a module over the group ring

[Julian Külshammer]

There was some previous discussion about this in the following thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Representation.20Theory/near/265624695

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/simple_module.lean#L118L158 looks very much like what we want.

[Johan Commelin]

Missing stuff:

• connection between docs#is_simple_module and docs#category_theory.simple
• for reasons of definitional equality, I think it's good if representations are modeled with a lot of redundancy. Something like

local notation K`[`G`]` := monoid_algebra K G

variables {G K V V₁ V₂ : Type*} [monoid G] [ring K]
variables [add_comm_group V] [distrib_mul_action G V] [module K V] [module (K[G]) V]
variables [is_scalar_tower G (K[G]) V] [is_scalar_tower K (K[G]) V]

What we need is easy ways to deduce half of this information from the other half.

[Johan Commelin]

For example, if we know module (K[G]) V then maybe a tactic can add [distrib_mul_action G V] and [is_scalar_tower G (K[G]) V].

[Johan Commelin]

Vice versa, if [distrib_mul_action G V] [module K V] are known, then

[module (K[G]) V] [is_scalar_tower G (K[G]) V] [is_scalar_tower K (K[G]) V]

can be added provided there is a suitable linearity condition satisfied.

[Johan Commelin]

Also missing, afaik:

instance monoid_algebra.monoid_action : distrib_mul_action G (K[G]) :=
{ smul := λ g x, monoid_algebra.of K G g * x,
  one_smul := λ x, by simp only [map_one, one_mul],
  mul_smul := by { intros, simp only [map_mul, mul_assoc] },
  smul_add := by { intros, simp only [mul_add] },
  smul_zero := λ g, mul_zero _ }

[Johan Commelin]

@Eric Wieser If you have some time to figure out the best way to set up all the scalar actions involved here, that would be really great. Getting the basic definition right has basically been blocking all progress in representation theory in mathlib for > 2 years.

[Eric Wieser]

I think that second action is docs#finsupp.comap_mul_action, which cannot be an instance as it causes diamonds

[Eric Wieser]

Hmm, actually finsupp.comap_mul_action is the action by g⁻¹ instead of g, just to make things more confusing

[Eric Wieser]

Sorry, it's me that's confused after all. docs#finsupp.comap_mul_action is indeed a different generalization of that instance, and the two really coincide when group G:

import algebra.monoid_algebra.basic

variables {G K : Type*}

noncomputable instance monoid_algebra.monoid_action [monoid G] [ring K] :
  distrib_mul_action G (monoid_algebra K G) :=
{ smul := λ g x, monoid_algebra.of K G g * x,
  one_smul := λ x, by simp only [map_one, one_mul],
  mul_smul := by { intros, simp only [map_mul, mul_assoc] },
  smul_add := by { intros, simp only [mul_add] },
  smul_zero := λ g, mul_zero _ }

attribute [ext] distrib_mul_action mul_action has_scalar

lemma monoid_algebra.monoid_action_eq_comap [group G] [ring K]:
  (finsupp.comap_distrib_mul_action : distrib_mul_action G (G →₀ K)) = monoid_algebra.monoid_action :=
  begin
    ext,
    dsimp [(•)],
    rw [monoid_algebra.single_mul_apply, one_mul],
  end

[Julian Külshammer]

This (the action of the inverse) comes from the fact that if G acts (on the left) on M, then normally G would act on the right on $Hom_k(M,N)$. But since $kG$ is a Hopf algebra, you can convert the right action into a left action using the antipode, which in the case of group algebras is the map $g\mapsto g^{-1}$.

[Johan Commelin]

@Eric Wieser So what would you suggest as the Lean way to talk about representations?

[Eric Wieser]

docs#monoid_algebra.comap_distrib_mul_action_self is a slightly clearer version

[Eric Wieser]

I don't really know what representations are right now so am not sure I can help without doing some background reading.

[Eric Wieser]

In case others haven't seen it, #11574 seem relevant here

[Johan Commelin]

@Eric Wieser A K-linear representation of a group G is a K-module V, together with a distrib_mul_action G V such that λ v, g • v is K-linear for all g : G.

[Johan Commelin]

A different way to say exactly the same thing, is to say that V is a monoid_algebra K G-module.

[Johan Commelin]

Of course "a different way to say the same thing" is nice in pen-and-paper maths, but can cause some headaches in Lean.

[Eric Wieser]

The first message is docs#distrib_mul_action.to_linear_map K V g, right?

[Johan Commelin]

Right, I think it is smul_comm_class K G V

[Johan Commelin]

So here's a better version of my list of variables upstairs:

local notation K`[`G`]` := monoid_algebra K G

variables {G K V V₁ V₂ : Type*} [monoid G] [ring K]
variables [add_comm_group V]
variables [distrib_mul_action G V] [module K V] [smul_comm_class K G V]
variables [module (K[G]) V]
variables [is_scalar_tower G (K[G]) V] [is_scalar_tower K (K[G]) V]

[Johan Commelin]

The claim is that

variables [distrib_mul_action G V] [module K V] [smul_comm_class K G V]
-- this line ↓ is the same mathematical content as this line ↑
variables [module (K[G]) V]

[Johan Commelin]

Propositionally asserting that the two lines are compatible is done on the last line, by

variables [is_scalar_tower G (K[G]) V] [is_scalar_tower K (K[G]) V]

[Eric Wieser]

The forward direction of your ↓ is precisely action_to_module from #11574

[Eric Wieser]

My question that I don't have an answer to - what happens when V = K[G]? Does the action agree with left-multiplication?

[Kevin Buzzard]

Yes, it looks like it to me.

[Eric Wieser]

In that case we ought to be able to remove the diamond

[Eric Wieser]

even if we can't, a non-defeq diamond is a lot less bad than a non-equal diamond

[Eric Wieser]

I've opened #11900 to remove the group G requirement from finsupp.comap_distrib_mul_action

[Eric Wieser]

Eric Wieser said:

docs#monoid_algebra.comap_distrib_mul_action_self is a slightly clearer version

I'm pretty sure this instance forms a non-equal diamond when G = kˣ

[Johan Commelin]

That's exactly a common example in maths. So we better get that one right (-;

[Johan Commelin]

What exactly is the diamond you are thinking of? (In this common example, k will be a field, hence commutative).

[Eric Wieser]

I'm trying to prove it now

[Eric Wieser]

/-- The actions by `monoid_algebra.comap_distrib_mul_action_self` and
`monoid_algebra.distrib_mul_action` are incompatible in the case when `G = kˣ` and
`kˣ` is nontrivial -/
example [semiring k] [nontrivial kˣ]:
  (monoid_algebra.comap_distrib_mul_action_self : distrib_mul_action kˣ (monoid_algebra k kˣ)) ≠
    monoid_algebra.distrib_mul_action :=
begin
  obtain ⟨u : kˣ, hu⟩ := exists_ne (1 : kˣ),
  haveI : nontrivial k := ⟨⟨u, 1, units.ext.ne hu⟩⟩,
  intro h,
  replace h := congr_arg (λ x : distrib_mul_action _ _, x.to_mul_action.to_has_scalar.smul) h,
  replace h := finsupp.congr_fun (congr_fun (congr_fun h u) (single u 1)) u,
  dsimp only at h,
  rw [comap_smul_single, smul_apply, single_eq_same, smul_eq_mul, units.smul_def, smul_eq_mul,
    mul_one, single_eq_pi_single] at h,
  apply hu,
  ext,
  rw ←h,
  dsimp,
  by_cases huu : u * u = u,
  { rw [huu, pi.single_eq_same], },
  { rw pi.single_eq_of_ne' huu at h,
    exact (u.ne_zero h.symm).elim, }
end

[Eric Wieser]

Should I add the finsupp version of that example next to finsupp.comap_mul_action to warn of the dangers?

example [semiring k] [nontrivial kˣ]:
  (finsupp.comap_distrib_mul_action : distrib_mul_action kˣ (kˣ →₀ k )) ≠
    finsupp.distrib_mul_action _ _ :=
begin
  obtain ⟨u : kˣ, hu⟩ := exists_ne (1 : kˣ),
  haveI : nontrivial k := ⟨⟨u, 1, units.ext.ne hu⟩⟩,
  intro h,
  replace h := congr_arg (λ x : distrib_mul_action _ _, x.to_mul_action.to_has_scalar.smul) h,
  replace h := finsupp.congr_fun (congr_fun (congr_fun h u) (single u 1)) u,
  dsimp only at h,
  rw [comap_smul_single, smul_apply, single_eq_same, smul_eq_mul, units.smul_def, smul_eq_mul,
    mul_one, single_eq_pi_single] at h,
  apply hu,
  ext,
  rw ←h,
  dsimp,
  by_cases huu : u * u = u,
  { rw [huu, pi.single_eq_same], },
  { rw pi.single_eq_of_ne' huu at h,
    exact (u.ne_zero h.symm).elim, }
end

[Pierre-Alexandre Bazin]

connection between docs#is_simple_module and docs#category_theory.simple

I'm working on this

[Kevin Buzzard]

Yes, that's a part of the story we're sure about :-)

[Eric Wieser]

Eric Wieser said:

Eric Wieser said:

docs#monoid_algebra.comap_distrib_mul_action_self is a slightly clearer version

I'm pretty sure this instance forms a non-equal diamond when G = kˣ

#11918 proves that this forms a diamond and as a result changes monoid_algebra.comap_distrib_mul_action_self to a def.

[Eric Wieser]

Eric Wieser said:

In that case we ought to be able to remove the diamond

We can make _this_ diamond defeq by changing

instance : has_mul (monoid_algebra k G) :=
⟨λf g, f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ * a₂) (b₁ * b₂)⟩

to

instance : has_mul (monoid_algebra k G) :=
⟨λf g, f.sum $ λa₁ b₁, b₁ • g.sum $ λa₂ b₂, single (a₁ * a₂) b₂⟩

Note that this diamond only occurs at all though if we allow the instance that I mention above as forming an unsolvable diamond...

[Pierre-Alexandre Bazin]

Pull request #11927 makes the link between simple modules and the Module category.

[Johan Commelin]

@Eric Wieser Can we make G act on k[G] from the right?

[Johan Commelin]

@Pierre-Alexandre Bazin Thanks for your PR! I left two comments.

[Johan Commelin]

One further remark, do you think the subproofs are useful as stand-alone lemmas for possible future work? If so, please extract them into their own lemmas.

[Eric Wieser]

I don't think acting from the right vs left makes any difference to the potential for diamonds

[Oliver Nash]

Pierre-Alexandre Bazin said:

Or we could directly define it as a module over the group ring

I vote for not doing this. I think we should define a group representation as a linear action on a module. We already have docs#lie_module and this has worked well so far. We did not define Lie algebra representations as representations of their universal enveloping algebra (though we do have this equivalence).

[Johan Commelin]

Eric Wieser said:

I don't think acting from the right vs left makes any difference to the potential for diamonds

Why not? Because then there will be two different actions: one on the left, one on the right. So the diamond vanishes because it doesn't even typecheck.

[Eric Wieser]

The same diamond should exist on both sides

[Eric Wieser]

The only reason it doesn't right now is that we're missing the right action by the units (corresponding to the right action by the underlying ring), but that's not a deliberate omission

[Johan Commelin]

Ok, fair enough. (But who would multiply with a units K on the right?? :rofl:)

[Eric Wieser]

I can see someone maybe wanting to do that if k is not commutative

[Julian Külshammer]

Would it be a solution to strongly suggest to the user to use a typeclass synonym for units K if they want to take it as G in the monoid_algebra K G?

[Johan Commelin]

Like Gm K?

[Eric Wieser]

What would be the difference between that synonym and the units themselves?

[Johan Commelin]

Different instances?

[Johan Commelin]

But I'm not sure if that's the right solution

[Eric Wieser]

Right, my question is which instance you would remove

[Johan Commelin]

Gm R is only defined for commutative rings R. Maybe that helps.

[Johan Commelin]

Really, I think that expressions of the form $∑_{g ∈ G} c_g • [g]$ with $c_g ∈ K$ should only accept scalar multiplication by $x ∈ K$ on the left and by $h ∈ G$ on the right.

[Johan Commelin]

That's what the notation forces on you.

[Johan Commelin]

@Julian Külshammer Do people consider monoid_algebra R G for non-commutative R?

[Eric Wieser]

With that rule you can't scalar multiply by nat

[Eric Wieser]

Johan Commelin said:

Julian Külshammer Do people consider monoid_algebra R G for non-commutative R?

I think @Oliver Nash did in the context of lie algebras; monoid_algebra doubles as a magma_algebra

[Johan Commelin]

But do we need an action from K on the right?

[Johan Commelin]

And more importantly, do we need an action from units K on the right. I very much doubt this.

[Eric Wieser]

Note that in the WIP #10716 I attempt to change algebra R A to additionally require that A has a compatible right-R action

[Eric Wieser]

In which case yes, we need a k-action from the right for monoid_algebra k G to be a k-algebra.

[Julian Külshammer]

@Johan Commelin Usually by a (not necessarily commutative) $R$-algebra $A$ one means that $R$ is commutative and that the action of $R$ is central on $A$. There is the more general concept , slightly confusingly called a $\Lambda$-ring, which is the same as a monoid object in the category of $\Lambda$-$\Lambda$-bimodules. In this case one usually doesn't assume that $\Lambda$ is commutative. And people (e.g. one of my PhD students) in particular work with skew group rings.

[Eric Wieser]

One option would just to be state that we don't care about diamonds - we seem to have them all over the place anyway. One I found just now:

import ring_theory.algebraic
universes u v
variables (R' : Type u) (S' : Type v)
open_locale polynomial
open polynomial

/-- `polynomial.has_scalar_pi` forms a diamond. -/
example [semiring R'] [nontrivial R'] :
  polynomial.has_scalar_pi _ _ ≠ (pi.has_scalar : has_scalar (R'[X]) (R' → R'[X])) :=
begin
  intro h,
  simp_rw [has_scalar.ext_iff, function.funext_iff, polynomial.ext_iff] at h,
  simpa using h X 1 1 0,
end

[Eric Wieser]

(de-instanced in #11935)

[Reid Barton]

That whole section pi looks a bit weird anyways

[Oliver Nash]

Eric Wieser said:

Johan Commelin said:

Julian Külshammer Do people consider monoid_algebra R G for non-commutative R?

I think Oliver Nash did in the context of lie algebras; monoid_algebra doubles as a magma_algebra

That's right. In my application R was commutative but the key result I needed was docs#monoid_algebra.lift_magma and this does not assume commutative coefficients.

[Johan Commelin]

One hacky way would be to define a right action of list G on monoid_algebra R G. Where [g] acts in the expected way. And longer lists act by repeated scalar multiplication (= first applying list.prod and then doing the scalar multiplication).

[Johan Commelin]

It would recover the notation that is used on paper :rofl:

[Eric Wieser]

you'd need to define * on list for that to work

[Yakov Pechersky]

I had added those polynomial pi scalar instances to think of polynomials as functions. What was my conceptual mistake? I'd like to understand what I got wrong.

[Reid Barton]

Well maybe I'm just not managing to reconstruct the kind of situation where you would want to use this instance.

[Reid Barton]

It's usually not that natural to think of polynomials as functions (e.g. because the function might not determine the polynomial). But mainly, I would expect (maybe naively) this instance to built out of other instances such as: if R acts on S then a -> R acts on a -> S (pointwise)

[Yakov Pechersky]

I have some unpushed branches on tropical polynomials that I think used these. So while I don't have them published, I guess we can uninstance them.

If we consider polynomials not as algebraic objects but as more high school terms, they're taught as functions. The function one gets through eval or aeval is uniquely determined over some semirings (fundamental theorem etc etc). That's the pointwise instance what I was "using" in these cases.

[Eric Wieser]

Your pointwise instance was acting on the domain though, which is not how any of our other instances act

[Eric Wieser]

Actually, that looks like it's really the same sort of diamond as the docs#pi.has_scalar' one I made a thread about a while ago

[Yakov Pechersky]

Ah, I found (thanks to Rob's CI script) where I was using the instance:

-- f(X) = √(X ^ 3 − 3 X + 1),
-- which is a root of Y ^ 2 − (X ^ 3 − 3 X + 1), is an algebraic function
example : is_algebraic (polynomial ℤ) (λ x, complex.cpow (x ^ 3 - 3 • x + 1) (1 / 2)) := sorry

https://github.com/pechersky/gouvea/blob/main/src/chapters/ch001/pg010.lean#L47-L72