From 95f4590d2de0ba53f6ed45ba5002a4c1fa8e2f66 Mon Sep 17 00:00:00 2001
From: Anne Baanen <vierkantor@vierkantor.com>
Date: Wed, 3 Apr 2024 17:37:30 +0000
Subject: [PATCH] refactor(Algebra/Module): Use coercion from
 SemilinearMapClass to SemilinearMap (#10758)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds a coercion from any instance of `SemilinearMapClass` to `SemilinearMap`. This is the standard practice for other parts of the library, such as ring homs (see also the recent change #10368). I also expect this change will help with some rough edges in #6057. Previously, a coercion from `f : AlgHom` to `LinearMap` would look like `f.toNonUnitalAlgHom.toDistribMulActionHom.toLinearMap`, now it should look like `SemilinearMapClass.semilinearMap f`.

The new coercion instances are `CoeHead` since the left hand side is a free variable `F`. I redefined the existing `DistribMulActionHom → LinearMap` coercion in terms of the `SemilinearMapClass` coercion to ensure we don't get any diamonds.
---
 Mathlib/Algebra/Module/LinearMap/Basic.lean | 32 ++++++++++++++++-----
 1 file changed, 25 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/Module/LinearMap/Basic.lean b/Mathlib/Algebra/Module/LinearMap/Basic.lean
index f6396cec981c2f..57d81e1102ac16 100644
--- a/Mathlib/Algebra/Module/LinearMap/Basic.lean
+++ b/Mathlib/Algebra/Module/LinearMap/Basic.lean
@@ -172,11 +172,16 @@ theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
 #align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_inv
 
 /-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
-abbrev semilinearMap : M →ₛₗ[σ] M₃ where
+@[coe]
+def semilinearMap : M →ₛₗ[σ] M₃ where
   toFun := f
   map_add' := map_add f
   map_smul' := map_smulₛₗ f
 
+/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
+instance instCoeToSemilinearMap : CoeHead F (M →ₛₗ[σ] M₃) where
+  coe f := semilinearMap f
+
 end SemilinearMapClass
 
 namespace LinearMapClass
@@ -186,6 +191,10 @@ variable {F : Type*} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Mod
 /-- Reinterpret an element of a type of linear maps as a linear map. -/
 abbrev linearMap : M₁ →ₗ[R] M₂ := SemilinearMapClass.semilinearMap f
 
+/-- Reinterpret an element of a type of linear maps as a linear map. -/
+instance instCoeToLinearMap : CoeHead F (M₁ →ₗ[R] M₂) where
+  coe f := SemilinearMapClass.semilinearMap f
+
 end LinearMapClass
 
 namespace LinearMap
@@ -266,6 +275,17 @@ theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
     ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f :=
   rfl
 
+theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
+    ((f : M →ₛₗ[σ] M₃) : M → M₃) = f :=
+  rfl
+
+theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
+    {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) :
+    f = g := by
+  apply DFunLike.ext
+  intro m
+  exact DFunLike.congr_fun h m
+
 /-- Identity map as a `LinearMap` -/
 def id : M →ₗ[R] M :=
   { DistribMulActionHom.id R with }
@@ -650,13 +670,11 @@ namespace DistribMulActionHom
 variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂]
 
 /-- A `DistribMulActionHom` between two modules is a linear map. -/
-@[coe]
-def toLinearMap (fₗ : M →+[R] M₂) : M →ₗ[R] M₂ :=
-  { fₗ with }
-#align distrib_mul_action_hom.to_linear_map DistribMulActionHom.toLinearMap
+instance instLinearMapClass : LinearMapClass (M →+[R] M₂) R M M₂ where
+  map_smulₛₗ := map_smul
 
-instance : CoeTC (M →+[R] M₂) (M →ₗ[R] M₂) :=
-  ⟨toLinearMap⟩
+instance instCoeTCLinearMap : CoeTC (M →+[R] M₂) (M →ₗ[R] M₂) where
+  coe f := SemilinearMapClass.semilinearMap f
 
 -- Porting note: because coercions get unfolded, there is no need for this rewrite
 #noalign distrib_mul_action_hom.to_linear_map_eq_coe