Tannaka duality for finite groups

In this file we prove Tannaka duality for finite groups.

The theorem can be formulated as follows: for any integral domain k, a finite group G can be recovered from FDRep k G, the monoidal category of finite dimensional k-linear representations of G, and the monoidal forgetful functor forget : FDRep k G ⥤ FGModuleCat k.

More specifically, the main result is the isomorphism equiv : G ≃* Aut (forget k G).

Reference

https://math.leidenuniv.nl/scripties/1bachCommelin.pdf

instance TannakaDuality.FiniteGroup.instMonoidalFDRepFGModuleCatForget₂ {k G : Type u} [CommRing k] [Group G] : (CategoryTheory.forget₂ (FDRep k G) (FGModuleCat k)).Monoidal

Equations

• TannakaDuality.FiniteGroup.instMonoidalFDRepFGModuleCatForget₂ = id inferInstance

def TannakaDuality.FiniteGroup.forget (k G : Type u) [CommRing k] [Group G] : CategoryTheory.LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)

The monoidal forgetful functor from FDRep k G to FGModuleCat k.

Equations

• TannakaDuality.FiniteGroup.forget k G = CategoryTheory.LaxMonoidalFunctor.of (CategoryTheory.forget₂ (FDRep k G) (FGModuleCat k))

@[simp]

theorem TannakaDuality.FiniteGroup.forget_obj {k G : Type u} [CommRing k] [Group G] (X : FDRep k G) : (forget k G).obj X = X.V

@[simp]

theorem TannakaDuality.FiniteGroup.forget_map {k G : Type u} [CommRing k] [Group G] (X Y : FDRep k G) (f : X ⟶ Y) : (forget k G).map f = f.hom

def TannakaDuality.FiniteGroup.equivApp {k G : Type u} [CommRing k] [Group G] (g : G) (X : FDRep k G) : X.V ≅ X.V

Definition of equivHom g : Aut (forget k G) by its components.

Equations

• TannakaDuality.FiniteGroup.equivApp g X = { hom := ModuleCat.ofHom (X.ρ g), inv := ModuleCat.ofHom (X.ρ g⁻¹), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TannakaDuality.FiniteGroup.equivApp_hom {k G : Type u} [CommRing k] [Group G] (g : G) (X : FDRep k G) : (equivApp g X).hom = ModuleCat.ofHom (X.ρ g)

@[simp]

theorem TannakaDuality.FiniteGroup.equivApp_inv {k G : Type u} [CommRing k] [Group G] (g : G) (X : FDRep k G) : (equivApp g X).inv = ModuleCat.ofHom (X.ρ g⁻¹)

def TannakaDuality.FiniteGroup.equivHom (k G : Type u) [CommRing k] [Group G] : G →* CategoryTheory.Aut (forget k G)

The group homomorphism G →* Aut (forget k G) shown to be an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TannakaDuality.FiniteGroup.equivHom_apply (k G : Type u) [CommRing k] [Group G] (g : G) : (equivHom k G) g = CategoryTheory.LaxMonoidalFunctor.isoOfComponents (equivApp g) ⋯ ⋯ ⋯

def TannakaDuality.FiniteGroup.rightRegular {k G : Type u} [CommRing k] [Group G] : Representation k G (G → k)

The representation on G → k induced by multiplication on the right in G.

Equations

• TannakaDuality.FiniteGroup.rightRegular = { toFun := fun (s : G) => { toFun := fun (f : G → k) (t : G) => f (t * s), map_add' := ⋯, map_smul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TannakaDuality.FiniteGroup.rightRegular_apply {k G : Type u} [CommRing k] [Group G] (s t : G) (f : G → k) : (rightRegular s) f t = f (t * s)

def TannakaDuality.FiniteGroup.leftRegular {k G : Type u} [CommRing k] [Group G] : Representation k G (G → k)

The representation on G → k induced by multiplication on the left in G.

Equations

• TannakaDuality.FiniteGroup.leftRegular = { toFun := fun (s : G) => { toFun := fun (f : G → k) (t : G) => f (s⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TannakaDuality.FiniteGroup.leftRegular_apply {k G : Type u} [CommRing k] [Group G] (s t : G) (f : G → k) : (leftRegular s) f t = f (s⁻¹ * t)

def TannakaDuality.FiniteGroup.rightFDRep {k G : Type u} [CommRing k] [Group G] [Fintype G] : FDRep k G

The right regular representation rightRegular on G → k as a FDRep k G.

Equations

• TannakaDuality.FiniteGroup.rightFDRep = FDRep.of TannakaDuality.FiniteGroup.rightRegular

theorem TannakaDuality.FiniteGroup.equivHom_inj {k G : Type u} [CommRing k] [Group G] [Fintype G] [Nontrivial k] [DecidableEq G] : Function.Injective ⇑(equivHom k G)

def TannakaDuality.FiniteGroup.mulRepHom {k G : Type u} [CommRing k] [Group G] [Fintype G] : CategoryTheory.MonoidalCategoryStruct.tensorObj rightFDRep rightFDRep ⟶ rightFDRep

The FDRep k G morphism induced by multiplication on G → k.

Equations

• TannakaDuality.FiniteGroup.mulRepHom = { hom := ModuleCat.ofHom (LinearMap.mul' k (G → k)), comm := ⋯ }

theorem TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp {k G : Type u} [CommRing k] [Group G] [Fintype G] (η : CategoryTheory.Aut (forget k G)) (f g : G → k) : let α := ModuleCat.Hom.hom (η.hom.hom.app rightFDRep); α (f * g) = α f * α g

The rightFDRep component of η : Aut (forget k G) preserves multiplication

def TannakaDuality.FiniteGroup.algHomOfRightFDRepComp {k G : Type u} [CommRing k] [Group G] [Fintype G] (η : CategoryTheory.Aut (forget k G)) : (G → k) →ₐ[k] G → k

The rightFDRep component of η : Aut (forget k G) gives rise to an algebra morphism (G → k) →ₐ[k] (G → k).

Equations

• TannakaDuality.FiniteGroup.algHomOfRightFDRepComp η = AlgHom.ofLinearMap (ModuleCat.Hom.hom (η.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep)) ⋯ ⋯