Theorems · Definition · group theory

TannakaDuality.FiniteGroup.equiv

(k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Group G] → [Finite G] → [IsDomain k] → G ≃* CategoryTheory.Aut (TannakaDuality.FiniteGroup.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.

Defined in

Mathlib.RepresentationTheory.Tannaka

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingGroupFiniteIsDomain