From 2fed255269edf9bdaf5f9cc2388e93100fb032c6 Mon Sep 17 00:00:00 2001
From: ybenmeur <180416181+ybenmeur@users.noreply.github.com>
Date: Fri, 21 Feb 2025 18:23:05 +0100
Subject: [PATCH 1/7] feat: Tannaka duality for finite groups

---
 Mathlib/RepresentationTheory/Tannaka.lean | 311 ++++++++++++++++++++++
 1 file changed, 311 insertions(+)
 create mode 100644 Mathlib/RepresentationTheory/Tannaka.lean

diff --git a/Mathlib/RepresentationTheory/Tannaka.lean b/Mathlib/RepresentationTheory/Tannaka.lean
new file mode 100644
index 0000000000000..6beb09f79b39a
--- /dev/null
+++ b/Mathlib/RepresentationTheory/Tannaka.lean
@@ -0,0 +1,311 @@
+/-
+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
+
+We prove **Tannaka duality** for finite groups, which states that a finite group `G`
+is characterized by `FDRep k G`, the category of finite dimensional `k`-linear
+representations of `G`, for any field `k`.
+
+## Notation
+
+- `F`   : monoidal forgetful functor `FDRep k G ⥤ FGModuleCat k`
+- `T`   : the morphism `G →* Aut (F k G)` shown to be an isomorphism
+- `τᵣ`  : right regular representation on `G → k`
+- `α`   : map sending a natural transformation `η : F ⟹ F` to its `τᵣ` component
+
+## Reference
+
+<https://math.leidenuniv.nl/scripties/1bachCommelin.pdf>
+-/
+
+noncomputable section
+
+open CategoryTheory MonoidalCategory ModuleCat Finset Pi
+
+universe u
+
+namespace TannakaDuality
+
+variable {k G : Type u} [Field 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 F := LaxMonoidalFunctor.of (forget₂ (FDRep k G) (FGModuleCat k))
+
+/-- Definition of `T g : Aut (F k G)` by its components -/
+def T_app (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]
+
+/-- The function defining `T` -/
+def T_fun (g : G) : Aut (F k G) :=
+  LaxMonoidalFunctor.isoOfComponents (T_app g) (fun f ↦ (f.comm g).symm) rfl (by intros; rfl)
+
+@[simp]
+lemma T_apply (g : G) (X : FDRep k G) : ((T_fun g).hom.hom.app X).hom = X.ρ g := rfl
+
+variable (k G) in
+/-- The group homomorphism `G →* Aut (F k G)` involved in the main theorem -/
+def T : G →* Aut (F k G) where
+  toFun := T_fun
+  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 τᵣ : 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 τₗ : 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 representation `τᵣ` on `G → k` induced by multiplication on
+the right in `G` as a `FDRep k G` -/
+def fdRepτᵣ : FDRep k G := FDRep.of τᵣ
+
+/-- Map sending `η : Aut (F k G)` to its component at `fdRepτᵣ k G` as a linear map -/
+def α (η : Aut (F k G)) : (G → k) →ₗ[k] (G → k) := (η.hom.hom.app (fdRepτᵣ k G)).hom
+
+end definitions
+
+variable [Fintype G]
+
+section lemma4
+
+-- *lemma 4.4*
+lemma T_injective [DecidableEq G] : Function.Injective (T k G) := by
+  rw [injective_iff_map_eq_one]
+  intro s h
+  apply_fun α at h
+  apply_fun (· (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 lemma4
+
+section lemma5
+
+-- *lemma 4.5*
+/-- An algebra morphism `φ : (G → k) →ₐ[k] k` is an evaluation map. -/
+lemma eval_of_alghom {G : Type u} [DecidableEq G] [Fintype G] (φ : (G → k) →ₐ[k] k) :
+    ∃ (s : G), φ = evalAlgHom _ _ s := by
+  have h1 := map_one φ
+  rw [← univ_sum_single (1 : G → k), map_sum] at h1
+  obtain ⟨s, hs⟩ : ∃ (s : G), φ (single s 1) ≠ 0 := by
+    by_contra
+    simp_all
+  have h2 : ∀ t ≠ s, φ (single t 1) = 0 := by
+    intros
+    apply eq_zero_of_ne_zero_of_mul_right_eq_zero hs
+    rw [← map_mul]
+    convert map_zero φ
+    ext u
+    by_cases u = s <;> simp_all
+  have h3 : φ (single s 1) = 1 := by
+    rwa [Fintype.sum_eq_single s] at h1
+    exact h2
+  use s
+  apply AlgHom.toLinearMap_injective
+  apply Basis.ext (basisFun k G)
+  intro t
+  by_cases t = s <;> simp_all
+
+end lemma5
+
+section lemma6
+
+/-- The `FDRep k G` morphism induced by multiplication on `G → k`. -/
+def μ : fdRepτᵣ k G ⊗ fdRepτᵣ k G ⟶ fdRepτᵣ k G where
+  hom := ofHom (LinearMap.mul' k (G → k))
+  comm := by
+    intro
+    ext (u : TensorProduct k (G → k) (G → k))
+    refine TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) ?_
+    intro _ _ hx hy
+    simp only [map_add, hx, hy]
+
+/-- For `η : Aut (F k G)`, `α η` is compatible with multiplication -/
+lemma map_mul_α (η : Aut (F k G)) : ∀ (x y : G → k), (α η) (x * y) = ((α η) x) * ((α η) y) := by
+  intro f g
+  have nat := η.hom.hom.naturality μ
+  have tensor := η.hom.isMonoidal.tensor
+  have F_μ {X Y} : Functor.LaxMonoidal.μ (F k G).toFunctor X Y = 𝟙 _ := rfl
+  simp only [F_μ, Category.id_comp, Category.comp_id] at tensor
+  rw [tensor] at nat
+  apply_fun Hom.hom at nat
+  apply_fun (· (f ⊗ₜ[k] g)) at nat
+  exact nat
+
+-- *lemma 4.6*
+/-- For `η : Aut (F k G)`, `α η` is an algebra morphism -/
+def algHomOfα (η : Aut (F k G)) : ((G → k)) →ₐ[k] ((G → k)) := by
+  refine AlgHom.ofLinearMap (α η) ?_ (map_mul_α η)
+  let α_inv : (G → k) → (G → k) := (η.inv.hom.app (fdRepτᵣ k G)).hom
+  have := η.inv_hom_id
+  apply_fun NatTrans.app ∘ LaxMonoidalFunctor.Hom.hom at this
+  replace := congrFun this (fdRepτᵣ k G)
+  apply_fun (Hom.hom · (1 : G → k)) at this
+  change (α η) (α_inv 1) = (1 : G → k) at this
+  have h := this
+  rwa [← one_mul (α_inv 1), map_mul_α, h, mul_one] at this
+
+end lemma6
+
+variable [DecidableEq G]
+
+section lemma7
+
+/-- `τₗ` commutes with `τᵣ`, so it is a representation morphism of `fdRepτᵣ` -/
+def τₗfdRepHom (s : G) : (fdRepτᵣ k G) ⟶ (fdRepτᵣ k G) where
+  hom := ofHom (τₗ s)
+  comm := by
+    intro (t : G)
+    ext (f : G → k)
+    funext u
+    change (τₗ s) ((τᵣ t) f) u = (τᵣ t) ((τₗ s) f) u
+    simp [mul_assoc]
+
+-- *lemma 4.7*
+lemma image_α_in_image_τᵣ (η : Aut (F k G)) : ∃ (s : G), α η = τᵣ s := by
+  obtain ⟨s, hs⟩ := eval_of_alghom ((evalAlgHom _ _ 1).comp (algHomOfα η))
+  use s
+  apply Basis.ext (basisFun k G)
+  intro u
+  ext t
+  have hnat := η.hom.hom.naturality (τₗfdRepHom t⁻¹)
+  apply_fun Hom.hom at hnat
+  calc
+    _ = τₗ t⁻¹ (α η (single u 1)) 1 := by simp
+    _ = α η (τₗ t⁻¹ (single u 1)) 1 :=
+      congrFun (congrFun (congrArg DFunLike.coe hnat) (single u 1)).symm 1
+    _ = evalAlgHom _ _ s (τₗ t⁻¹ (single u 1)) :=
+      congrFun (congrArg DFunLike.coe hs) ((τₗ t⁻¹) (single u 1))
+    _ = _ := by
+      by_cases u = t * s <;> simp_all [single_apply]
+
+end lemma7
+
+section lemma8
+
+/-- Auxiliary map for the proof of `α_injective` -/
+@[simps]
+def φ {X : FDRep k G} (v : X) : (G → k) →ₗ[k] X where
+  toFun f := ∑ s : G, (f s) • (X.ρ s⁻¹ v)
+  map_add' _ _ := by
+    simp only [add_apply, add_smul]
+    exact sum_add_distrib
+  map_smul' _ _ := by
+    simp only [smul_apply, smul_eq_mul, RingHom.id_apply, smul_sum, smul_smul]
+
+lemma φ_e_one_eq_id {X : FDRep k G} (v : X) : (φ v) (single 1 1) = v := by
+  rw [φ_apply]
+  let a := fun s ↦ (single 1 1 : G → k) s • (X.ρ s⁻¹) v
+  calc
+    _ = (∑ s ∈ {1}ᶜ, a s) + a 1 :=
+      Fintype.sum_eq_sum_compl_add 1 a
+    _ = a 1 := by
+      apply add_left_eq_self.mpr
+      apply sum_eq_zero
+      simp_all [a]
+    _ = _ := by
+      simp [a]
+
+/-- Auxiliary representation morphism for the proof of `α_injective` -/
+@[simps]
+def φRepMor (X : FDRep k G) (v : X) : (fdRepτᵣ k G) ⟶ X where
+  hom := ofHom (φ v)
+  comm := by
+    intro (t : G)
+    ext (f : G → k)
+    change (φ v) (τᵣ t f) = X.ρ t (φ v f)
+    simp only [φ_apply, map_sum]
+    set φ_term := fun (X : FDRep k G) (f : G → k) v s ↦ (f s) • (X.ρ s⁻¹ v)
+    have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (τᵣ t f) v)
+    simp only [φ_term, univ_map_embedding] at this
+    rw [this]
+    apply sum_congr rfl
+    simp
+
+-- *lemma 4.8*
+/-- If `η₁ η₂ : Aut (F k G)` agree on `fdRepτᵣ` then they are equal -/
+lemma α_injective (η₁ η₂ : Aut (F k G)) (h : α η₁ = α η₂) : η₁ = η₂ := by
+  ext X v
+  have h1 := η₁.hom.hom.naturality (φRepMor X v)
+  have h2 := η₂.hom.hom.naturality (φRepMor X v)
+  rw [hom_ext h, ← h2] at h1
+  apply_fun Hom.hom at h1
+  apply_fun (· (single 1 1)) at h1
+  change Hom.hom _ ((φ v) _) = Hom.hom _ ((φ v) _) at h1
+  rw [φ_e_one_eq_id] at h1
+  exact h1
+
+end lemma8
+
+section prop11
+
+-- *proposition 4.11*
+lemma T_surjective : Function.Surjective (T k G) := by
+  intro η
+  obtain ⟨s, h⟩ := image_α_in_image_τᵣ η
+  use s
+  apply α_injective
+  exact h.symm
+
+end prop11
+
+section thm
+
+-- *theorem 4.3*
+theorem tannaka_duality : Function.Bijective (T k G) :=
+  ⟨T_injective, T_surjective⟩
+
+example : G ≃* Aut (F k G) :=
+  MulEquiv.ofBijective (T k G) tannaka_duality
+
+end thm
+
+end TannakaDuality

From 3f053214dcce0e51e1fc32c4342801729a60eda2 Mon Sep 17 00:00:00 2001
From: ybenmeur <180416181+ybenmeur@users.noreply.github.com>
Date: Fri, 21 Feb 2025 19:56:35 +0100
Subject: [PATCH 2/7] first part

---
 Mathlib/RepresentationTheory/Tannaka.lean | 222 ++--------------------
 1 file changed, 11 insertions(+), 211 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Tannaka.lean b/Mathlib/RepresentationTheory/Tannaka.lean
index 6beb09f79b39a..01f4da7848725 100644
--- a/Mathlib/RepresentationTheory/Tannaka.lean
+++ b/Mathlib/RepresentationTheory/Tannaka.lean
@@ -8,16 +8,18 @@ import Mathlib.RepresentationTheory.FDRep
 /-!
 # Tannaka duality for finite groups
 
-We prove **Tannaka duality** for finite groups, which states that a finite group `G`
-is characterized by `FDRep k G`, the category of finite dimensional `k`-linear
-representations of `G`, for any field `k`.
+In this file we prove Tannaka duality for finite groups.
+
+The theorem can be formulated as follows: for any field `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 `F : FDRep k G ⥤ FGModuleCat k`.
 
 ## Notation
 
-- `F`   : monoidal forgetful functor `FDRep k G ⥤ FGModuleCat k`
+- `F`   : the monoidal forgetful functor `FDRep k G ⥤ FGModuleCat k`
 - `T`   : the morphism `G →* Aut (F k G)` shown to be an isomorphism
-- `τᵣ`  : right regular representation on `G → k`
-- `α`   : map sending a natural transformation `η : F ⟹ F` to its `τᵣ` component
+- `τᵣ`  : the right regular representation on `G → k`
+- `α`   : the map sending a monoidal natural isomorphism `η : Aut (F k G)` to its `τᵣ` component
 
 ## Reference
 
@@ -26,7 +28,7 @@ representations of `G`, for any field `k`.
 
 noncomputable section
 
-open CategoryTheory MonoidalCategory ModuleCat Finset Pi
+open CategoryTheory ModuleCat Pi
 
 universe u
 
@@ -64,7 +66,7 @@ def T_fun (g : G) : Aut (F k G) :=
 lemma T_apply (g : G) (X : FDRep k G) : ((T_fun g).hom.hom.app X).hom = X.ρ g := rfl
 
 variable (k G) in
-/-- The group homomorphism `G →* Aut (F k G)` involved in the main theorem -/
+/-- The group homomorphism `G →* Aut (F k G)` shown to be bijective -/
 def T : G →* Aut (F k G) where
   toFun := T_fun
   map_one' := by ext; simp; rfl
@@ -85,26 +87,10 @@ def τᵣ : Representation k G (G → k) where
     ext
     simp [mul_assoc]
 
-/-- The representation on `G → k` induced by multiplication on the left in `G` -/
-@[simps]
-def τₗ : 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 representation `τᵣ` on `G → k` induced by multiplication on
-the right in `G` as a `FDRep k G` -/
+/-- The right regular representation `τᵣ` on `G → k` as a `FDRep k G` -/
 def fdRepτᵣ : FDRep k G := FDRep.of τᵣ
 
 /-- Map sending `η : Aut (F k G)` to its component at `fdRepτᵣ k G` as a linear map -/
@@ -114,9 +100,6 @@ end definitions
 
 variable [Fintype G]
 
-section lemma4
-
--- *lemma 4.4*
 lemma T_injective [DecidableEq G] : Function.Injective (T k G) := by
   rw [injective_iff_map_eq_one]
   intro s h
@@ -125,187 +108,4 @@ lemma T_injective [DecidableEq G] : Function.Injective (T k G) := by
   change (single 1 1 : G → k) (1 * s) = (single 1 1 : G → k) 1 at h
   simp_all [single_apply]
 
-end lemma4
-
-section lemma5
-
--- *lemma 4.5*
-/-- An algebra morphism `φ : (G → k) →ₐ[k] k` is an evaluation map. -/
-lemma eval_of_alghom {G : Type u} [DecidableEq G] [Fintype G] (φ : (G → k) →ₐ[k] k) :
-    ∃ (s : G), φ = evalAlgHom _ _ s := by
-  have h1 := map_one φ
-  rw [← univ_sum_single (1 : G → k), map_sum] at h1
-  obtain ⟨s, hs⟩ : ∃ (s : G), φ (single s 1) ≠ 0 := by
-    by_contra
-    simp_all
-  have h2 : ∀ t ≠ s, φ (single t 1) = 0 := by
-    intros
-    apply eq_zero_of_ne_zero_of_mul_right_eq_zero hs
-    rw [← map_mul]
-    convert map_zero φ
-    ext u
-    by_cases u = s <;> simp_all
-  have h3 : φ (single s 1) = 1 := by
-    rwa [Fintype.sum_eq_single s] at h1
-    exact h2
-  use s
-  apply AlgHom.toLinearMap_injective
-  apply Basis.ext (basisFun k G)
-  intro t
-  by_cases t = s <;> simp_all
-
-end lemma5
-
-section lemma6
-
-/-- The `FDRep k G` morphism induced by multiplication on `G → k`. -/
-def μ : fdRepτᵣ k G ⊗ fdRepτᵣ k G ⟶ fdRepτᵣ k G where
-  hom := ofHom (LinearMap.mul' k (G → k))
-  comm := by
-    intro
-    ext (u : TensorProduct k (G → k) (G → k))
-    refine TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) ?_
-    intro _ _ hx hy
-    simp only [map_add, hx, hy]
-
-/-- For `η : Aut (F k G)`, `α η` is compatible with multiplication -/
-lemma map_mul_α (η : Aut (F k G)) : ∀ (x y : G → k), (α η) (x * y) = ((α η) x) * ((α η) y) := by
-  intro f g
-  have nat := η.hom.hom.naturality μ
-  have tensor := η.hom.isMonoidal.tensor
-  have F_μ {X Y} : Functor.LaxMonoidal.μ (F k G).toFunctor X Y = 𝟙 _ := rfl
-  simp only [F_μ, Category.id_comp, Category.comp_id] at tensor
-  rw [tensor] at nat
-  apply_fun Hom.hom at nat
-  apply_fun (· (f ⊗ₜ[k] g)) at nat
-  exact nat
-
--- *lemma 4.6*
-/-- For `η : Aut (F k G)`, `α η` is an algebra morphism -/
-def algHomOfα (η : Aut (F k G)) : ((G → k)) →ₐ[k] ((G → k)) := by
-  refine AlgHom.ofLinearMap (α η) ?_ (map_mul_α η)
-  let α_inv : (G → k) → (G → k) := (η.inv.hom.app (fdRepτᵣ k G)).hom
-  have := η.inv_hom_id
-  apply_fun NatTrans.app ∘ LaxMonoidalFunctor.Hom.hom at this
-  replace := congrFun this (fdRepτᵣ k G)
-  apply_fun (Hom.hom · (1 : G → k)) at this
-  change (α η) (α_inv 1) = (1 : G → k) at this
-  have h := this
-  rwa [← one_mul (α_inv 1), map_mul_α, h, mul_one] at this
-
-end lemma6
-
-variable [DecidableEq G]
-
-section lemma7
-
-/-- `τₗ` commutes with `τᵣ`, so it is a representation morphism of `fdRepτᵣ` -/
-def τₗfdRepHom (s : G) : (fdRepτᵣ k G) ⟶ (fdRepτᵣ k G) where
-  hom := ofHom (τₗ s)
-  comm := by
-    intro (t : G)
-    ext (f : G → k)
-    funext u
-    change (τₗ s) ((τᵣ t) f) u = (τᵣ t) ((τₗ s) f) u
-    simp [mul_assoc]
-
--- *lemma 4.7*
-lemma image_α_in_image_τᵣ (η : Aut (F k G)) : ∃ (s : G), α η = τᵣ s := by
-  obtain ⟨s, hs⟩ := eval_of_alghom ((evalAlgHom _ _ 1).comp (algHomOfα η))
-  use s
-  apply Basis.ext (basisFun k G)
-  intro u
-  ext t
-  have hnat := η.hom.hom.naturality (τₗfdRepHom t⁻¹)
-  apply_fun Hom.hom at hnat
-  calc
-    _ = τₗ t⁻¹ (α η (single u 1)) 1 := by simp
-    _ = α η (τₗ t⁻¹ (single u 1)) 1 :=
-      congrFun (congrFun (congrArg DFunLike.coe hnat) (single u 1)).symm 1
-    _ = evalAlgHom _ _ s (τₗ t⁻¹ (single u 1)) :=
-      congrFun (congrArg DFunLike.coe hs) ((τₗ t⁻¹) (single u 1))
-    _ = _ := by
-      by_cases u = t * s <;> simp_all [single_apply]
-
-end lemma7
-
-section lemma8
-
-/-- Auxiliary map for the proof of `α_injective` -/
-@[simps]
-def φ {X : FDRep k G} (v : X) : (G → k) →ₗ[k] X where
-  toFun f := ∑ s : G, (f s) • (X.ρ s⁻¹ v)
-  map_add' _ _ := by
-    simp only [add_apply, add_smul]
-    exact sum_add_distrib
-  map_smul' _ _ := by
-    simp only [smul_apply, smul_eq_mul, RingHom.id_apply, smul_sum, smul_smul]
-
-lemma φ_e_one_eq_id {X : FDRep k G} (v : X) : (φ v) (single 1 1) = v := by
-  rw [φ_apply]
-  let a := fun s ↦ (single 1 1 : G → k) s • (X.ρ s⁻¹) v
-  calc
-    _ = (∑ s ∈ {1}ᶜ, a s) + a 1 :=
-      Fintype.sum_eq_sum_compl_add 1 a
-    _ = a 1 := by
-      apply add_left_eq_self.mpr
-      apply sum_eq_zero
-      simp_all [a]
-    _ = _ := by
-      simp [a]
-
-/-- Auxiliary representation morphism for the proof of `α_injective` -/
-@[simps]
-def φRepMor (X : FDRep k G) (v : X) : (fdRepτᵣ k G) ⟶ X where
-  hom := ofHom (φ v)
-  comm := by
-    intro (t : G)
-    ext (f : G → k)
-    change (φ v) (τᵣ t f) = X.ρ t (φ v f)
-    simp only [φ_apply, map_sum]
-    set φ_term := fun (X : FDRep k G) (f : G → k) v s ↦ (f s) • (X.ρ s⁻¹ v)
-    have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (τᵣ t f) v)
-    simp only [φ_term, univ_map_embedding] at this
-    rw [this]
-    apply sum_congr rfl
-    simp
-
--- *lemma 4.8*
-/-- If `η₁ η₂ : Aut (F k G)` agree on `fdRepτᵣ` then they are equal -/
-lemma α_injective (η₁ η₂ : Aut (F k G)) (h : α η₁ = α η₂) : η₁ = η₂ := by
-  ext X v
-  have h1 := η₁.hom.hom.naturality (φRepMor X v)
-  have h2 := η₂.hom.hom.naturality (φRepMor X v)
-  rw [hom_ext h, ← h2] at h1
-  apply_fun Hom.hom at h1
-  apply_fun (· (single 1 1)) at h1
-  change Hom.hom _ ((φ v) _) = Hom.hom _ ((φ v) _) at h1
-  rw [φ_e_one_eq_id] at h1
-  exact h1
-
-end lemma8
-
-section prop11
-
--- *proposition 4.11*
-lemma T_surjective : Function.Surjective (T k G) := by
-  intro η
-  obtain ⟨s, h⟩ := image_α_in_image_τᵣ η
-  use s
-  apply α_injective
-  exact h.symm
-
-end prop11
-
-section thm
-
--- *theorem 4.3*
-theorem tannaka_duality : Function.Bijective (T k G) :=
-  ⟨T_injective, T_surjective⟩
-
-example : G ≃* Aut (F k G) :=
-  MulEquiv.ofBijective (T k G) tannaka_duality
-
-end thm
-
 end TannakaDuality

From 1a057b3c709cdf4c5b15806b99b60bcfe6f27d1d Mon Sep 17 00:00:00 2001
From: ybenmeur <180416181+ybenmeur@users.noreply.github.com>
Date: Fri, 21 Feb 2025 20:20:23 +0100
Subject: [PATCH 3/7] fix CI error

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index cef77a892d711..20242001d4ab1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -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

From 80e393c411aa77a5ccd2a3fc8c14f16e4e106d4b Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Mon, 24 Feb 2025 10:24:39 +0100
Subject: [PATCH 4/7] generalize most of the file to commrings

---
 Mathlib/RepresentationTheory/FDRep.lean | 73 +++++++++++++------------
 1 file changed, 38 insertions(+), 35 deletions(-)

diff --git a/Mathlib/RepresentationTheory/FDRep.lean b/Mathlib/RepresentationTheory/FDRep.lean
index 5c30b1048a148..24304a5306ee7 100644
--- a/Mathlib/RepresentationTheory/FDRep.lean
+++ b/Mathlib/RepresentationTheory/FDRep.lean
@@ -45,32 +45,35 @@ 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) :=
@@ -78,52 +81,52 @@ instance (V W : FDRep k G) : FiniteDimensional k (V ⟶ W) :=
     (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
 
@@ -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
 

From bda74f141d1f6c0a91dac88b3cd5dc07ffbf3539 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Mon, 24 Feb 2025 10:24:47 +0100
Subject: [PATCH 5/7] generalize to domains

---
 Mathlib/RepresentationTheory/Tannaka.lean | 154 +++++++++++++++++++++-
 1 file changed, 152 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Tannaka.lean b/Mathlib/RepresentationTheory/Tannaka.lean
index 01f4da7848725..fbaf450bbd0da 100644
--- a/Mathlib/RepresentationTheory/Tannaka.lean
+++ b/Mathlib/RepresentationTheory/Tannaka.lean
@@ -34,7 +34,7 @@ universe u
 
 namespace TannakaDuality
 
-variable {k G : Type u} [Field k] [Group G]
+variable {k G : Type u} [CommRing k] [Group G]
 
 section definitions
 
@@ -100,7 +100,7 @@ end definitions
 
 variable [Fintype G]
 
-lemma T_injective [DecidableEq G] : Function.Injective (T k G) := by
+lemma T_injective [Nontrivial k] [DecidableEq G] : Function.Injective (T k G) := by
   rw [injective_iff_map_eq_one]
   intro s h
   apply_fun α at h
@@ -108,4 +108,154 @@ lemma T_injective [DecidableEq G] : Function.Injective (T k G) := by
   change (single 1 1 : G → k) (1 * s) = (single 1 1 : G → k) 1 at h
   simp_all [single_apply]
 
+/-- An algebra morphism `φ : (G → k) →ₐ[k] k` is an evaluation map. -/
+lemma eval_of_alghom [IsDomain k] {G : Type u} [DecidableEq G] [Fintype G] (φ : (G → k) →ₐ[k] k) :
+    ∃ (s : G), φ = evalAlgHom _ _ s := by
+  have h1 := map_one φ
+  rw [← univ_sum_single (1 : G → k), map_sum] at h1
+  obtain ⟨s, hs⟩ : ∃ (s : G), φ (single s 1) ≠ 0 := by
+    by_contra
+    simp_all
+  have h2 : ∀ t ≠ s, φ (single t 1) = 0 := by
+    intros
+    apply eq_zero_of_ne_zero_of_mul_right_eq_zero hs
+    rw [← map_mul]
+    convert map_zero φ
+    ext u
+    by_cases u = s <;> simp_all
+  have h3 : φ (single s 1) = 1 := by
+    rwa [Fintype.sum_eq_single s] at h1
+    exact h2
+  use s
+  apply AlgHom.toLinearMap_injective
+  apply Basis.ext (basisFun k G)
+  intro t
+  by_cases t = s <;> simp_all
+
+/-- The `FDRep k G` morphism induced by multiplication on `G → k`. -/
+def μ : fdRepτᵣ k G ⊗ fdRepτᵣ k G ⟶ fdRepτᵣ k G where
+  hom := ofHom (LinearMap.mul' k (G → k))
+  comm := by
+    intro
+    ext (u : TensorProduct k (G → k) (G → k))
+    refine TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) ?_
+    intro _ _ hx hy
+    simp only [map_add, hx, hy]
+
+/-- For `η : Aut (F k G)`, `α η` is compatible with multiplication -/
+lemma map_mul_α (η : Aut (F k G)) : ∀ (x y : G → k), (α η) (x * y) = ((α η) x) * ((α η) y) := by
+  intro f g
+  have nat := η.hom.hom.naturality μ
+  have tensor := η.hom.isMonoidal.tensor
+  have F_μ {X Y} : Functor.LaxMonoidal.μ (F k G).toFunctor X Y = 𝟙 _ := rfl
+  simp only [F_μ, Category.id_comp, Category.comp_id] at tensor
+  rw [tensor] at nat
+  apply_fun Hom.hom at nat
+  apply_fun (· (f ⊗ₜ[k] g)) at nat
+  exact nat
+
+/-- For `η : Aut (F k G)`, `α η` gives rise to an algebra morphism `(G → k) →ₐ[k] (G → k)` -/
+def algHomOfα (η : Aut (F k G)) : (G → k) →ₐ[k] (G → k) := by
+  refine AlgHom.ofLinearMap (α η) ?_ (map_mul_α η)
+  let α_inv : (G → k) → (G → k) := (η.inv.hom.app (fdRepτᵣ k G)).hom
+  have := η.inv_hom_id
+  apply_fun NatTrans.app ∘ LaxMonoidalFunctor.Hom.hom at this
+  replace := congrFun this (fdRepτᵣ k G)
+  apply_fun (Hom.hom · (1 : G → k)) at this
+  change (α η) (α_inv 1) = (1 : G → k) at this
+  have h := this
+  rwa [← one_mul (α_inv 1), map_mul_α, h, mul_one] at this
+
+variable [DecidableEq G]
+
+/-- `τₗ` as a morphism `fdRepτᵣ k G ⟶ fdRepτᵣ k G` in `FDRep k G` -/
+def τₗFDRepHom (s : G) : fdRepτᵣ k G ⟶ fdRepτᵣ k G where
+  hom := ofHom (τₗ s)
+  comm := by
+    intro (t : G)
+    ext (f : G → k)
+    funext u
+    change (τₗ s) ((τᵣ t) f) u = (τᵣ t) ((τₗ s) f) u
+    simp [mul_assoc]
+
+lemma image_α_in_image_τᵣ [IsDomain k] (η : Aut (F k G)) : ∃ (s : G), α η = τᵣ s := by
+  obtain ⟨s, hs⟩ := eval_of_alghom ((evalAlgHom _ _ 1).comp (algHomOfα η))
+  use s
+  apply Basis.ext (basisFun k G)
+  intro u
+  ext t
+  have hnat := η.hom.hom.naturality (τₗFDRepHom t⁻¹)
+  apply_fun Hom.hom at hnat
+  calc
+    _ = τₗ t⁻¹ (α η (single u 1)) 1 := by simp
+    _ = α η (τₗ t⁻¹ (single u 1)) 1 :=
+      congrFun (congrFun (congrArg DFunLike.coe hnat) (single u 1)).symm 1
+    _ = evalAlgHom _ _ s (τₗ t⁻¹ (single u 1)) :=
+      congrFun (congrArg DFunLike.coe hs) ((τₗ t⁻¹) (single u 1))
+    _ = _ := by
+      by_cases u = t * s <;> simp_all [single_apply]
+
+/-- Auxiliary map for the proof of `α_injective` -/
+@[simps]
+def φ {X : FDRep k G} (v : X) : (G → k) →ₗ[k] X where
+  toFun f := ∑ s : G, (f s) • (X.ρ s⁻¹ v)
+  map_add' _ _ := by
+    simp only [add_apply, add_smul]
+    exact sum_add_distrib
+  map_smul' _ _ := by
+    simp only [smul_apply, smul_eq_mul, RingHom.id_apply, smul_sum, smul_smul]
+
+lemma φ_e_one_eq_id {X : FDRep k G} (v : X) : (φ v) (single 1 1) = v := by
+  rw [φ_apply]
+  let a := fun s ↦ (single 1 1 : G → k) s • (X.ρ s⁻¹) v
+  calc
+    _ = (∑ s ∈ {1}ᶜ, a s) + a 1 :=
+      Fintype.sum_eq_sum_compl_add 1 a
+    _ = a 1 := by
+      apply add_left_eq_self.mpr
+      apply sum_eq_zero
+      simp_all [a]
+    _ = _ := by
+      simp [a]
+
+/-- Auxiliary representation morphism for the proof of `α_injective` -/
+@[simps]
+def φFDRepHom (X : FDRep k G) (v : X) : (fdRepτᵣ k G) ⟶ X where
+  hom := ofHom (φ v)
+  comm := by
+    intro (t : G)
+    ext (f : G → k)
+    change (φ v) (τᵣ t f) = X.ρ t (φ v f)
+    simp only [φ_apply, map_sum]
+    set φ_term := fun (X : FDRep k G) (f : G → k) v s ↦ (f s) • (X.ρ s⁻¹ v)
+    have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (τᵣ t f) v)
+    simp only [φ_term, univ_map_embedding] at this
+    rw [this]
+    apply sum_congr rfl
+    simp
+
+lemma α_injective (η₁ η₂ : Aut (F k G)) (h : α η₁ = α η₂) : η₁ = η₂ := by
+  ext X v
+  have h1 := η₁.hom.hom.naturality (φFDRepHom X v)
+  have h2 := η₂.hom.hom.naturality (φFDRepHom X v)
+  rw [hom_ext h, ← h2] at h1
+  apply_fun Hom.hom at h1
+  apply_fun (· (single 1 1)) at h1
+  change Hom.hom _ ((φ v) _) = Hom.hom _ ((φ v) _) at h1
+  rw [φ_e_one_eq_id] at h1
+  exact h1
+
+lemma T_surjective [IsDomain k] : Function.Surjective (T k G) := by
+  intro η
+  obtain ⟨s, h⟩ := image_α_in_image_τᵣ η
+  use s
+  apply α_injective
+  exact h.symm
+
+theorem tannaka_duality [IsDomain k] : Function.Bijective (T k G) :=
+  ⟨T_injective, T_surjective⟩
+
+variable (k G) in
+def equiv [IsDomain k] : G ≃* Aut (F k G) := MulEquiv.ofBijective (T k G) tannaka_duality
+
 end TannakaDuality

From 21cc95f1b586cd68a96f11a8fd4497f26757a57d Mon Sep 17 00:00:00 2001
From: ybenmeur <180416181+ybenmeur@users.noreply.github.com>
Date: Mon, 24 Feb 2025 20:46:06 +0100
Subject: [PATCH 6/7] update from #22176

---
 Mathlib/RepresentationTheory/Tannaka.lean | 222 ++++------------------
 1 file changed, 41 insertions(+), 181 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Tannaka.lean b/Mathlib/RepresentationTheory/Tannaka.lean
index fbaf450bbd0da..e191d8969855a 100644
--- a/Mathlib/RepresentationTheory/Tannaka.lean
+++ b/Mathlib/RepresentationTheory/Tannaka.lean
@@ -10,16 +10,11 @@ import Mathlib.RepresentationTheory.FDRep
 
 In this file we prove Tannaka duality for finite groups.
 
-The theorem can be formulated as follows: for any field `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 `F : FDRep k G ⥤ FGModuleCat k`.
+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`.
 
-## Notation
-
-- `F`   : the monoidal forgetful functor `FDRep k G ⥤ FGModuleCat k`
-- `T`   : the morphism `G →* Aut (F k G)` shown to be an isomorphism
-- `τᵣ`  : the right regular representation on `G → k`
-- `α`   : the map sending a monoidal natural isomorphism `η : Aut (F k G)` to its `τᵣ` component
+More specifically, the main result is the isomorphism `equiv : G ≃* Aut (forget k G)`.
 
 ## Reference
 
@@ -28,12 +23,14 @@ and the monoidal forgetful functor `F : FDRep k G ⥤ FGModuleCat k`.
 
 noncomputable section
 
-open CategoryTheory ModuleCat Pi
+open CategoryTheory MonoidalCategory ModuleCat Finset Pi
 
 universe u
 
 namespace TannakaDuality
 
+namespace FiniteGroup
+
 variable {k G : Type u} [CommRing k] [Group G]
 
 section definitions
@@ -42,11 +39,12 @@ 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 F := LaxMonoidalFunctor.of (forget₂ (FDRep k G) (FGModuleCat k))
+/-- The monoidal forgetful functor from `FDRep k G` to `FGModuleCat k`. -/
+def forget := LaxMonoidalFunctor.of (forget₂ (FDRep k G) (FGModuleCat k))
 
-/-- Definition of `T g : Aut (F k G)` by its components -/
-def T_app (g : G) (X : FDRep k G) : X.V ≅ X.V where
+/-- 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
@@ -58,23 +56,17 @@ def T_app (g : G) (X : FDRep k G) : X.V ≅ X.V where
     change (X.ρ g * X.ρ g⁻¹) x = x
     simp [← map_mul]
 
-/-- The function defining `T` -/
-def T_fun (g : G) : Aut (F k G) :=
-  LaxMonoidalFunctor.isoOfComponents (T_app g) (fun f ↦ (f.comm g).symm) rfl (by intros; rfl)
-
-@[simp]
-lemma T_apply (g : G) (X : FDRep k G) : ((T_fun g).hom.hom.app X).hom = X.ρ g := rfl
-
 variable (k G) in
-/-- The group homomorphism `G →* Aut (F k G)` shown to be bijective -/
-def T : G →* Aut (F k G) where
-  toFun := T_fun
+/-- 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` -/
+/-- The representation on `G → k` induced by multiplication on the right in `G`. -/
 @[simps]
-def τᵣ : Representation k G (G → k) where
+def rightRegular : Representation k G (G → k) where
   toFun s := {
     toFun f t := f (t * s)
     map_add' _ _ := rfl
@@ -87,175 +79,43 @@ def τᵣ : Representation k G (G → k) where
     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 `τᵣ` on `G → k` as a `FDRep k G` -/
-def fdRepτᵣ : FDRep k G := FDRep.of τᵣ
+/-- The right regular representation `rightRegular` on `G → k` as a `FDRep k G`. -/
+def rightFDRep : FDRep k G := FDRep.of rightRegular
 
-/-- Map sending `η : Aut (F k G)` to its component at `fdRepτᵣ k G` as a linear map -/
-def α (η : Aut (F k G)) : (G → k) →ₗ[k] (G → k) := (η.hom.hom.app (fdRepτᵣ k G)).hom
+/-- 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 T_injective [Nontrivial k] [DecidableEq G] : Function.Injective (T k G) := by
+lemma equivHom_inj [Nontrivial k] [DecidableEq G] : Function.Injective (equivHom k G) := by
   rw [injective_iff_map_eq_one]
   intro s h
-  apply_fun α at h
+  apply_fun toRightFDRepComp at h
   apply_fun (· (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]
 
-/-- An algebra morphism `φ : (G → k) →ₐ[k] k` is an evaluation map. -/
-lemma eval_of_alghom [IsDomain k] {G : Type u} [DecidableEq G] [Fintype G] (φ : (G → k) →ₐ[k] k) :
-    ∃ (s : G), φ = evalAlgHom _ _ s := by
-  have h1 := map_one φ
-  rw [← univ_sum_single (1 : G → k), map_sum] at h1
-  obtain ⟨s, hs⟩ : ∃ (s : G), φ (single s 1) ≠ 0 := by
-    by_contra
-    simp_all
-  have h2 : ∀ t ≠ s, φ (single t 1) = 0 := by
-    intros
-    apply eq_zero_of_ne_zero_of_mul_right_eq_zero hs
-    rw [← map_mul]
-    convert map_zero φ
-    ext u
-    by_cases u = s <;> simp_all
-  have h3 : φ (single s 1) = 1 := by
-    rwa [Fintype.sum_eq_single s] at h1
-    exact h2
-  use s
-  apply AlgHom.toLinearMap_injective
-  apply Basis.ext (basisFun k G)
-  intro t
-  by_cases t = s <;> simp_all
-
-/-- The `FDRep k G` morphism induced by multiplication on `G → k`. -/
-def μ : fdRepτᵣ k G ⊗ fdRepτᵣ k G ⟶ fdRepτᵣ k G where
-  hom := ofHom (LinearMap.mul' k (G → k))
-  comm := by
-    intro
-    ext (u : TensorProduct k (G → k) (G → k))
-    refine TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) ?_
-    intro _ _ hx hy
-    simp only [map_add, hx, hy]
-
-/-- For `η : Aut (F k G)`, `α η` is compatible with multiplication -/
-lemma map_mul_α (η : Aut (F k G)) : ∀ (x y : G → k), (α η) (x * y) = ((α η) x) * ((α η) y) := by
-  intro f g
-  have nat := η.hom.hom.naturality μ
-  have tensor := η.hom.isMonoidal.tensor
-  have F_μ {X Y} : Functor.LaxMonoidal.μ (F k G).toFunctor X Y = 𝟙 _ := rfl
-  simp only [F_μ, Category.id_comp, Category.comp_id] at tensor
-  rw [tensor] at nat
-  apply_fun Hom.hom at nat
-  apply_fun (· (f ⊗ₜ[k] g)) at nat
-  exact nat
-
-/-- For `η : Aut (F k G)`, `α η` gives rise to an algebra morphism `(G → k) →ₐ[k] (G → k)` -/
-def algHomOfα (η : Aut (F k G)) : (G → k) →ₐ[k] (G → k) := by
-  refine AlgHom.ofLinearMap (α η) ?_ (map_mul_α η)
-  let α_inv : (G → k) → (G → k) := (η.inv.hom.app (fdRepτᵣ k G)).hom
-  have := η.inv_hom_id
-  apply_fun NatTrans.app ∘ LaxMonoidalFunctor.Hom.hom at this
-  replace := congrFun this (fdRepτᵣ k G)
-  apply_fun (Hom.hom · (1 : G → k)) at this
-  change (α η) (α_inv 1) = (1 : G → k) at this
-  have h := this
-  rwa [← one_mul (α_inv 1), map_mul_α, h, mul_one] at this
-
-variable [DecidableEq G]
-
-/-- `τₗ` as a morphism `fdRepτᵣ k G ⟶ fdRepτᵣ k G` in `FDRep k G` -/
-def τₗFDRepHom (s : G) : fdRepτᵣ k G ⟶ fdRepτᵣ k G where
-  hom := ofHom (τₗ s)
-  comm := by
-    intro (t : G)
-    ext (f : G → k)
-    funext u
-    change (τₗ s) ((τᵣ t) f) u = (τᵣ t) ((τₗ s) f) u
-    simp [mul_assoc]
-
-lemma image_α_in_image_τᵣ [IsDomain k] (η : Aut (F k G)) : ∃ (s : G), α η = τᵣ s := by
-  obtain ⟨s, hs⟩ := eval_of_alghom ((evalAlgHom _ _ 1).comp (algHomOfα η))
-  use s
-  apply Basis.ext (basisFun k G)
-  intro u
-  ext t
-  have hnat := η.hom.hom.naturality (τₗFDRepHom t⁻¹)
-  apply_fun Hom.hom at hnat
-  calc
-    _ = τₗ t⁻¹ (α η (single u 1)) 1 := by simp
-    _ = α η (τₗ t⁻¹ (single u 1)) 1 :=
-      congrFun (congrFun (congrArg DFunLike.coe hnat) (single u 1)).symm 1
-    _ = evalAlgHom _ _ s (τₗ t⁻¹ (single u 1)) :=
-      congrFun (congrArg DFunLike.coe hs) ((τₗ t⁻¹) (single u 1))
-    _ = _ := by
-      by_cases u = t * s <;> simp_all [single_apply]
-
-/-- Auxiliary map for the proof of `α_injective` -/
-@[simps]
-def φ {X : FDRep k G} (v : X) : (G → k) →ₗ[k] X where
-  toFun f := ∑ s : G, (f s) • (X.ρ s⁻¹ v)
-  map_add' _ _ := by
-    simp only [add_apply, add_smul]
-    exact sum_add_distrib
-  map_smul' _ _ := by
-    simp only [smul_apply, smul_eq_mul, RingHom.id_apply, smul_sum, smul_smul]
-
-lemma φ_e_one_eq_id {X : FDRep k G} (v : X) : (φ v) (single 1 1) = v := by
-  rw [φ_apply]
-  let a := fun s ↦ (single 1 1 : G → k) s • (X.ρ s⁻¹) v
-  calc
-    _ = (∑ s ∈ {1}ᶜ, a s) + a 1 :=
-      Fintype.sum_eq_sum_compl_add 1 a
-    _ = a 1 := by
-      apply add_left_eq_self.mpr
-      apply sum_eq_zero
-      simp_all [a]
-    _ = _ := by
-      simp [a]
-
-/-- Auxiliary representation morphism for the proof of `α_injective` -/
-@[simps]
-def φFDRepHom (X : FDRep k G) (v : X) : (fdRepτᵣ k G) ⟶ X where
-  hom := ofHom (φ v)
-  comm := by
-    intro (t : G)
-    ext (f : G → k)
-    change (φ v) (τᵣ t f) = X.ρ t (φ v f)
-    simp only [φ_apply, map_sum]
-    set φ_term := fun (X : FDRep k G) (f : G → k) v s ↦ (f s) • (X.ρ s⁻¹ v)
-    have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (τᵣ t f) v)
-    simp only [φ_term, univ_map_embedding] at this
-    rw [this]
-    apply sum_congr rfl
-    simp
-
-lemma α_injective (η₁ η₂ : Aut (F k G)) (h : α η₁ = α η₂) : η₁ = η₂ := by
-  ext X v
-  have h1 := η₁.hom.hom.naturality (φFDRepHom X v)
-  have h2 := η₂.hom.hom.naturality (φFDRepHom X v)
-  rw [hom_ext h, ← h2] at h1
-  apply_fun Hom.hom at h1
-  apply_fun (· (single 1 1)) at h1
-  change Hom.hom _ ((φ v) _) = Hom.hom _ ((φ v) _) at h1
-  rw [φ_e_one_eq_id] at h1
-  exact h1
-
-lemma T_surjective [IsDomain k] : Function.Surjective (T k G) := by
-  intro η
-  obtain ⟨s, h⟩ := image_α_in_image_τᵣ η
-  use s
-  apply α_injective
-  exact h.symm
-
-theorem tannaka_duality [IsDomain k] : Function.Bijective (T k G) :=
-  ⟨T_injective, T_surjective⟩
-
-variable (k G) in
-def equiv [IsDomain k] : G ≃* Aut (F k G) := MulEquiv.ofBijective (T k G) tannaka_duality
+end FiniteGroup
 
 end TannakaDuality

From 6db2a5832517955661a746055c32feab68293887 Mon Sep 17 00:00:00 2001
From: ybenmeur <180416181+ybenmeur@users.noreply.github.com>
Date: Tue, 25 Feb 2025 18:29:30 +0100
Subject: [PATCH 7/7] Update Mathlib/RepresentationTheory/Tannaka.lean

Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>
---
 Mathlib/RepresentationTheory/Tannaka.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Tannaka.lean b/Mathlib/RepresentationTheory/Tannaka.lean
index e191d8969855a..b9ef3fc3b5928 100644
--- a/Mathlib/RepresentationTheory/Tannaka.lean
+++ b/Mathlib/RepresentationTheory/Tannaka.lean
@@ -111,8 +111,7 @@ 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 toRightFDRepComp at h
-  apply_fun (· (single 1 1) 1) at 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]