[Merged by Bors] - doc(RepresentationTheory): add some doc for three basic files

Mathlib/RepresentationTheory/Basic.lean

@@ -30,7 +30,12 @@ representations.
 ## Implementation notes
 
 Representations of a monoid `G` on a `k`-module `V` are implemented as
-homomorphisms `G →* (V →ₗ[k] V)`.
+homomorphisms `G →* (V →ₗ[k] V)`. We use the abbreviation `Representation` for this hom space.
+
+The theorem `asAlgebraHom_def` constructs a module over the group `k`-algebra of `G` (implemented
+as `MonoidAlgebra k G`) corresponding to a representation. If `ρ : Representation k G V`, this
+module can be accessed via `ρ.asModule`. Conversely, given a `MonoidAlgebra k G-module `M`
+`M.ofModule` is the associociated representation seen as a homomorphism.
 -/
 
 

Mathlib/RepresentationTheory/Character.lean

@@ -15,6 +15,15 @@ import Mathlib.RepresentationTheory.Invariants
 This file introduces characters of representation and proves basic lemmas about how characters
 behave under various operations on representations.
 
+A key result is the orthogonality of characters for irreducible representations of finite group
+over an algebraically closed field whose characteristic doesn't divide the order of the group. It
+is the therem `char_orthonormal`
+
+# Implementation notes
+
+Irreducible representations are implemented categorically, using the `Simple` class deined in
+`Mathlib.CategoryTheory.Simple`
+
 # TODO
 * Once we have the monoidal closed structure on `FdRep k G` and a better API for the rigid
 structure, `char_dual` and `char_linHom` should probably be stated in terms of `Vᘁ` and `ihom V W`.

Mathlib/RepresentationTheory/FdRep.lean

@@ -20,6 +20,10 @@ Also `V.ρ` gives the homomorphism `G →* (V →ₗ[k] V)`.
 Conversely, given a homomorphism `ρ : G →* (V →ₗ[k] V)`,
 you can construct the bundled representation as `Rep.of ρ`.
 
+We prove Schur's Lemma: the dimension of the `Hom`-space between two irreducible representation is
+`0` if they are not isomorphic, and `1` if they are.
+This is the content of `finrank_hom_simple_simple`
+
 We verify that `FdRep k G` is a `k`-linear monoidal category, and rigid when `G` is a group.
 
 `FdRep k G` has all finite limits.
@@ -125,7 +129,8 @@ open scoped Classical
 -- deterministic timeout.
 instance : HasKernels (FdRep k G) := by infer_instance
 
--- Verify that Schur's lemma applies out of the box.
+/-- Schur's Lemma: the dimension of the `Hom`-space between two irreducible representation is `0` if
+they are not isomorphic, and `1` if they are. It applies out of the box. -/
 theorem finrank_hom_simple_simple [IsAlgClosed k] (V W : FdRep k G) [Simple V] [Simple W] :
     finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0 :=
   CategoryTheory.finrank_hom_simple_simple k V W