Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: definitions for Tannaka duality for finite groups #22173

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4561,6 +4561,7 @@ import Mathlib.RepresentationTheory.GroupCohomology.Resolution
import Mathlib.RepresentationTheory.Invariants
import Mathlib.RepresentationTheory.Maschke
import Mathlib.RepresentationTheory.Rep
import Mathlib.RepresentationTheory.Tannaka
import Mathlib.RingTheory.AdicCompletion.Algebra
import Mathlib.RingTheory.AdicCompletion.AsTensorProduct
import Mathlib.RingTheory.AdicCompletion.Basic
Expand Down
73 changes: 38 additions & 35 deletions Mathlib/RepresentationTheory/FDRep.lean
Original file line number Diff line number Diff line change
Expand Up @@ -45,85 +45,88 @@ open CategoryTheory.Limits


/-- The category of finite dimensional `k`-linear representations of a monoid `G`. -/
abbrev FDRep (k G : Type u) [Field k] [Monoid G] :=
Action (FGModuleCat.{u} k) (MonCat.of G)
abbrev FDRep (R G : Type u) [Ring R] [Monoid G] :=
Action (FGModuleCat.{u} R) (MonCat.of G)

namespace FDRep

variable {k G : Type u} [Field k] [Monoid G]
variable {R k G : Type u} [CommRing R] [Field k] [Monoid G]

-- Porting note: `@[derive]` didn't work for `FDRep`. Add the 4 instances here.
instance : LargeCategory (FDRep k G) := inferInstance
instance : ConcreteCategory (FDRep k G) (Action.HomSubtype _ _) := inferInstance
instance : Preadditive (FDRep k G) := inferInstance
instance : LargeCategory (FDRep R G) := inferInstance
instance : ConcreteCategory (FDRep R G) (Action.HomSubtype _ _) := inferInstance
instance : Preadditive (FDRep R G) := inferInstance
instance : HasFiniteLimits (FDRep k G) := inferInstance

instance : Linear k (FDRep k G) := by infer_instance
instance : Linear R (FDRep R G) := by infer_instance

instance : CoeSort (FDRep k G) (Type u) :=
instance : CoeSort (FDRep R G) (Type u) :=
fun V => V.V⟩

instance (V : FDRep k G) : AddCommGroup V := by
change AddCommGroup ((forget₂ (FDRep k G) (FGModuleCat k)).obj V).obj; infer_instance
instance (V : FDRep R G) : AddCommGroup V := by
change AddCommGroup ((forget₂ (FDRep R G) (FGModuleCat R)).obj V).obj; infer_instance

instance (V : FDRep k G) : Module k V := by
change Module k ((forget₂ (FDRep k G) (FGModuleCat k)).obj V).obj; infer_instance
instance (V : FDRep R G) : Module R V := by
change Module R ((forget₂ (FDRep R G) (FGModuleCat R)).obj V).obj; infer_instance

instance (V : FDRep R G) : Module.Finite R V := by
change Module.Finite R ((forget₂ (FDRep R G) (FGModuleCat R)).obj V); infer_instance

instance (V : FDRep k G) : FiniteDimensional k V := by
change FiniteDimensional k ((forget₂ (FDRep k G) (FGModuleCat k)).obj V); infer_instance
infer_instance

/-- All hom spaces are finite dimensional. -/
instance (V W : FDRep k G) : FiniteDimensional k (V ⟶ W) :=
FiniteDimensional.of_injective ((forget₂ (FDRep k G) (FGModuleCat k)).mapLinearMap k)
(Functor.map_injective (forget₂ (FDRep k G) (FGModuleCat k)))

/-- The monoid homomorphism corresponding to the action of `G` onto `V : FDRep k G`. -/
def ρ (V : FDRep k G) : G →* V →ₗ[k] V :=
def ρ (V : FDRep R G) : G →* V →ₗ[R] V :=
(ModuleCat.endRingEquiv _).toMonoidHom.comp (Action.ρ V).hom

@[simp]
lemma endRingEquiv_symm_comp_ρ (V : FDRep k G) :
lemma endRingEquiv_symm_comp_ρ (V : FDRep R G) :
(MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj).symm).comp (ρ V) =
(Action.ρ V).hom :=
rfl

@[simp]
lemma endRingEquiv_comp_ρ (V : FDRep k G) :
lemma endRingEquiv_comp_ρ (V : FDRep R G) :
(MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj)).comp (Action.ρ V).hom = ρ V := rfl

@[simp]
lemma hom_action_ρ (V : FDRep k G) (g : G) : (Action.ρ V g).hom = ρ V g := rfl
lemma hom_action_ρ (V : FDRep R G) (g : G) : (Action.ρ V g).hom = ρ V g := rfl

/-- The underlying `LinearEquiv` of an isomorphism of representations. -/
def isoToLinearEquiv {V W : FDRep k G} (i : V ≅ W) : V ≃ₗ[k] W :=
FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)
def isoToLinearEquiv {V W : FDRep R G} (i : V ≅ W) : V ≃ₗ[R] W :=
FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat R) (MonCat.of G)).mapIso i)

theorem Iso.conj_ρ {V W : FDRep k G} (i : V ≅ W) (g : G) :
theorem Iso.conj_ρ {V W : FDRep R G} (i : V ≅ W) (g : G) :
W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g) := by
rw [FDRep.isoToLinearEquiv, ← hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj, Iso.conj_apply,
← ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff,
Iso.eq_inv_comp ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)]
Iso.eq_inv_comp ((Action.forget (FGModuleCat R) (MonCat.of G)).mapIso i)]
exact (i.hom.comm g).symm

/-- Lift an unbundled representation to `FDRep`. -/
@[simps ρ]
abbrev of {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
(ρ : Representation k G V) : FDRep k G :=
⟨FGModuleCat.of k V, MonCat.ofHom ρ ≫ MonCat.ofHom
(ModuleCat.endRingEquiv (ModuleCat.of k V)).symm.toMonoidHom⟩
abbrev of {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V]
(ρ : Representation R G V) : FDRep R G :=
⟨FGModuleCat.of R V, MonCat.ofHom ρ ≫ MonCat.ofHom
(ModuleCat.endRingEquiv (ModuleCat.of R V)).symm.toMonoidHom⟩

instance : HasForget₂ (FDRep k G) (Rep k G) where
forget₂ := (forget₂ (FGModuleCat k) (ModuleCat k)).mapAction (MonCat.of G)
instance : HasForget₂ (FDRep R G) (Rep R G) where
forget₂ := (forget₂ (FGModuleCat R) (ModuleCat R)).mapAction (MonCat.of G)

theorem forget₂_ρ (V : FDRep k G) : ((forget₂ (FDRep k G) (Rep k G)).obj V).ρ = V.ρ := by
theorem forget₂_ρ (V : FDRep R G) : ((forget₂ (FDRep R G) (Rep R G)).obj V).ρ = V.ρ := by
ext g v; rfl

-- Verify that the monoidal structure is available.
example : MonoidalCategory (FDRep k G) := by infer_instance
example : MonoidalCategory (FDRep R G) := by infer_instance

example : MonoidalPreadditive (FDRep k G) := by infer_instance
example : MonoidalPreadditive (FDRep R G) := by infer_instance

example : MonoidalLinear k (FDRep k G) := by infer_instance
example : MonoidalLinear R (FDRep R G) := by infer_instance

open Module

Expand All @@ -139,13 +142,13 @@ theorem finrank_hom_simple_simple [IsAlgClosed k] (V W : FDRep k G) [Simple V] [
CategoryTheory.finrank_hom_simple_simple k V W

/-- The forgetful functor to `Rep k G` preserves hom-sets and their vector space structure. -/
def forget₂HomLinearEquiv (X Y : FDRep k G) :
((forget₂ (FDRep k G) (Rep k G)).obj X ⟶
(forget₂ (FDRep k G) (Rep k G)).obj Y) ≃ₗ[k] X ⟶ Y where
def forget₂HomLinearEquiv (X Y : FDRep R G) :
((forget₂ (FDRep R G) (Rep R G)).obj X ⟶
(forget₂ (FDRep R G) (Rep R G)).obj Y) ≃ₗ[R] X ⟶ Y where
toFun f := ⟨f.hom, f.comm⟩
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun f := ⟨(forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom, f.comm⟩
invFun f := ⟨(forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom, f.comm⟩
left_inv _ := by ext; rfl
right_inv _ := by ext; rfl

Expand Down
120 changes: 120 additions & 0 deletions Mathlib/RepresentationTheory/Tannaka.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
/-
Copyright (c) 2025 Yacine Benmeuraiem. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yacine Benmeuraiem
-/
import Mathlib.RepresentationTheory.FDRep

/-!
# 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>
-/

noncomputable section

open CategoryTheory MonoidalCategory ModuleCat Finset Pi

universe u

namespace TannakaDuality

namespace FiniteGroup

variable {k G : Type u} [CommRing k] [Group G]

section definitions

instance : (forget₂ (FDRep k G) (FGModuleCat k)).Monoidal := by
change (Action.forget _ _).Monoidal; infer_instance

variable (k G) in
/-- The monoidal forgetful functor from `FDRep k G` to `FGModuleCat k`. -/
def forget := LaxMonoidalFunctor.of (forget₂ (FDRep k G) (FGModuleCat k))

/-- Definition of `equivHom g : Aut (forget k G)` by its components. -/
@[simps]
def equivApp (g : G) (X : FDRep k G) : X.V ≅ X.V where
hom := ofHom (X.ρ g)
inv := ofHom (X.ρ g⁻¹)
hom_inv_id := by
ext x
change (X.ρ g⁻¹ * X.ρ g) x = x
simp [← map_mul]
inv_hom_id := by
ext x
change (X.ρ g * X.ρ g⁻¹) x = x
simp [← map_mul]

variable (k G) in
/-- The group homomorphism `G →* Aut (forget k G)` shown to be an isomorphism. -/
def equivHom : G →* Aut (forget k G) where
toFun g :=
LaxMonoidalFunctor.isoOfComponents (equivApp g) (fun f ↦ (f.comm g).symm) rfl (by intros; rfl)
map_one' := by ext; simp; rfl
map_mul' _ _ := by ext; simp; rfl

/-- The representation on `G → k` induced by multiplication on the right in `G`. -/
@[simps]
def rightRegular : Representation k G (G → k) where
toFun s := {
toFun f t := f (t * s)
map_add' _ _ := rfl
map_smul' _ _ := rfl
}
map_one' := by
ext
simp
map_mul' _ _ := by
ext
simp [mul_assoc]

/-- The representation on `G → k` induced by multiplication on the left in `G`. -/
@[simps]
def leftRegular : Representation k G (G → k) where
toFun s := {
toFun f t := f (s⁻¹ * t)
map_add' _ _ := rfl
map_smul' _ _ := rfl
}
map_one' := by
ext
simp
map_mul' _ _ := by
ext
simp [mul_assoc]

variable [Fintype G]

variable (k G) in
/-- The right regular representation `rightRegular` on `G → k` as a `FDRep k G`. -/
def rightFDRep : FDRep k G := FDRep.of rightRegular

/-- Map sending `η : Aut (forget k G)` to its component at `rightFDRep k G` as a linear map. -/
def toRightFDRepComp (η : Aut (forget k G)) : (G → k) →ₗ[k] (G → k) :=
(η.hom.hom.app (rightFDRep k G)).hom

end definitions

variable [Fintype G]

lemma equivHom_inj [Nontrivial k] [DecidableEq G] : Function.Injective (equivHom k G) := by
rw [injective_iff_map_eq_one]
intro s h
apply_fun (fun x ↦ (toRightFDRepComp x) (single 1 1) 1) at h
change (single 1 1 : G → k) (1 * s) = (single 1 1 : G → k) 1 at h
simp_all [single_apply]

end FiniteGroup

end TannakaDuality