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.

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_inv {k G : Type u} [CommRing k] [Group G] (g : G) (X : FDRep k G) : (equivApp g X).inv = ModuleCat.ofHom (X.ρ g⁻¹)

@[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)

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] [Finite 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_injective {k G : Type u} [CommRing k] [Group G] [Finite G] [Nontrivial k] : Function.Injective ⇑(equivHom k G)

@[deprecated TannakaDuality.FiniteGroup.equivHom_injective (since := "2025-04-27")]

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

Alias of TannakaDuality.FiniteGroup.equivHom_injective.

def TannakaDuality.FiniteGroup.mulRepHom {k G : Type u} [CommRing k] [Group G] [Finite 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] [Finite 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] [Finite 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)) ⋯ ⋯

def TannakaDuality.FiniteGroup.sumSMulInv {k G : Type u} [CommRing k] [Group G] [Fintype G] {X : FDRep k G} (v : ↑X.V) : (G → k) →ₗ[k] ↑X.V

For v : X and G a finite group, the G-equivariant linear map from the right regular representation rightFDRep to X sending single 1 1 to v.

Equations

• TannakaDuality.FiniteGroup.sumSMulInv v = { toFun := fun (f : G → k) => ∑ s : G, f s • (X.ρ s⁻¹) v, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TannakaDuality.FiniteGroup.sumSMulInv_apply {k G : Type u} [CommRing k] [Group G] [Fintype G] {X : FDRep k G} (v : ↑X.V) (f : G → k) : (sumSMulInv v) f = ∑ s : G, f s • (X.ρ s⁻¹) v

@[simp]

theorem TannakaDuality.FiniteGroup.sumSMulInv_single_id {k G : Type u} [CommRing k] [Group G] [Fintype G] [DecidableEq G] {X : FDRep k G} (v : ↑X.V) : ∑ s : G, Pi.single 1 1 s • (X.ρ s⁻¹) v = v

def TannakaDuality.FiniteGroup.ofRightFDRep {k G : Type u} [CommRing k] [Group G] [Finite G] [Fintype G] (X : FDRep k G) (v : ↑X.V) : rightFDRep ⟶ X

For v : X and G a finite group, the representation morphism from the right regular representation rightFDRep to X sending single 1 1 to v.

Equations

• TannakaDuality.FiniteGroup.ofRightFDRep X v = { hom := ModuleCat.ofHom (TannakaDuality.FiniteGroup.sumSMulInv v), comm := ⋯ }

@[simp]

theorem TannakaDuality.FiniteGroup.ofRightFDRep_hom {k G : Type u} [CommRing k] [Group G] [Finite G] [Fintype G] (X : FDRep k G) (v : ↑X.V) : (ofRightFDRep X v).hom = ModuleCat.ofHom (sumSMulInv v)

theorem TannakaDuality.FiniteGroup.toRightFDRepComp_injective {k G : Type u} [CommRing k] [Group G] [Finite G] {η₁ η₂ : CategoryTheory.Aut (forget k G)} (h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep) : η₁ = η₂

def TannakaDuality.FiniteGroup.leftRegularFDRepHom {k G : Type u} [CommRing k] [Group G] [Finite G] (s : G) : CategoryTheory.End rightFDRep

leftRegular as a morphism rightFDRep k G ⟶ rightFDRep k G in FDRep k G.

Equations

• TannakaDuality.FiniteGroup.leftRegularFDRepHom s = { hom := ModuleCat.ofHom (TannakaDuality.FiniteGroup.leftRegular s), comm := ⋯ }

theorem TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] (η : CategoryTheory.Aut (forget k G)) : ∃ (s : G), ModuleCat.Hom.hom (η.hom.hom.app rightFDRep) = rightRegular s

theorem TannakaDuality.FiniteGroup.equivHom_surjective {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] : Function.Surjective ⇑(equivHom k G)

def TannakaDuality.FiniteGroup.equiv (k G : Type u) [CommRing k] [Group G] [Finite G] [IsDomain k] : G ≃* CategoryTheory.Aut (forget k G)

Tannaka duality for finite groups:

A finite group G is isomorphic to Aut (forget k G), where k is any integral domain, and forget k G is the monoidal forgetful functor FDRep k G ⥤ FGModuleCat k G.

Equations

• TannakaDuality.FiniteGroup.equiv k G = MulEquiv.ofBijective (TannakaDuality.FiniteGroup.equivHom k G) ⋯