From 9e71aa5dfe8a3cbe676627e604a1e7396763b770 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Oct 2024 23:53:06 +0000 Subject: [PATCH] one more --- Mathlib/LinearAlgebra/Alternating/Basic.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean index dde41ea7b541d..0ea0a6592c3b6 100644 --- a/Mathlib/LinearAlgebra/Alternating/Basic.lean +++ b/Mathlib/LinearAlgebra/Alternating/Basic.lean @@ -454,6 +454,17 @@ theorem smul_compAlternatingMap [Monoid S] [DistribMulAction S N₂] [SMulCommCl (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) : (s • g).compAlternatingMap f = s • g.compAlternatingMap f := rfl +variable (S) in +/-- `LinearMap.compAlternatingMap` as an `S`-linear map. -/ +@[simps] +def compAlternatingMapₗ [Semiring S] [Module S N] [Module S N₂] + [SMulCommClass R S N] [SMulCommClass R S N₂] [LinearMap.CompatibleSMul N N₂ S R] + (g : N →ₗ[R] N₂) : + (M [⋀^ι]→ₗ[R] N) →ₗ[S] (M [⋀^ι]→ₗ[R] N₂) where + toFun := g.compAlternatingMap + map_add' := g.compAlternatingMap_add + map_smul' := g.compAlternatingMap_smul + theorem smulRight_eq_comp {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f :=