feat(linear_algebra): A-linear maps between finite dimensional vector…

… spaces over k are finite dimensional (#13934)






Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/module/algebra.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.module.basic
+import algebra.algebra.basic
+
+/-!
+# Additional facts about modules over algebras.
+-/
+
+namespace linear_map
+
+section restrict_scalars
+
+variables (k : Type*) [comm_semiring k] (A : Type*) [semiring A] [algebra k A]
+variables (M : Type*) [add_comm_monoid M] [module k M] [module A M] [is_scalar_tower k A M]
+variables (N : Type*) [add_comm_monoid N] [module k N] [module A N] [is_scalar_tower k A N]
+
+/--
+Restriction of scalars for linear maps between modules over a `k`-algebra is itself `k`-linear.
+-/
+@[simps]
+def restrict_scalars_linear_map : (M →ₗ[A] N) →ₗ[k] (M →ₗ[k] N) :=
+{ to_fun := linear_map.restrict_scalars k,
+  map_add' := by tidy,
+  map_smul' := by tidy, }
+
+end restrict_scalars
+
+end linear_map

src/linear_algebra/matrix/to_lin.lean

@@ -7,6 +7,7 @@ import data.matrix.block
 import linear_algebra.matrix.finite_dimensional
 import linear_algebra.std_basis
 import ring_theory.algebra_tower
+import algebra.module.algebra
 
 /-!
 # Linear maps and matrices
@@ -593,10 +594,23 @@ variables {K : Type*} [field K]
 variables {V : Type*} [add_comm_group V] [module K V] [finite_dimensional K V]
 variables {W : Type*} [add_comm_group W] [module K W] [finite_dimensional K W]
 
-instance : finite_dimensional K (V →ₗ[K] W) :=
+instance finite_dimensional : finite_dimensional K (V →ₗ[K] W) :=
 linear_equiv.finite_dimensional
   (linear_map.to_matrix (basis.of_vector_space K V) (basis.of_vector_space K W)).symm
 
+section
+
+variables {A : Type*} [ring A] [algebra K A] [module A V] [is_scalar_tower K A V]
+  [module A W] [is_scalar_tower K A W]
+
+/-- Linear maps over a `k`-algebra are finite dimensional (over `k`) if both the source and
+target are, since they form a subspace of all `k`-linear maps. -/
+instance finite_dimensional' : finite_dimensional K (V →ₗ[A] W) :=
+finite_dimensional.of_injective (restrict_scalars_linear_map K A V W)
+  (restrict_scalars_injective _)
+
+end
+
 /--
 The dimension of the space of linear transformations is the product of the dimensions of the
 domain and codomain.