feat: algebraic properties of LinearMap.compMultilinear

This also demotes `LinearMap.compAlternatingMap` to a plain function, for consistency.

Mathlib/LinearAlgebra/Alternating/Basic.lean

@@ -407,19 +407,42 @@ end AlternatingMap
 
 namespace LinearMap
 
-variable {N₂ : Type*} [AddCommMonoid N₂] [Module R N₂]
+variable {S : Type*} {N₂ : Type*} [AddCommMonoid N₂] [Module R N₂]
 
 /-- Composing an alternating map with a linear map on the left gives again an alternating map. -/
-def compAlternatingMap (g : N →ₗ[R] N₂) : (M [⋀^ι]→ₗ[R] N) →+ (M [⋀^ι]→ₗ[R] N₂) where
-  toFun f :=
-    { g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N) with
-      map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }
-  map_zero' := by
-    ext
-    simp
-  map_add' a b := by
-    ext
-    simp
+def compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι]→ₗ[R] N₂ where
+  __ := g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N)
+  map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij]
+
+@[simp]
+theorem compAlternatingMap_zero (g : N →ₗ[R] N₂) :
+    g.compAlternatingMap (0 : M [⋀^ι]→ₗ[R] N) = 0 :=
+  AlternatingMap.ext fun _ => map_zero g
+
+@[simp]
+theorem zero_compAlternatingMap (f: M [⋀^ι]→ₗ[R] N) :
+    (0 : N →ₗ[R] N₂).compAlternatingMap f = 0 := rfl
+
+@[simp]
+theorem compAlternatingMap_add (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N) :
+    g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂ :=
+  AlternatingMap.ext fun _ => map_add g _ _
+
+@[simp]
+theorem add_compAlternatingMap (g₁ g₂ : N →ₗ[R] N₂) (f: M [⋀^ι]→ₗ[R] N) :
+    (g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f := rfl
+
+@[simp]
+theorem compAlternatingMap_smul [Monoid S] [DistribMulAction S N] [DistribMulAction S N₂]
+    [SMulCommClass R S N] [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R]
+    (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
+    g.compAlternatingMap (s • f) = s • g.compAlternatingMap f :=
+  AlternatingMap.ext fun _ => g.map_smul_of_tower _ _
+
+@[simp]
+theorem smul_compAlternatingMap [Monoid S] [DistribMulAction S N₂] [SMulCommClass R S N₂]
+    (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
+    (s • g).compAlternatingMap f = s • g.compAlternatingMap f := rfl
 
 @[simp]
 theorem coe_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -787,6 +787,36 @@ theorem compMultilinearMap_apply (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R
     g.compMultilinearMap f m = g (f m) :=
   rfl
 
+@[simp]
+theorem compMultilinearMap_zero (g : M₂ →ₗ[R] M₃) :
+    g.compMultilinearMap (0 : MultilinearMap R M₁ M₂) = 0 :=
+  MultilinearMap.ext fun _ => map_zero g
+
+@[simp]
+theorem zero_compMultilinearMap (f: MultilinearMap R M₁ M₂) :
+    (0 : M₂ →ₗ[R] M₃).compMultilinearMap f = 0 := rfl
+
+@[simp]
+theorem compMultilinearMap_add (g : M₂ →ₗ[R] M₃) (f₁ f₂ : MultilinearMap R M₁ M₂) :
+    g.compMultilinearMap (f₁ + f₂) = g.compMultilinearMap f₁ + g.compMultilinearMap f₂ :=
+  MultilinearMap.ext fun _ => map_add g _ _
+
+@[simp]
+theorem add_compMultilinearMap (g₁ g₂ : M₂ →ₗ[R] M₃) (f: MultilinearMap R M₁ M₂) :
+    (g₁ + g₂).compMultilinearMap f = g₁.compMultilinearMap f + g₂.compMultilinearMap f := rfl
+
+@[simp]
+theorem compMultilinearMap_smul [Monoid S] [DistribMulAction S M₂] [DistribMulAction S M₃]
+    [SMulCommClass R S M₂] [SMulCommClass R S M₃] [CompatibleSMul M₂ M₃ S R]
+    (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
+    g.compMultilinearMap (s • f) = s • g.compMultilinearMap f :=
+  MultilinearMap.ext fun _ => g.map_smul_of_tower _ _
+
+@[simp]
+theorem smul_compMultilinearMap [Monoid S] [DistribMulAction S M₃] [SMulCommClass R S M₃]
+    (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
+    (s • g).compMultilinearMap f = s • g.compMultilinearMap f := rfl
+
 /-- The multilinear version of `LinearMap.subtype_comp_codRestrict` -/
 @[simp]
 theorem subtype_compMultilinearMap_codRestrict (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂)