doc: fix some issues under RepresentationTheory (#16409)

Mathlib/RepresentationTheory/Action/Basic.lean

@@ -16,7 +16,7 @@ import Mathlib.CategoryTheory.Conj
 The prototypical example is `V = ModuleCat R`,
 where `Action (ModuleCat R) G` is the category of `R`-linear representations of `G`.
 
-We check `Action V G ≌ (singleObj G ⥤ V)`,
+We check `Action V G ≌ (CategoryTheory.singleObj G ⥤ V)`,
 and construct the restriction functors `res {G H : MonCat} (f : G ⟶ H) : Action V H ⥤ Action V G`.
 -/
 

Mathlib/RepresentationTheory/Basic.lean

@@ -13,11 +13,10 @@ representations.
 
 ## Main definitions
 
-  * Representation.Representation
-  * Representation.character
-  * Representation.tprod
-  * Representation.linHom
-  * Representation.dual
+  * `Representation`
+  * `Representation.tprod`
+  * `Representation.linHom`
+  * `Representation.dual`
 
 ## Implementation notes
 
@@ -26,7 +25,7 @@ homomorphisms `G →* (V →ₗ[k] V)`. We use the abbreviation `Representation`
 
 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`
+module can be accessed via `ρ.asModule`. Conversely, given a `MonoidAlgebra k G`-module `M`,
 `M.ofModule` is the associociated representation seen as a homomorphism.
 -/
 
@@ -449,7 +448,7 @@ theorem dual_apply (g : G) : (dual ρV) g = Module.Dual.transpose (R := k) (ρV
   rfl
 
 /-- Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$
-(implemented by `LinearAlgebra.Contraction.dualTensorHom`).
+(implemented by `dualTensorHom` in `Mathlib.LinearAlgebra.Contraction`).
 Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on
 $Hom_k(V, W)$.
 This lemma says that $φ$ is $G$-linear.

Mathlib/RepresentationTheory/Character.lean

@@ -19,8 +19,8 @@ is the theorem `char_orthonormal`
 
 ## Implementation notes
 
-Irreducible representations are implemented categorically, using the `Simple` class defined in
-`Mathlib.CategoryTheory.Simple`
+Irreducible representations are implemented categorically, using the `CategoryTheory.Simple` class
+defined in `Mathlib.CategoryTheory.Simple`
 
 ## TODO
 * Once we have the monoidal closed structure on `FdRep k G` and a better API for the rigid

Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

@@ -30,8 +30,8 @@ $\mathrm{H}^n(G, A) \cong \mathrm{Ext}^n(k, A),$ where $\mathrm{Ext}$ is taken i
 `Rep k G`.
 
 To talk about cohomology in low degree, please see the file
-`RepresentationTheory.GroupCohomology.LowDegree`, which gives simpler expressions for `H⁰, H¹, H²`
-than the definition `groupCohomology` in this file.
+`Mathlib.RepresentationTheory.GroupCohomology.LowDegree`, which gives simpler expressions for
+`H⁰`, `H¹`, `H²` than the definition `groupCohomology` in this file.
 
 ## Main definitions
 

Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

@@ -23,9 +23,9 @@ This allows us to define a `k[G]`-basis on `k[Gⁿ⁺¹]`, by mapping the natura
 
 We then define the standard resolution of `k` as a trivial representation, by
 taking the alternating face map complex associated to an appropriate simplicial `k`-linear
-`G`-representation. This simplicial object is the `linearization` of the simplicial `G`-set given
-by the universal cover of the classifying space of `G`, `EG`. We prove this simplicial `G`-set `EG`
-is isomorphic to the Čech nerve of the natural arrow of `G`-sets `G ⟶ {pt}`.
+`G`-representation. This simplicial object is the `Rep.linearization` of the simplicial `G`-set
+given by the universal cover of the classifying space of `G`, `EG`. We prove this simplicial
+`G`-set `EG` is isomorphic to the Čech nerve of the natural arrow of `G`-sets `G ⟶ {pt}`.
 
 We then use this isomorphism to deduce that as a complex of `k`-modules, the standard resolution
 of `k` as a trivial `G`-representation is homotopy equivalent to the complex with `k` at 0 and 0