feat(representation_theory/character): formula for the dimension of t…

…he invariants in terms of the character (#15084)

src/representation_theory/character.lean

@@ -6,6 +6,7 @@ Authors: Antoine Labelle
 import representation_theory.fdRep
 import linear_algebra.trace
 import representation_theory.basic
+import representation_theory.invariants
 
 /-!
 # Characters of representations
@@ -22,7 +23,8 @@ noncomputable theory
 
 universes u
 
-open linear_map category_theory.monoidal_category representation
+open linear_map category_theory.monoidal_category representation finite_dimensional
+open_locale big_operators
 
 variables {k G : Type u} [field k]
 
@@ -68,6 +70,12 @@ by rw [char_mul_comm, inv_mul_cancel_left]
   (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 }
 
+variables [fintype G] [invertible (fintype.card G : k)]
+
+theorem average_char_eq_finrank_invariants (V : fdRep k G) :
+  ⅟(fintype.card G : k) • ∑ g : G, V.character g = finrank k (invariants V.ρ) :=
+by { rw ←(is_proj_average_map V.ρ).trace, simp [character, group_algebra.average, _root_.map_sum], }
+
 end group
 
 end fdRep

src/representation_theory/invariants.lean

@@ -33,16 +33,14 @@ The average of all elements of the group `G`, considered as an element of `monoi
 noncomputable def average : monoid_algebra k G :=
   ⅟(fintype.card G : k) • ∑ g : G, of k G g
 
-lemma average_def : average k G = ⅟(fintype.card G : k) • ∑ g : G, of k G g := rfl
-
 /--
 `average k G` is invariant under left multiplication by elements of `G`.
 -/
 @[simp]
 theorem mul_average_left (g : G) :
   (finsupp.single g 1 * average k G : monoid_algebra k G) = average k G :=
 begin
-  simp only [mul_one, finset.mul_sum, algebra.mul_smul_comm, average_def, monoid_algebra.of_apply,
+  simp only [mul_one, finset.mul_sum, algebra.mul_smul_comm, average, monoid_algebra.of_apply,
     finset.sum_congr, monoid_algebra.single_mul_single],
   set f : G → monoid_algebra k G := λ x, finsupp.single x 1,
   show ⅟ ↑(fintype.card G) • ∑ (x : G), f (g * x) = ⅟ ↑(fintype.card G) • ∑ (x : G), f x,
@@ -56,7 +54,7 @@ end
 theorem mul_average_right (g : G) :
   average k G * finsupp.single g 1 = average k G :=
 begin
-  simp only [mul_one, finset.sum_mul, algebra.smul_mul_assoc, average_def, monoid_algebra.of_apply,
+  simp only [mul_one, finset.sum_mul, algebra.smul_mul_assoc, average, monoid_algebra.of_apply,
     finset.sum_congr, monoid_algebra.single_mul_single],
   set f : G → monoid_algebra k G := λ x, finsupp.single x 1,
   show ⅟ ↑(fintype.card G) • ∑ (x : G), f (x * g) = ⅟ ↑(fintype.card G) • ∑ (x : G), f x,
@@ -111,7 +109,7 @@ The `average_map` acts as the identity on the subspace of invariants.
 theorem average_map_id (v : V) (hv : v ∈ invariants ρ) : average_map ρ v = v :=
 begin
   rw mem_invariants at hv,
-  simp [average_def, map_sum, hv, finset.card_univ, nsmul_eq_smul_cast k _ v, smul_smul],
+  simp [average, map_sum, hv, finset.card_univ, nsmul_eq_smul_cast k _ v, smul_smul],
 end
 
 theorem is_proj_average_map : linear_map.is_proj ρ.invariants ρ.average_map :=