feat: add some simp lemmas for FGModuleCat and FDRep (#22668)

Add some `simp` lemmas to deal with `FGModuleCat` and `FDRep`.

Author: ybenmeur

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -58,7 +58,7 @@ instance : CoeSort (FGModuleCat R) (Type u) :=
 
 attribute [coe] FGModuleCat.carrier
 
-@[simp] lemma obj_carrier (M : FGModuleCat R) : M.obj.carrier = M.carrier := rfl
+@[simp] lemma FGModuleCat.obj_carrier (M : FGModuleCat R) : M.obj.carrier = M.carrier := rfl
 
 instance (M : FGModuleCat R) : AddCommGroup M := by
   change AddCommGroup M.obj
@@ -88,6 +88,11 @@ section Ring
 
 variable (R : Type u) [Ring R]
 
+@[simp] lemma hom_comp (A B C : FGModuleCat R) (f : A ⟶ B) (g : B ⟶ C) :
+  (f ≫ g).hom = g.hom.comp f.hom := rfl
+
+@[simp] lemma hom_id (A : FGModuleCat R) : (𝟙 A : A ⟶ A).hom = LinearMap.id := rfl
+
 instance finite (V : FGModuleCat R) : Module.Finite R V :=
   V.property
 
@@ -98,6 +103,10 @@ instance : Inhabited (FGModuleCat R) :=
 abbrev of (V : Type u) [AddCommGroup V] [Module R V] [Module.Finite R V] : FGModuleCat R :=
   ⟨ModuleCat.of R V, by change Module.Finite R V; infer_instance⟩
 
+@[simp]
+lemma of_carrier (V : Type u) [AddCommGroup V] [Module R V] [Module.Finite R V] :
+  of R V = V := rfl
+
 variable {R} in
 /-- Lift a linear map between finitely generated modules to `FGModuleCat R`. -/
 abbrev ofHom {V W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V]

Mathlib/RepresentationTheory/FDRep.lean

@@ -125,6 +125,21 @@ abbrev of {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V]
     (ρ : Representation R G V) : FDRep R G :=
   ⟨FGModuleCat.of R V, (ModuleCat.endRingEquiv _).symm.toMonoidHom.comp ρ⟩
 
+/-- This lemma is about `FDRep.ρ`, instead of `Action.ρ` for `of_ρ`. -/
+@[simp]
+theorem of_ρ' {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] (ρ : G →* V →ₗ[R] V) :
+    (of ρ).ρ = ρ := rfl
+
+@[simp]
+theorem ρ_inv_self_apply {G : Type u} [Group G] {A : FDRep R G} (g : G) (x : A) :
+    A.ρ g⁻¹ (A.ρ g x) = x :=
+  show (A.ρ g⁻¹ * A.ρ g) x = x by rw [← map_mul, inv_mul_cancel, map_one, LinearMap.one_apply]
+
+@[simp]
+theorem ρ_self_inv_apply {G : Type u} [Group G] {A : FDRep R G} (g : G) (x : A) :
+    A.ρ g (A.ρ g⁻¹ x) = x :=
+  show (A.ρ g * A.ρ g⁻¹) x = x by rw [← map_mul, mul_inv_cancel, map_one, LinearMap.one_apply]
+
 instance : HasForget₂ (FDRep R G) (Rep R G) where
   forget₂ := (forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G