Commit 2025-03-13 06:53 6e898a31

View on Github →

feat: definitions for Tannaka duality for finite groups (#22173) Introduces the file Mathlib/RepresentationTheory/Tannaka.lean with the basic definitions required for the proof of Tannaka duality for finite groups, along with the first lemma showing the injectivity of equivHom.

depends on: #22235
depends on: #22668

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/Tannaka.lean

added def TannakaDuality.FiniteGroup.equivApp

added def TannakaDuality.FiniteGroup.equivHom

added theorem TannakaDuality.FiniteGroup.equivHom_inj

added def TannakaDuality.FiniteGroup.forget

added theorem TannakaDuality.FiniteGroup.forget_map

added theorem TannakaDuality.FiniteGroup.forget_obj

added def TannakaDuality.FiniteGroup.leftRegular

added theorem TannakaDuality.FiniteGroup.leftRegular_apply

added def TannakaDuality.FiniteGroup.rightFDRep

added def TannakaDuality.FiniteGroup.rightRegular

added theorem TannakaDuality.FiniteGroup.rightRegular_apply