improved R-linearity to A-linearity in the PushForward of Derivations (#31464)

Let $A$ be an $R$-algebra for a commutative ring $R$ and $f:M\to N$ an $A$-module homomorphism.
Given a derivation $D\in Der_R(A,M)$, we have a derivation $f \circ D$ of $Der_R(A,N)$. The induced map
$Der_R(A,M)\to  Der_R(A,N)$ is $A$-linear but was only reported to be $R$-linear in the previous implementation.

All changes are in the PushForward section of the RingTheory/Derivation/Basic.lean file. The statements of definitions 
* `_root_.LinearMap.compDer`
* `llcomp`
* `_root_.LinearEquiv.compDer`
are changed from $R$-linear to $A$-linear.

For the stronger linearity the proof of `map_smul'` in `_root_.LinearMap.compDer` had to be changed. The rest remains as is.


Edit: Some files explicitly used the weaker version, these have now been changed, by applying `.restrictScalars (R:=...)`, whereever the weaker linearity version of `compDer` was needed.

Co-authored-by: leo <leonid.ryvkin@rub.de>

Author: Ljon4ik4

Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean

@@ -159,7 +159,8 @@ instance : AddCommGroup (LeftInvariantDerivation I G) :=
   coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => rfl) fun _ _ => rfl
 
 instance : SMul 𝕜 (LeftInvariantDerivation I G) where
-  smul r X := ⟨r • X.1, fun g => by simp_rw [LinearMap.map_smul, left_invariant']⟩
+  smul r X := ⟨r • X.1, fun g => by
+    simp only [LinearMap.map_smul_of_tower, map_smul]; rw [left_invariant']⟩
 
 variable (r)
 

Mathlib/Geometry/Manifold/DerivationBundle.lean

@@ -113,8 +113,8 @@ namespace Derivation
 variable {I}
 
 /-- The evaluation at a point as a linear map. -/
-def evalAt (x : M) : Derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ →ₗ[𝕜] PointDerivation I x :=
-  (ContMDiffFunction.evalAt I x).compDer
+def evalAt (x : M) : Derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ →ₗ[C^∞⟮I, M; 𝕜⟯⟨x⟩]
+  PointDerivation I x := (ContMDiffFunction.evalAt I x).compDer
 
 theorem evalAt_apply (x : M) : evalAt x X f = (X f) x :=
   rfl

Mathlib/RingTheory/Derivation/Basic.lean

@@ -267,15 +267,15 @@ variable (f : M →ₗ[A] N) (e : M ≃ₗ[A] N)
 
 /-- We can push forward derivations using linear maps, i.e., the composition of a derivation with a
 linear map is a derivation. Furthermore, this operation is linear on the spaces of derivations. -/
-def _root_.LinearMap.compDer : Derivation R A M →ₗ[R] Derivation R A N where
+def _root_.LinearMap.compDer : Derivation R A M →ₗ[A] Derivation R A N where
   toFun D :=
     { toLinearMap := (f : M →ₗ[R] N).comp (D : A →ₗ[R] M)
       map_one_eq_zero' := by simp only [LinearMap.comp_apply, coeFn_coe, map_one_eq_zero, map_zero]
       leibniz' := fun a b => by
         simp only [coeFn_coe, LinearMap.comp_apply, LinearMap.map_add, leibniz,
           LinearMap.coe_restrictScalars, LinearMap.map_smul] }
   map_add' D₁ D₂ := by ext; exact LinearMap.map_add _ _ _
-  map_smul' r D := by dsimp; ext; exact LinearMap.map_smul (f : M →ₗ[R] N) _ _
+  map_smul' r D := by ext; dsimp; simp only [_root_.map_smul]
 
 @[simp]
 theorem coe_to_linearMap_comp : (f.compDer D : A →ₗ[R] N) = (f : M →ₗ[R] N).comp (D : A →ₗ[R] M) :=
@@ -287,13 +287,13 @@ theorem coe_comp : (f.compDer D : A → N) = (f : M →ₗ[R] N).comp (D : A →
 
 /-- The composition of a derivation with a linear map as a bilinear map -/
 @[simps]
-def llcomp : (M →ₗ[A] N) →ₗ[A] Derivation R A M →ₗ[R] Derivation R A N where
+def llcomp : (M →ₗ[A] N) →ₗ[A] Derivation R A M →ₗ[A] Derivation R A N where
   toFun f := f.compDer
   map_add' f₁ f₂ := by ext; rfl
   map_smul' r D := by ext; rfl
 
 /-- Pushing a derivation forward through a linear equivalence is an equivalence. -/
-def _root_.LinearEquiv.compDer : Derivation R A M ≃ₗ[R] Derivation R A N :=
+def _root_.LinearEquiv.compDer : Derivation R A M ≃ₗ[A] Derivation R A N :=
   { e.toLinearMap.compDer with
     invFun := e.symm.toLinearMap.compDer
     left_inv := fun D => by ext a; exact e.symm_apply_apply (D a)

Mathlib/RingTheory/Kaehler/Basic.lean

@@ -370,7 +370,7 @@ local instance instR : Module R (KaehlerDifferential.ideal R S).cotangentIdeal :
 /-- Derivations into `Ω[S⁄R]` is equivalent to derivations
 into `(KaehlerDifferential.ideal R S).cotangentIdeal`. -/
 noncomputable def KaehlerDifferential.endEquivDerivation' :
-    Derivation R S Ω[S⁄R] ≃ₗ[R] Derivation R S (ideal R S).cotangentIdeal :=
+    Derivation R S Ω[S⁄R] ≃ₗ[S] Derivation R S (ideal R S).cotangentIdeal :=
   LinearEquiv.compDer ((KaehlerDifferential.ideal R S).cotangentEquivIdeal.restrictScalars S)
 
 /-- (Implementation) An `Equiv` version of `KaehlerDifferential.End_equiv_aux`.