Tannaka duality for finite groups

Stream: maths

[Yacine Benmeuraiem]

I have formalized Tannaka duality for finite groups and I have been trying to make it suitable to be added to mathlib. Here is the current state.
The "Indicator" section needs cleaning up and should maybe be implemented more generally, there's also the eval_of_alghom which might be interesting in general, and also it might be useful to generalize the representations τᵣ and τₗ as well (representations on spaces of functions with domain G by translations, induced by left and right multiplication in G), that is if these aren't already in mathlib. The rest is specific for the proof and I'm not sure how I'm supposed to deal with that honestly.

[Sophie Morel]

To add some context, Yacine is a student in our "Higher categories and formalization" master's programme de Lyon, and this is his first formalization project. I encouraged him to submit it to mathlib.

[Kevin Buzzard]

@Yacine Benmeuraiem your code doesn't compile for me -- mathlib wants FDRep to eat a Field and you've given it a CommRing.

[Kevin Buzzard]

Line 90: it's not ideal to make definitions in tactic mode, although here you're probably OK; tactic mode can introduce random ids and things which are not needed; maybe

def T_fun (g : G) : Aut (F k G) :=
  LaxMonoidalFunctor.isoOfComponents (T_app g)
  (by intro _ _ f; exact (f.comm g).symm) rfl (by intros; rfl)

is safer.

[Kevin Buzzard]

rfl is better than exact rfl (it's both shorter and more powerful to use the tactic rfl than the term rfl).

[Kevin Buzzard]

abbrev e would not be allowed in mathlib -- you can't just claim e in the root namespace for your function. Probably there is a way of doing this with notation? Similarly with α -- maybe everything should go in a TannakaDuality namespace or something?

[Kevin Buzzard]

lemma mul_e (s : G) (f : G → k) : (e s) * f = f s • (e s) := by
    ext t
    by_cases h : s = t
    · simp [h]
    · simp [e_eq_of_ne h]

-- let the simplifier do the work, you often don't need to explicitly invoke stuff like mul_zero.

[Kevin Buzzard]

Instead of intros at the beginning of a structure field proof (e.g. in \phi) you can move the inputs left of the := e.g.

  map_smul' _ _ := by
    simp [Finset.smul_sum, smul_smul]

[Yacine Benmeuraiem]

Oh yes... I changed FDRep.lean but then I wanted to keep things in one file and I missed something... Rep takes a Ring so I was confused that FDRep needed a Field.
For e I was planning on replacing every instance with Pi.single (as I have with many notations that I was using at first), and similarly for α. I hadn't thought about using notation, it would be nice if that's okay to do.
I was thinking that declaring a bunch of auxiliary things specifically for one proof was not very nice, and maybe some of them could be squeezed in directly where they are used, but I'm not sure if that would be any better. Declaring a namespace sounds good.
Thanks for the feedback!

[Yacine Benmeuraiem]

I created PRs #22173 #22174 #22176.

[Johan Commelin]

Very nice! May I suggest using Finite somewhere in the namespace? Just to leave room for a future Tannaka duality in full generality.

Also, the notation that you set up in the file will be somewhat hard to guess outside of the file. For this reason, I think it is better to use longer names. Such as forget instead of F.

[Yacine Benmeuraiem]

Thanks! I went for the namespace TannakaDuality.FiniteGroup and implemented your suggestions.

[Johan Commelin]

Now that the dependent PR has been merged, could you please merge master into your PR branch?

[Yacine Benmeuraiem]

Done :+1: