From 4fd263babc93035783de6cac61043bd1b8ae715d Mon Sep 17 00:00:00 2001
From: antoinelab01 <antoinelab01@gmail.com>
Date: Fri, 24 Jun 2022 21:45:08 +0000
Subject: [PATCH] feat(representation_theory/character): characters of
 representations (#14453)

---
 src/algebra/category/FinVect.lean        | 23 ++++++++
 src/representation_theory/basic.lean     | 38 +++---------
 src/representation_theory/character.lean | 73 ++++++++++++++++++++++++
 src/representation_theory/fdRep.lean     | 48 +++++++++++++++-
 4 files changed, 151 insertions(+), 31 deletions(-)
 create mode 100644 src/representation_theory/character.lean

diff --git a/src/algebra/category/FinVect.lean b/src/algebra/category/FinVect.lean
index 9ad5f74d0422b..f78a110c0bf5d 100644
--- a/src/algebra/category/FinVect.lean
+++ b/src/algebra/category/FinVect.lean
@@ -108,4 +108,27 @@ instance right_dual : has_right_dual V := ⟨FinVect_dual K V⟩
 
 instance right_rigid_category : right_rigid_category (FinVect K) := { }
 
+variables {K V} (W : FinVect K)
+
+/-- Converts and isomorphism in the category `FinVect` to a `linear_equiv` between the underlying
+vector spaces. -/
+def iso_to_linear_equiv {V W : FinVect K} (i : V ≅ W) : V ≃ₗ[K] W :=
+  ((forget₂ (FinVect.{u} K) (Module.{u} K)).map_iso i).to_linear_equiv
+
+lemma iso.conj_eq_conj {V W : FinVect K} (i : V ≅ W) (f : End V) :
+  iso.conj i f = linear_equiv.conj (iso_to_linear_equiv i) f := rfl
+
 end FinVect
+
+variables {K}
+
+/-- Converts a `linear_equiv` to an isomorphism in the category `FinVect`. -/
+@[simps] def linear_equiv.to_FinVect_iso
+  {V W : Type u} [add_comm_group V] [module K V] [finite_dimensional K V]
+  [add_comm_group W] [module K W] [finite_dimensional K W]
+  (e : V ≃ₗ[K] W) :
+  FinVect.of K V ≅ FinVect.of K W :=
+{ hom := e.to_linear_map,
+  inv := e.symm.to_linear_map,
+  hom_inv_id' := by {ext, exact e.left_inv x},
+  inv_hom_id' := by {ext, exact e.right_inv x} }
diff --git a/src/representation_theory/basic.lean b/src/representation_theory/basic.lean
index 1ed9a58913776..d865818794286 100644
--- a/src/representation_theory/basic.lean
+++ b/src/representation_theory/basic.lean
@@ -109,33 +109,6 @@ by simp only [as_group_hom, monoid_hom.coe_to_hom_units]
 
 end group
 
-section character
-
-variables {k G V : Type*} [comm_ring k] [group G] [add_comm_group V] [module k V]
-variables (ρ : representation k G V)
-
-/--
-The character associated to a representation of `G`, which as a map `G → k`
-sends each element to the trace of the corresponding linear map.
--/
-@[simp]
-noncomputable def character (g : G) : k := trace k V (ρ g)
-
-theorem char_mul_comm (g : G) (h : G) : character ρ (h * g) = character ρ (g * h) :=
-by simp only [trace_mul_comm, character, map_mul]
-
-/-- The character of a representation is constant on conjugacy classes. -/
-theorem char_conj (g : G) (h : G) : (character ρ) (h * g * h⁻¹) = (character ρ) g :=
-by simp only [character, ←as_group_hom_apply, map_mul, map_inv, trace_conj]
-
-variables [nontrivial k] [module.free k V] [module.finite k V]
-
-/-- The evaluation of the character at the identity is the dimension of the representation. -/
-theorem char_one : character ρ 1 = finite_dimensional.finrank k V :=
-by simp only [character, map_one, trace_one]
-
-end character
-
 section tensor_product
 
 variables {k G V W : Type*} [comm_semiring k] [monoid G]
@@ -153,7 +126,7 @@ def tprod : representation k G (V ⊗[k] W) :=
   map_one' := by simp only [map_one, tensor_product.map_one],
   map_mul' := λ g h, by simp only [map_mul, tensor_product.map_mul] }
 
-notation ρV ` ⊗ ` ρW := tprod ρV ρW
+local notation ρV ` ⊗ ` ρW := tprod ρV ρW
 
 @[simp]
 lemma tprod_apply (g : G) : (ρV ⊗ ρW) g = tensor_product.map (ρV g) (ρW g) := rfl
@@ -199,7 +172,14 @@ def dual : representation k G (module.dual k V) :=
     by {ext, simp only [coe_comp, function.comp_app, mul_inv_rev, map_mul, coe_mk, mul_apply]}}
 
 @[simp]
-lemma dual_apply (g : G) (f : module.dual k V) : (dual ρV) g f = f ∘ₗ (ρV g⁻¹) := rfl
+lemma dual_apply (g : G) : (dual ρV) g = module.dual.transpose (ρV g⁻¹) := rfl
+
+lemma dual_tensor_hom_comm (g : G) :
+  (dual_tensor_hom k V W) ∘ₗ (tensor_product.map (ρV.dual g) (ρW g)) =
+  (lin_hom ρV ρW) g ∘ₗ (dual_tensor_hom k V W) :=
+begin
+  ext, simp [module.dual.transpose_apply],
+end
 
 end linear_hom
 
diff --git a/src/representation_theory/character.lean b/src/representation_theory/character.lean
new file mode 100644
index 0000000000000..85fee3c0243ce
--- /dev/null
+++ b/src/representation_theory/character.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2022 Antoine Labelle. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Labelle
+-/
+import representation_theory.fdRep
+import linear_algebra.trace
+import representation_theory.basic
+
+/-!
+# Characters of representations
+
+This file introduces characters of representation and proves basic lemmas about how characters
+behave under various operations on representations.
+
+# TODO
+* Once we have the monoidal closed structure on `fdRep k G` and a better API for the rigid
+structure, `char_dual` and `char_lin_hom` should probably be stated in terms of `Vᘁ` and `ihom V W`.
+-/
+
+noncomputable theory
+
+universes u
+
+open linear_map category_theory.monoidal_category representation
+
+variables {k G : Type u} [field k]
+
+namespace fdRep
+
+section monoid
+
+variables [monoid G]
+
+/-- The character of a representation `V : fdRep k G` is the function associating to `g : G` the
+trace of the linear map `V.ρ g`.-/
+def character (V : fdRep k G) (g : G) := linear_map.trace k V (V.ρ g)
+
+lemma char_mul_comm (V : fdRep k G) (g : G) (h : G) : V.character (h * g) = V.character (g * h) :=
+by simp only [trace_mul_comm, character, map_mul]
+
+@[simp] lemma char_one  (V : fdRep k G) : V.character 1 = finite_dimensional.finrank k V :=
+by simp only [character, map_one, trace_one]
+
+/-- The character is multiplicative under the tensor product. -/
+@[simp] lemma char_tensor (V W : fdRep k G) : (V ⊗ W).character = V.character * W.character :=
+by { ext g, convert trace_tensor_product' (V.ρ g) (W.ρ g) }
+
+/-- The character of isomorphic representations is the same. -/
+lemma char_iso  {V W : fdRep k G} (i : V ≅ W) : V.character = W.character :=
+by { ext g, simp only [character, fdRep.iso.conj_ρ i], exact (trace_conj' (V.ρ g) _).symm }
+
+end monoid
+
+section group
+
+variables [group G]
+
+/-- The character of a representation is constant on conjugacy classes. -/
+@[simp] lemma char_conj (V : fdRep k G) (g : G) (h : G) :
+  V.character (h * g * h⁻¹) = V.character g :=
+by rw [char_mul_comm, inv_mul_cancel_left]
+
+@[simp] lemma char_dual (V : fdRep k G) (g : G) : (of (dual V.ρ)).character g = V.character g⁻¹ :=
+  trace_transpose' (V.ρ g⁻¹)
+
+@[simp] lemma char_lin_hom (V W : fdRep k G) (g : G) :
+  (of (lin_hom V.ρ W.ρ)).character g = (V.character g⁻¹) * (W.character g) :=
+by { rw [←char_iso (dual_tensor_iso_lin_hom _ _), char_tensor, pi.mul_apply, char_dual], refl }
+
+end group
+
+end fdRep
diff --git a/src/representation_theory/fdRep.lean b/src/representation_theory/fdRep.lean
index 234bc92c25010..bdc8703f7707c 100644
--- a/src/representation_theory/fdRep.lean
+++ b/src/representation_theory/fdRep.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import representation_theory.Rep
 import algebra.category.FinVect
+import representation_theory.basic
 
 /-!
 # `fdRep k G` is the category of finite dimensional `k`-linear representations of `G`.
@@ -50,13 +51,28 @@ by { change module k ((forget₂ (fdRep k G) (FinVect k)).obj V), apply_instance
 instance (V : fdRep k G) : finite_dimensional k V :=
 by { change finite_dimensional k ((forget₂ (fdRep k G) (FinVect k)).obj V), apply_instance, }
 
+/-- The monoid homomorphism corresponding to the action of `G` onto `V : fdRep k G`. -/
+def ρ (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ
+
+/-- The underlying `linear_equiv` of an isomorphism of representations. -/
+def iso_to_linear_equiv {V W : fdRep k G} (i : V ≅ W) : V ≃ₗ[k] W :=
+  FinVect.iso_to_linear_equiv ((Action.forget (FinVect k) (Mon.of G)).map_iso i)
+
+lemma iso.conj_ρ {V W : fdRep k G} (i : V ≅ W) (g : G) :
+   W.ρ g = (fdRep.iso_to_linear_equiv i).conj (V.ρ g) :=
+begin
+  rw [fdRep.iso_to_linear_equiv, ←FinVect.iso.conj_eq_conj, iso.conj_apply],
+  rw [iso.eq_inv_comp ((Action.forget (FinVect k) (Mon.of G)).map_iso i)],
+  exact (i.hom.comm g).symm,
+end
+
 -- This works well with the new design for representations:
 example (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ
 
-/-- Lift an unbundled representation to `Rep`. -/
+/-- Lift an unbundled representation to `fdRep`. -/
 @[simps ρ]
 def of {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V]
-  (ρ : G →* (V →ₗ[k] V)) : Rep k G :=
+  (ρ : representation k G V) : fdRep k G :=
 ⟨FinVect.of k V, ρ⟩
 
 instance : has_forget₂ (fdRep k G) (Rep k G) :=
@@ -75,3 +91,31 @@ noncomputable instance : right_rigid_category (fdRep k G) :=
 by { change right_rigid_category (Action (FinVect k) (Group.of G)), apply_instance, }
 
 end fdRep
+
+namespace fdRep
+
+open representation
+
+variables {k G V W : Type u} [field k] [group G]
+variables [add_comm_group V] [module k V] [add_comm_group W] [module k W]
+variables [finite_dimensional k V] [finite_dimensional k W]
+variables (ρV : representation k G V) (ρW : representation k G W)
+
+/-- Auxiliary definition for `fdRep.dual_tensor_iso_lin_hom`. -/
+noncomputable def dual_tensor_iso_lin_hom_aux :
+  ((fdRep.of ρV.dual) ⊗ (fdRep.of ρW)).V ≅ (fdRep.of (lin_hom ρV ρW)).V :=
+(dual_tensor_hom_equiv k V W).to_FinVect_iso
+
+/-- When `V` and `W` are finite dimensional representations of a group `G`, the isomorphism
+`dual_tensor_hom_equiv k V W` of vector spaces induces an isomorphism of representations. -/
+noncomputable def dual_tensor_iso_lin_hom :
+  (fdRep.of ρV.dual) ⊗ (fdRep.of ρW) ≅ fdRep.of (lin_hom ρV ρW) :=
+begin
+  apply Action.mk_iso (dual_tensor_iso_lin_hom_aux ρV ρW),
+  convert (dual_tensor_hom_comm ρV ρW),
+end
+
+@[simp] lemma dual_tensor_iso_lin_hom_hom_hom :
+  (dual_tensor_iso_lin_hom ρV ρW).hom.hom = dual_tensor_hom k V W := rfl
+
+end fdRep