feat(linear_algebra/multilinear/basic): the space of multilinear maps…

… is finite-dimensional when the components are finite-dimensional (#10504)

Formalized as part of the Sphere Eversion project.

src/linear_algebra/multilinear/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import linear_algebra.basic
+import linear_algebra.matrix.to_lin
 import algebra.algebra.basic
 import algebra.big_operators.order
 import algebra.big_operators.ring
@@ -713,6 +714,8 @@ def dom_dom_congr_linear_equiv {ι₁ ι₂} [decidable_eq ι₁] [decidable_eq
   .. (dom_dom_congr_equiv σ : multilinear_map A (λ i : ι₁, M₂) M₃ ≃+
         multilinear_map A (λ i : ι₂, M₂) M₃) }
 
+variables (R M₁)
+
 /-- The dependent version of `multilinear_map.dom_dom_congr_linear_equiv`. -/
 @[simps apply symm_apply]
 def dom_dom_congr_linear_equiv' {ι' : Type*} [decidable_eq ι'] (σ : ι ≃ ι') :
@@ -1256,14 +1259,14 @@ end multilinear_map
 
 end currying
 
+namespace multilinear_map
+
 section submodule
 
 variables {R M M₂}
 [ring R] [∀i, add_comm_monoid (M₁ i)] [add_comm_monoid M'] [add_comm_monoid M₂]
 [∀i, module R (M₁ i)] [module R M'] [module R M₂]
 
-namespace multilinear_map
-
 /-- The pushforward of an indexed collection of submodule `p i ⊆ M₁ i` by `f : M₁ → M₂`.
 
 Note that this is not a submodule - it is not closed under addition. -/
@@ -1285,6 +1288,30 @@ lemma map_nonempty [nonempty ι] (f : multilinear_map R M₁ M₂) (p : Π i, su
 def range [nonempty ι] (f : multilinear_map R M₁ M₂) : sub_mul_action R M₂ :=
 f.map (λ i, ⊤)
 
-end multilinear_map
-
 end submodule
+
+section finite_dimensional
+
+variables [fintype ι] [field R] [add_comm_group M₂] [module R M₂] [finite_dimensional R M₂]
+variables [∀ i, add_comm_group (M₁ i)] [∀ i, module R (M₁ i)] [∀ i, finite_dimensional R (M₁ i)]
+
+instance : finite_dimensional R (multilinear_map R M₁ M₂) :=
+begin
+  suffices : ∀ n (N : fin n → Type*) [∀ i, add_comm_group (N i)],
+    by exactI ∀ [∀ i, module R (N i)], by exactI ∀ [∀ i, finite_dimensional R (N i)],
+    finite_dimensional R (multilinear_map R N M₂),
+  { haveI := this _ (M₁ ∘ (fintype.equiv_fin ι).symm),
+    have e := dom_dom_congr_linear_equiv' R M₁ M₂ (fintype.equiv_fin ι),
+    exact e.symm.finite_dimensional, },
+  intros,
+  tactic.unfreeze_local_instances,
+  induction n with n ih,
+  { exact (const_linear_equiv_of_is_empty R N M₂ : _).finite_dimensional, },
+  { suffices : finite_dimensional R (N 0 →ₗ[R] multilinear_map R (λ (i : fin n), N i.succ) M₂),
+    { exact (multilinear_curry_left_equiv R N M₂).finite_dimensional, },
+    apply linear_map.finite_dimensional, },
+end
+
+end finite_dimensional
+
+end multilinear_map