refactor(RepresentationTheory/Rep/Res): refactor resFunctor (leanprover-community#41054)

This PR refactors the definition of `resFunctor`, in the current master since the whole definition is an `abbrev`, everything is exposed and if one does `ext; simp` one of the possible outcome in the infoview would be 
```
ofHom { toLinearMap := (Hom.hom ..).toLinearMap, isIntertwining' := ⋯ }
```
which is not helpful unfolds too much, this PR seals the `map` part of the functor to make it less transparent while keep the definition of `resFunctor` as an `abbrev` to maintain the full transparency on the underlying type.

Author: Whysoserioushah

Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean

@@ -551,7 +551,7 @@ noncomputable def resNatTrans (n : ℕ) :
     simp only [functor_map, Functor.comp_map,
       ← cancel_epi (groupCohomology.π _ n), HomologicalComplex.homologyπ_naturality_assoc,
       HomologicalComplex.homologyπ_naturality, ← HomologicalComplex.cyclesMap_comp_assoc,
-      ← cochainsMap_comp, res_obj_ρ, Category.comp_id, Rep.hom_id]
+      ← cochainsMap_comp, res_obj_ρ, Category.comp_id]
     rfl
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean

@@ -853,11 +853,9 @@ noncomputable def coresNatTrans (n : ℕ) :
     simp only [← cancel_epi (groupHomology.π _ n), Functor.comp_map,
       functor_map, HomologicalComplex.homologyπ_naturality_assoc,
       HomologicalComplex.homologyπ_naturality, ← HomologicalComplex.cyclesMap_comp_assoc,
-      ← chainsMap_comp, res_obj_ρ, Rep.hom_id, Category.id_comp]
+      ← chainsMap_comp, Category.id_comp]
     rfl
 
-
-
 set_option backward.isDefEq.respectTransparency false in
 /-- Given a normal subgroup `S ≤ G`, this sends `A : Rep k G` to the `n`th "coinflation" map
 `Hₙ(G, A) ⟶ Hₙ(G ⧸ S, A_S)` induced by the quotient maps `G →* G ⧸ S` and `A →ₗ A_S`. -/

Mathlib/RepresentationTheory/Induced.lean

@@ -260,8 +260,7 @@ noncomputable def coinvariantsTensorIndNatIso :
     (coinvariantsTensor k H).obj (ind φ A) ≅ resFunctor φ ⋙ (coinvariantsTensor k G).obj A :=
   NatIso.ofComponents (fun B => coinvariantsTensorIndIso φ A B) fun {X Y} f => by
     ext
-    simp [coinvariantsTensorIndHom, coinvariantsTensorMk,
-      hom_comm_apply, Representation.IntertwiningMap.toLinearMap_apply]
+    simp [coinvariantsTensorIndHom, coinvariantsTensorMk, hom_comm_apply]
 
 end
 end Rep

Mathlib/RepresentationTheory/Invariants.lean

@@ -265,7 +265,7 @@ noncomputable def quotientToInvariantsFunctor (S : Subgroup G) [S.Normal] :
     Rep.{w} k G ⥤ Rep k (G ⧸ S) where
   obj X := X.quotientToInvariants S
   map {X Y} f := Rep.ofHom ⟨((invariantsFunctor k S).map ((Rep.resFunctor S.subtype).map f)).hom,
-    fun g ↦ QuotientGroup.induction_on g fun g ↦ by ext x; simp [hom_comm_apply]⟩
+    fun g ↦ QuotientGroup.induction_on g fun g ↦ by ext; simp [hom_comm_apply]⟩
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The adjunction between the functor equipping a module with the trivial representation, and

Mathlib/RepresentationTheory/Rep/Res.lean

@@ -25,10 +25,17 @@ open CategoryTheory
 
 namespace Rep
 
+/-- The map induced by a monoid homomorphism `f : H →* G` on morphisms between
+`G`-representations. -/
+@[expose, implicit_reducible]
+def resMap {X Y : Rep k G} (f : H →* G) (p : X ⟶ Y) :
+    of (X := X.V) (X.ρ.comp f) ⟶ of (X := Y.V) (Y.ρ.comp f) :=
+  ofHom ⟨p.hom, fun h ↦ by simpa using p.hom.2 (f h)⟩
+
 /-- The restriction functor `Rep R G ⥤ Rep R H` for a subgroup `H` of `G`. -/
 abbrev resFunctor (f : H →* G) : Rep.{t} k G ⥤ Rep k H where
   obj A := of (X := A.V) (A.ρ.comp f)
-  map f' := ofHom ⟨f'.hom, fun h ↦ by simpa using f'.hom.2 (f h)⟩
+  map f' := resMap f f'
 
 /-- The restriction of `X : Rep k G` associated to a monoid homomorphism `f : H →* G` -/
 abbrev res (f : H →* G) (M : Rep k G) := (resFunctor f).obj M
@@ -43,16 +50,23 @@ lemma coe_res_obj_ρ' (h : H) : (res f M).ρ h = M.ρ (f h) := rfl
 
 lemma res_obj_V : (res f M).V = M.V := rfl
 
-lemma res_map_hom_toLinearMap {M N : Rep k G} (p : M ⟶ N) :
-    ((resFunctor f).map p).hom.toLinearMap = p.hom.toLinearMap := rfl
+@[simp]
+lemma resMap_hom_toLinearMap {M N : Rep k G} (p : M ⟶ N) :
+    (resMap f p).hom.toLinearMap = p.hom.toLinearMap := rfl
+
+@[deprecated (since := "26/06/2026")]
+alias res_map_hom_toLinearMap := resMap_hom_toLinearMap
+
+@[simp]
+lemma resMap_hom_apply {M N : Rep k G} (p : M ⟶ N) (x : M.V) :
+    @DFunLike.coe (Representation.IntertwiningMap (M.ρ.comp f) (N.ρ.comp f)) _ _ _
+      (resMap f p).hom x = p.hom x := rfl
 
 section
 
 instance : (resFunctor (k := k) f).Faithful where
   map_injective h := by
-    ext : 2
-    rw [Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff] at h
-    simpa using h
+    simpa [Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff] using h
 
 /-- Morphism between `X Y : Rep k G` can be lifted from restrictions associated with `f : H →* G`
   when `f` is surjective. -/
@@ -65,21 +79,13 @@ lemma liftHomOfSurj_toLinearMap {X Y : Rep k G} (hf : Function.Surjective f)
       f'.hom.toLinearMap := rfl
 
 lemma full_res (hf : (⇑f).Surjective) : (resFunctor (k := k) f).Full where
-  map_surjective {X Y} f' := ⟨liftHomOfSurj f hf f', by
-    ext : 2; rw [res_map_hom_toLinearMap, liftHomOfSurj_toLinearMap]⟩
+  map_surjective {X Y} f' := ⟨liftHomOfSurj f hf f', by ext; simp⟩
 
 instance : (resFunctor (k := k) f).Additive where
-  map_add {_ _} _ _ := by
-    ext : 2;
-    simp only [add_hom, Representation.IntertwiningMap.add_toLinearMap]
-    rfl
+  map_add {_ _} _ _ := by ext : 2; simp [add_hom]
 
 instance {k : Type u} [CommSemiring k] : (resFunctor (k := k) f).Linear k where
-  map_smul {X Y} l r := by
-    ext : 2;
-    rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
-      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
-      res_map_hom_toLinearMap]
+  map_smul {_ _} _ _ := by ext : 2; simp [smul_hom]
 
 noncomputable section