Proving equivalence of representation statements

Stream: mathlib4

[Gareth Ma]

RepresentationTheory has 3 (eh, mostly 2) ways of writing down a representation of a group G. Here are my notes I have on a paper, to make the rest of this question make more sense

1. Rep : defined categorically, an `Action` of `G` in the category of `MonCat`
2. Representation : the explicit definition `G →* V →ₗ[k] V`
3. k[G]-Module : a module over k[G], written as `[Module (MonoidAlgebra k G) V]`

1 <=> 2: <V.ρ, Rep.of>
1 <=> 3: Rep.equivalenceModuleMonoidAlgebra
2 <=> 3: <Representation.asModuleModule, Representation.ofModule>

(Oh also FdRep has another separate definition, an Action over a FGMod)

To say a representation $\rho$ is irreducible, for (1) CategoryTheory.Simple is used, and for (3) RingTheory.IsSimpleModule is used I believe. So now I want to prove they are the same thing:

import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.RingTheory.SimpleModule
import Mathlib.CategoryTheory.Simple

theorem Rep.is_simple_iff_isSimpleModule
    {G : Type u} [Group G] {V : Rep k G} [inst : Nontrivial V.V] :
    Simple V ↔ IsSimpleModule (MonoidAlgebra k G) V.ρ.asModule := by

I tried both directions for maybe 2/3 hours but can't get anywhere, so if someone can help that would be great :sweat:

[Gareth Ma]

Here's my attempt on one direction =>:

theorem Rep.isSimpleModule_of_Simple {G : Type u} [Group G] {V : Rep k G}
    [inst : Nontrivial V.V] (hV : Simple V) :
      IsSimpleModule (MonoidAlgebra k G) V.ρ.asModule := by
  obtain ⟨hV⟩ := hV
  refine IsSimpleOrder.mk (toNontrivial := ?_) ?_
  · /- Nontrivial instance can't be inferred.. -/
    use ⊥, ⊤
    rw [ne_comm, Ne, Submodule.eq_bot_iff]
    push_neg
    obtain ⟨y, hy⟩ := exists_ne (0 : V.V)
    use y, mem_top, hy
  · intro W
    let W' := Rep.equivalenceModuleMonoidAlgebra.inverse.obj $ ModuleCat.of (MonoidAlgebra k G) W
    specialize @hV W'
    let hom := W.subtype
    /- So W.subtype gives a k[G]-linear hom (W →ₗ[k[G]] V.ρ.asModule) -/
    /- But I want a (CT) morphism (W' : Rep k G) ⟶ V -/

[Kevin Buzzard]

Can you make a #mwe ? I get errors if I just naively add the imports from the first code block into the second.

[Gareth Ma]

import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.RingTheory.SimpleModule
import Mathlib.CategoryTheory.Simple

open LinearMap Module Submodule Representation FiniteDimensional Function Pointwise CategoryTheory
  MonoidAlgebra JordanHolderModule

universe u
variable {n : ℕ} (hn : 1 < n) {k : Type u} [Field k] {ζ : k} (hζ : ζ ∈ primitiveRoots n k)

def Rep.smul_def {G V : Type u} [Group G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V}
    (g : MonoidAlgebra k G) (x : ρ.asModule) :
      g • x = (ρ.asAlgebraHom g) x := by
  rfl

-- Idk if this is useful but it exists
def lift_rep_hom {G : Type u} [Group G] {V W : Rep k G} (f : V ⟶ W) :
    V.ρ.asModule →ₗ[MonoidAlgebra k G] W.ρ.asModule := by
  -- I don't know how this works but if you remove any part of this e.g. try to
  -- "inline" the f_mod definition into the use, it will fail!
  let f_mod : V.ρ.asModule →+ W.ρ.asModule := (f.hom : V.V →+ W.V)
  use f_mod, fun g x ↦ ?_
  simp
  obtain ⟨⟨f', hf'₁⟩, hf'₂⟩ := f
  simp [Rep.smul_def, asAlgebraHom, lift_apply']
  rw [map_finsupp_sum]
  congr! with g c
  change f'.toFun _ = c • (W.ρ g) (f'.toFun x)
  rw [hf'₁]
  congr 1
  exact Rep.hom_comm_apply ⟨⟨f', hf'₁⟩, hf'₂⟩ g x

-- A (finite dimensional) kG-representation is simple if and only if it's a simple module over k
theorem FdRep.is_simple_iff_isSemiSimple'' {G : Type u} [Group G] {V : FdRep k G} :
    Simple V ↔ IsSimpleModule k V := by
  -- Supposedly it should be unwrapping definitions and lifting morphisms between types
  -- But uh
  sorry

[Gareth Ma]

sorry for that, I got too frustrated and forgot

[Kevin Buzzard]

Half-hearted start (I'm off to catch a train) but I agree this is a pain. Probably this API should be there. Mathlib, as you've pointed out, has several ways of defining representations and we need the API to go between them assuming we're not planning on nuking any of them (which we're not as far as I know)

[Kevin Buzzard]

import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.RingTheory.SimpleModule
import Mathlib.CategoryTheory.Simple

open MonoidAlgebra Representation CategoryTheory

universe u

variable {k : Type u} [Field k]

-- missing API?
theorem Submodule.bot_eq_top_iff_subsingleton (W : Type*) [AddCommGroup W] [Module k W] :
    (⊥ : Submodule k W) = ⊤ ↔ Subsingleton W := by
  refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ ?_⟩
  · intros x y
    have foo : x ∈ (⊤ : Submodule k W) := mem_top
    rw [← h, mem_bot] at foo
    rw [foo, eq_comm, ← mem_bot k, h]
    apply mem_top
  · ext x
    simp
    apply h.1

-- A (finite dimensional) kG-representation is simple if and only if it's a simple module over k
theorem FdRep.is_simple_iff_isSemiSimple'' {G : Type u} [Group G] {V : FdRep k G} :
    Simple V ↔ IsSimpleModule k V := by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩
  · have : Nontrivial (Submodule k V) := {
    exists_pair_ne := ⟨⊥, ⊤, fun h2 ↦ by
      apply id_nonzero V
      change (⊥ : Submodule k V) = ⊤ at h2
      ext (x : V)
      simp only [Action.id_hom, id_apply, Action.zero_hom]
      rw [Submodule.bot_eq_top_iff_subsingleton] at h2
      apply h2.1⟩}
    refine ⟨?_⟩
    intro M
    -- now make M ⟶ V or V ⟶ V / M (possibly easier to show the latter is fd) and go from there
    sorry
  · rintro Y hY _
    -- constructor, then grind it out? Use h to prove nontrivial V, and if f isn't 0 then
    -- the image of f is not bot so it's top, and the kernel of f is bot because f is mono,
    -- so f is an isomorphism by abelian category
    sorry

[Andrew Yang]

docs#Submodule.subsingleton_iff and docs#subsingleton_iff_bot_eq_top for the first one.

[Andrew Yang]

Though we are probably missing things like

theorem CategoryTheory.Functor.map_isZero_iff {C D} [Category C] [Category D] (F : C ⥤ D)
    [HasZeroMorphisms C] [HasZeroMorphisms D] [PreservesZeroMorphisms F] [Faithful F] {X} :
    IsZero (F.obj X) ↔ IsZero X := by
  rw [IsZero.iff_id_eq_zero, IsZero.iff_id_eq_zero, ← F.map_id, F.map_eq_zero_iff]

theorem ModuleCat.isZero_iff {R} [Ring R] {M : ModuleCat R} : IsZero M ↔ Subsingleton M :=
  ⟨fun h ↦ @Equiv.subsingleton _ _
    ((forget _).mapIso (h.iso (isZero_of_subsingleton (ModuleCat.of R PUnit)))).toEquiv
    (inferInstanceAs (Subsingleton PUnit)), fun _ ↦ isZero_of_subsingleton _⟩

theorem FdRep.isZero_iff {G : Type u} [Group G] {V : FdRep k G} : IsZero V ↔ Subsingleton V := by
  rw [← (forget₂ (FdRep k G) (FGModuleCat k)).map_isZero_iff,
    ← (FGModuleCat.forget₂Monoidal _).map_isZero_iff, ModuleCat.isZero_iff]
  rfl

instance {G : Type u} [Group G] {V : FdRep k G} [Simple V] : Nontrivial V := by
  rw [← not_subsingleton_iff_nontrivial, ← FdRep.isZero_iff]
  exact Simple.not_isZero V

[Oliver Nash]

I've said this before elsewhere but I'd encourage anyone thinking about our group representation API to consider the following alternate design (which would replace docs#Representation):

import Mathlib.RepresentationTheory.Basic

variable (R G M : Type*) [CommRing R] [AddCommGroup M] [Module R M] [Group G]

class GroupRepresentation [MulAction G M] extends SMulCommClass R G M :=
  smul_add (g : G) (m n : M) : g • (m + n) = g • m + g • n

-- Or maybe even:
abbrev GroupRepresentation' [MulAction G M] [DistribSMul G M] := SMulCommClass R G M

This is the approach taken in docs#LieModule and seems to have worked nicely there.

[Oliver Nash]

The only potential problem I see would be the case when R = G since there would be two scalar actions on M but with the typeclasses I have proposed, this cannot thappen.

[Kevin Buzzard]

I think this can happen because unfortunately the trivial ring is a group. This could be fixed by demanding that R is nontrivial, as a nontrivial group can't have a 0.

I'm motivated to make this refactor because I have a Masters student developing the representation theory of locally profinite groups, and if it happens then the sooner the better. R could still be a CommSemiring as far as I can see, but the other big change, namely that G is no longer allowed to be a monoid (stopping G = R from being possible), is somehow nontrivial. Do we actually care about representations of monoids? The reason I like this approach is that I personally don't think I care about such things, but adding sane hypotheses like R != 0 and G is a group might upset some of the generalists among us, who will observe that the original definition works fine in this case. This might be true but do we ever need it in practice? If people actually about representations of monoids then this might be a blocker.

[Kevin Buzzard]

Another question: why

abbrev GroupRepresentation' [MulAction G M] [DistribSMul G M] := SMulCommClass R G M

? How about

abbrev GroupRepresentation' [DistribMulAction G M] := SMulCommClass R G M

? Does [MulAction G M] [DistribSMul G M] create a diamond for SMul G M?

[Damiano Testa]

I think that the theory of representations of general monoids is just really hard and not much has been done. In simple cases, there are ad hoc methods where you can pretend that you are dealing with representations of a close-by group. This MO question gives some examples.

[Kevin Buzzard]

But the question is: do we literally stop people from being able to talk about representations of monoids? Pros: all the worries about k = G go away. Cons: we can't talk about representations of monoids any more.

[Damiano Testa]

I suspect that no one has effectively used representations of monoids. Maybe, when there is an interest, whoever needs to weaken the assumptions Group --> Monoid can think about how to do it?

[Damiano Testa]

I feel that this is one of these situations where, in informal maths you say "this is all the same for monoids". In reality, it is not true, but since your monoid was Nat, it is actually true.

[Matthew Ballard]

Damiano Testa said:

I suspect that no one has effectively used representations of monoids.

This is referencing mathlib right?

[Kevin Buzzard]

I've remembered the diamond that this introduces: if R acts on M then so does the unit group R^x, so there are problems if G=R^x. In Iwasawa you have $\Z_p^x$ acting on $\Z_p$-modules in a nontrivial way :-/

[Damiano Testa]

Matthew Ballard said:

Damiano Testa said:

I suspect that no one has effectively used representations of monoids.

This is referencing mathlib right?

Yes, I meant in mathlib.

I find it hard to express the concept, but I would like to say that no one has really needed representations of non-group monoids in mathlib.

[Oliver Nash]

Kevin Buzzard said:

I've remembered the diamond that this introduces: if R acts on M then so does the unit group R^x, so there are problems if G=R^x. In Iwasawa you have $\Z_p^x$ acting on $\Z_p$-modules in a nontrivial way :-/

Oh darn, that is a shame. So even informally if $u \in \Z_p^ˣ$ and $v$ is a vector in some $\Z_p$-module, then one has to be mindful of the context to know what someone means mean if they write $u \cdot v$?

[Kevin Buzzard]

yeah, the trick in the literature is that they use different notation for the elements of Z_p^* ;-) For p>2 this group is topologically cyclic and if gamma is a fixed generator then equations like $\gamma\cdot z=\chi(\gamma)z$ are just understood by the reader who I guess is assumed to be an expert in the area :-) ("obviously if I write the dot I mean the group action, and if I don't I mean the module action")

[Yaël Dillies]

Yeah, maybe Iwasawa should use a type synonym for Z_p^*

[Kevin Buzzard]

Yup

[Oliver Nash]

Yaël Dillies said:

Yeah, maybe Iwasawa should use a type synonym for Z_p^*

Good point; in fact it would have to use a synonym or else there would be two scalar actions in view of docs#Units.instSMul So in fact I retract my "Oh darn" above.