Rename homMulEquiv to endMulEquiv

leanprover-community · Dec 2, 2024 · d34a272 · d34a272
1 parent 656f2c3
commit d34a272
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -420,7 +420,7 @@ variable (M N : ModuleCat.{v} R)
 
 /-- `ModuleCat.Hom.hom` as an isomorphism of monoids. -/
 @[simps]
-def homMulEquiv : End M ≃* (M →ₗ[R] M) where
+def endMulEquiv : End M ≃* (M →ₗ[R] M) where
   toFun := ModuleCat.Hom.hom
   invFun := ModuleCat.asHom
   map_mul' _ _ := rfl

diff --git a/Mathlib/RepresentationTheory/Character.lean b/Mathlib/RepresentationTheory/Character.lean
@@ -116,7 +116,7 @@ theorem char_orthonormal (V W : FDRep k G) [Simple V] [Simple W] :
     rw [char_iso (FDRep.dualTensorIsoLinHom W.ρ V)]
   -- The average over the group of the character of a representation equals the dimension of the
   -- space of invariants.
-  rw [average_char_eq_finrank_invariants, ← FDRep.homMulEquiv_comp_ρ (of _),
+  rw [average_char_eq_finrank_invariants, ← FDRep.endMulEquiv_comp_ρ (of _),
       FDRep.of_ρ (linHom W.ρ V.ρ)]
   -- The space of invariants of `Hom(W, V)` is the subspace of `G`-equivariant linear maps,
   -- `Hom_G(W, V)`.

diff --git a/Mathlib/RepresentationTheory/FDRep.lean b/Mathlib/RepresentationTheory/FDRep.lean
@@ -82,15 +82,15 @@ instance (V W : FDRep k G) : FiniteDimensional k (V ⟶ W) :=
 
 /-- The monoid homomorphism corresponding to the action of `G` onto `V : FDRep k G`. -/
 def ρ (V : FDRep k G) : G →* V →ₗ[k] V :=
-  (ModuleCat.homMulEquiv _).toMonoidHom.comp (Action.ρ V)
+  (ModuleCat.endMulEquiv _).toMonoidHom.comp (Action.ρ V)
 
 @[simp]
-lemma homMulEquiv_symm_comp_ρ (V : FDRep k G) :
-    (MonoidHomClass.toMonoidHom (ModuleCat.homMulEquiv V.V.obj).symm).comp (ρ V) = Action.ρ V := rfl
+lemma endMulEquiv_symm_comp_ρ (V : FDRep k G) :
+    (MonoidHomClass.toMonoidHom (ModuleCat.endMulEquiv V.V.obj).symm).comp (ρ V) = Action.ρ V := rfl
 
 @[simp]
-lemma homMulEquiv_comp_ρ (V : FDRep k G) :
-    (MonoidHomClass.toMonoidHom (ModuleCat.homMulEquiv V.V.obj)).comp (Action.ρ V) = ρ V := rfl
+lemma endMulEquiv_comp_ρ (V : FDRep k G) :
+    (MonoidHomClass.toMonoidHom (ModuleCat.endMulEquiv V.V.obj)).comp (Action.ρ V) = ρ V := rfl
 
 @[simp]
 lemma hom_action_ρ (V : FDRep k G) (g : G) : (Action.ρ V g).hom = ρ V g := rfl
@@ -111,7 +111,7 @@ theorem Iso.conj_ρ {V W : FDRep k G} (i : V ≅ W) (g : G) :
 @[simps ρ]
 def of {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
     (ρ : Representation k G V) : FDRep k G :=
-  ⟨FGModuleCat.of k V, ρ ≫ MonCat.ofHom (ModuleCat.homMulEquiv _).symm.toMonoidHom⟩
+  ⟨FGModuleCat.of k V, ρ ≫ MonCat.ofHom (ModuleCat.endMulEquiv _).symm.toMonoidHom⟩
 
 instance : HasForget₂ (FDRep k G) (Rep k G) where
   forget₂ := (forget₂ (FGModuleCat k) (ModuleCat k)).mapAction (MonCat.of G)

diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean
@@ -61,11 +61,11 @@ instance (V : Rep k G) : Module k V := by
 -/
 def ρ (V : Rep k G) : Representation k G V :=
 -- Porting note: was `V.ρ`
-  (ModuleCat.homMulEquiv V.V).toMonoidHom.comp (Action.ρ V)
+  (ModuleCat.endMulEquiv V.V).toMonoidHom.comp (Action.ρ V)
 
 /-- Lift an unbundled representation to `Rep`. -/
 def of {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) : Rep k G :=
-  ⟨ModuleCat.of k V, MonCat.ofHom ((ModuleCat.homMulEquiv _).symm.toMonoidHom.comp ρ) ⟩
+  ⟨ModuleCat.of k V, MonCat.ofHom ((ModuleCat.endMulEquiv _).symm.toMonoidHom.comp ρ) ⟩
 
 @[simp]
 theorem coe_of {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) :
@@ -77,7 +77,7 @@ theorem of_ρ {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k
   rfl
 
 theorem Action_ρ_eq_ρ {A : Rep k G} :
-    Action.ρ A = (ModuleCat.homMulEquiv _).symm.toMonoidHom.comp A.ρ :=
+    Action.ρ A = (ModuleCat.endMulEquiv _).symm.toMonoidHom.comp A.ρ :=
   rfl
 
 @[simp]