feat(representation_theory/basic): basics of group representation the…

…ory (#11207)

Some basic lemmas about group representations and some theory regarding the subspace of fixed points of a representation. 



Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/monoid_algebra/basic.lean

@@ -368,6 +368,9 @@ variables (k G)
 
 end
 
+lemma smul_of [mul_one_class G] (g : G) (r : k) :
+  r • (of k G g) = single g r := by simp
+
 lemma of_injective [mul_one_class G] [nontrivial k] : function.injective (of k G) :=
 λ a b h, by simpa using (single_eq_single_iff _ _ _ _).mp h
 
@@ -813,6 +816,28 @@ by simp
 
 end opposite
 
+section submodule
+
+variables {k G} [comm_semiring k] [monoid G]
+variables {V : Type*} [add_comm_monoid V]
+variables [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V]
+
+/-- A submodule over `k` which is stable under scalar multiplication by elements of `G` is a
+submodule over `monoid_algebra k G`  -/
+def submodule_of_smul_mem (W : submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → (of k G g) • v ∈ W) :
+  submodule (monoid_algebra k G) V :=
+{ carrier := W,
+  zero_mem' := W.zero_mem',
+  add_mem' := W.add_mem',
+  smul_mem' := begin
+    intros f v hv,
+    rw [←finsupp.sum_single f, finsupp.sum, finset.sum_smul],
+    simp_rw [←smul_of, smul_assoc],
+    exact submodule.sum_smul_mem W _ (λ g _, h g v hv)
+  end  }
+
+end submodule
+
 end monoid_algebra
 
 /-! ### Additive monoids -/

src/representation_theory/basic.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2022 Antoine Labelle. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Labelle
+-/
+import algebra.module.basic
+import algebra.module.linear_map
+import algebra.monoid_algebra.basic
+import linear_algebra.trace
+
+/-!
+# Monoid representations
+
+This file introduces monoid representations and their characters and proves basic lemmas about them,
+including equivalences between different definitions of representations.
+
+## Main definitions
+
+  * `representation.as_module`
+  * `representation.as_group_hom`
+  * `representation.character`
+
+## Implementation notes
+
+A representation of a monoid `G` over a commutative semiring `k` is implemented as a `k`-module `V`
+together with a `distrib_mul_action G V` instance and a `smul_comm_class G k V` instance.
+
+Alternatively, one can use a monoid homomorphism `G →* (V →ₗ[k] V)`. The definitions `as_monoid_hom`
+and `rep_space` allow to go back and forth between these two definitions.
+-/
+
+open monoid_algebra
+
+namespace representation
+
+section
+variables (k G V : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V]
+variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]
+
+/--
+A `k`-linear representation of `G` on `V` can be thought of as
+an algebra map from `monoid_algebra k G` into the `k`-linear endomorphisms of `V`.
+-/
+noncomputable def as_algebra_hom : monoid_algebra k G →ₐ[k] (module.End k V) :=
+  (lift k G _) (distrib_mul_action.to_module_End k V)
+
+lemma as_algebra_hom_def :
+  as_algebra_hom k G V = (lift k G _) (distrib_mul_action.to_module_End k V) := rfl
+
+@[simp]
+lemma as_algebra_hom_single (g : G):
+  (as_algebra_hom k G V (finsupp.single g 1)) = (distrib_mul_action.to_module_End k V) g :=
+by simp [as_algebra_hom_def]
+
+/--
+A `k`-linear representation of `G` on `V` can be thought of as
+a module over `monoid_algebra k G`.
+-/
+noncomputable instance as_module : module (monoid_algebra k G) V :=
+  module.comp_hom V (as_algebra_hom k G V).to_ring_hom
+
+lemma as_module_apply (a : monoid_algebra k G) (v : V):
+  a • v = (as_algebra_hom k G V a) v := rfl
+
+lemma of_smul (g : G) (v : V) :
+  (of k G g) • v =  g • v := by simp [as_module_apply]
+
+instance as_module_scalar_tower : is_scalar_tower k (monoid_algebra k G) V :=
+{ smul_assoc := λ r a v, by simp [as_module_apply] }
+
+instance as_module_smul_comm : smul_comm_class k (monoid_algebra k G) V :=
+{ smul_comm := λ r a v, by simp [as_module_apply] }
+
+end
+
+section group
+variables (k G V : Type*) [comm_semiring k] [group G] [add_comm_monoid V]
+variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]
+
+/--
+When `G` is a group, a `k`-linear representation of `G` on `V` can be thought of as
+a group homomorphism from `G` into the invertible `k`-linear endomorphisms of `V`.
+-/
+def as_group_hom : G →* units (V →ₗ[k] V) :=
+  monoid_hom.to_hom_units (distrib_mul_action.to_module_End k V)
+
+end group
+
+section character
+
+variables (k G V : Type*) [field k] [group G] [add_comm_group V]
+variables [module k V] [distrib_mul_action G V] [smul_comm_class G k 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 :=
+linear_map.trace k V (as_group_hom k G V g)
+
+/-- The evaluation of the character at the identity is the dimension of the representation. -/
+theorem char_one : character k G V 1 = finite_dimensional.finrank k V := by simp
+
+/-- The character of a representation is constant on conjugacy classes. -/
+theorem char_conj (g : G) (h : G) : (character k G V) (h * g * h⁻¹) = (character k G V) g := by simp
+
+end character
+
+end representation

src/representation_theory/invariants.lean

@@ -0,0 +1,121 @@
+/-
+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.basic
+
+/-!
+# Subspace of invariants a group representation
+
+This file introduce the subspace of invariants of a group representation
+and proves basic result about it.
+The main tool used is the average of all elements of the group, seen as an element of
+`monoid_algebra k G`. Scalar multiplication by this special element gives a projection onto the
+subspace of invariants.
+In order for the definition of the average element to make sense, we need to assume for most of the
+results that the order of `G` is invertible in `k` (e. g. `k` has characteristic `0`).
+-/
+
+open_locale big_operators
+open monoid_algebra finset finite_dimensional linear_map representation
+
+namespace representation
+
+section average
+
+variables (k G : Type*) [comm_semiring k] [group G]
+variables [fintype G] [invertible (fintype.card G : k)]
+
+/--
+The average of all elements of the group `G`, considered as an element of `monoid_algebra k G`.
+-/
+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 [average_def, finset.mul_sum],
+  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,
+  rw function.bijective.sum_comp (group.mul_left_bijective g) _,
+end
+
+/--
+`average k G` is invariant under right multiplication by elements of `G`.
+-/
+@[simp]
+theorem mul_average_right (g : G) :
+  average k G * finsupp.single g 1 = average k G :=
+begin
+  simp [average_def, finset.sum_mul],
+  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,
+  rw function.bijective.sum_comp (group.mul_right_bijective g) _,
+end
+
+end average
+
+section invariants
+
+variables (k G V : Type*) [comm_semiring k] [group G] [add_comm_group V]
+variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]
+
+/--
+The subspace of invariants, consisting of the vectors fixed by all elements of `G`.
+-/
+def invariants : submodule k V :=
+{ carrier := set_of (λ v, ∀ (g : G), g • v = v),
+  zero_mem' := by simp,
+  add_mem' := λ v w hv hw g, by simp [hv g, hw g],
+  smul_mem' := λ r v hv g, by simp [smul_comm, hv g] }
+
+@[simp]
+lemma mem_invariants (v : V) : v ∈ (invariants k G V) ↔ ∀ (g: G), g • v = v := by refl
+
+lemma invariants_eq_inter :
+  (invariants k G V).carrier = ⋂ g : G, function.fixed_points (has_scalar.smul g) :=
+by { ext, simp [function.is_fixed_pt] }
+
+/--
+The subspace of invariants, as a submodule over `monoid_algebra k G`.
+-/
+noncomputable def invariants' : submodule (monoid_algebra k G) V :=
+  submodule_of_smul_mem (invariants k G V) (λ g v hv, by {rw [of_smul, hv g], exact hv})
+
+@[simp] lemma invariants'_carrier :
+  (invariants' k G V).carrier = (invariants k G V).carrier := rfl
+
+variables [fintype G] [invertible (fintype.card G : k)]
+
+/--
+Scalar multiplication by `average k G` sends elements of `V` to the subspace of invariants.
+-/
+theorem smul_average_invariant (v : V) : (average k G) • v ∈ invariants k G V :=
+λ g, by rw [←of_smul k, smul_smul, of_apply, mul_average_left]
+
+/--
+`average k G` acts as the identity on the subspace of invariants.
+-/
+theorem smul_average_id (v ∈ invariants k G V) : (average k G) • v = v :=
+begin
+  simp at H,
+  simp [average_def, sum_smul, H, card_univ, nsmul_eq_smul_cast k _ v, smul_smul, of_smul,
+    -of_apply],
+end
+
+/--
+Scalar multiplication by `average k G` gives a projection map onto the subspace of invariants.
+-/
+noncomputable def average_map : V →ₗ[k] V := (as_algebra_hom k G V) (average k G)
+
+end invariants
+
+end representation