feat(linear_algebra/multilinear/finite_dimensional): generalize to finite and free (#14199)

This also renames some `free` and `finite` instances which had garbage names.

Author: eric-wieser

src/linear_algebra/free_module/basic.lean

@@ -128,6 +128,10 @@ instance self : module.free R R := of_basis $ basis.singleton unit R
 instance of_subsingleton [subsingleton N] : module.free R N :=
 of_basis (basis.empty N : basis pempty R N)
 
+@[priority 100]
+instance of_subsingleton' [subsingleton R] : module.free R N :=
+by letI := module.subsingleton R N; exact module.free.of_subsingleton R N
+
 instance dfinsupp {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_monoid (M i)]
   [Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] : module.free R (Π₀ i, M i) :=
 of_basis $ dfinsupp.basis $ λ i, choose_basis R (M i)

src/linear_algebra/free_module/finite/basic.lean

@@ -50,8 +50,10 @@ section comm_ring
 variables [comm_ring R] [add_comm_group M] [module R M] [module.free R M]
 variables [add_comm_group N] [module R N] [module.free R N]
 
-instance [nontrivial R] [module.finite R M] [module.finite R N] : module.free R (M →ₗ[R] N) :=
+instance linear_map [module.finite R M] [module.finite R N] : module.free R (M →ₗ[R] N) :=
 begin
+  casesI subsingleton_or_nontrivial R,
+  { apply module.free.of_subsingleton' },
   classical,
   exact of_equiv
     (linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R N)).symm,
@@ -72,9 +74,13 @@ instance _root_.module.finite.matrix {ι₁ : Type*} [fintype ι₁] {ι₂ : Ty
   module.finite R (matrix ι₁ ι₂ R) :=
 module.finite.of_basis $ pi.basis $ λ i, pi.basis_fun R _
 
-instance [nontrivial R] [module.finite R M] [module.finite R N] :
+variables (M)
+
+instance _root_.module.finite.linear_map [module.finite R M] [module.finite R N] :
   module.finite R (M →ₗ[R] N) :=
 begin
+  casesI subsingleton_or_nontrivial R,
+  { apply_instance },
   classical,
   have f := (linear_map.to_matrix (choose_basis R M) (choose_basis R N)).symm,
   exact module.finite.of_surjective f.to_linear_map (linear_equiv.surjective f),
@@ -87,11 +93,14 @@ section integer
 variables [add_comm_group M] [module.finite ℤ M] [module.free ℤ M]
 variables [add_comm_group N] [module.finite ℤ N] [module.free ℤ N]
 
-instance : module.finite ℤ (M →+ N) :=
+instance _root_.module.finite.add_monoid_hom : module.finite ℤ (M →+ N) :=
 module.finite.equiv (add_monoid_hom_lequiv_int ℤ).symm
 
-instance : module.free ℤ (M →+ N) :=
-module.free.of_equiv (add_monoid_hom_lequiv_int ℤ).symm
+instance add_monoid_hom : module.free ℤ (M →+ N) :=
+begin
+  letI : module.free ℤ (M →ₗ[ℤ] N) := module.free.linear_map _ _ _,
+  exact module.free.of_equiv (add_monoid_hom_lequiv_int ℤ).symm
+end
 
 end integer
 

src/linear_algebra/multilinear/finite_dimensional.lean

@@ -4,38 +4,59 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import linear_algebra.multilinear.basic
-import linear_algebra.matrix.to_lin
+import linear_algebra.free_module.finite.basic
 
 /-! # Multilinear maps over finite dimensional spaces
 
-The main result of this file is `multilinear_map.finite_dimensional`.
+The main results are that multilinear maps over finitely-generated, free modules are
+finitely-generated and free.
 
-We do not put this in `linear_algebra/multilinear_map/basic`, as `matrix.to_lin` pulls in a lot of
-imports, which can cause timeouts downstream.
+* `module.finite.multilinear_map`
+* `module.free.multilinear_map`
+
+We do not put this in `linear_algebra/multilinear_map/basic` to avoid making the imports too large
+there.
 -/
 
 namespace multilinear_map
 
 variables {ι R M₂ : Type*} {M₁ : ι → Type*}
 variables [decidable_eq ι]
-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)]
+variables [fintype ι] [comm_ring R] [add_comm_group M₂] [module R M₂]
+variables [Π i, add_comm_group (M₁ i)] [Π i, module R (M₁ i)]
+variables [module.finite R M₂] [module.free R M₂]
+variables [∀ i, module.finite R (M₁ i)] [∀ i, module.free R (M₁ i)]
 
-instance : finite_dimensional R (multilinear_map R M₁ M₂) :=
+-- the induction requires us to show both at once
+private lemma free_and_finite :
+  module.free R (multilinear_map R M₁ M₂) ∧ module.finite 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),
+  -- the `fin n` case is sufficient
+  suffices : ∀ n (N : fin n → Type*) [Π i, add_comm_group (N i)],
+    by exactI ∀ [Π i, module R (N i)],
+    by exactI ∀ [∀ i, module.finite R (N i)] [∀ i, module.free R (N i)],
+      module.free R (multilinear_map R N M₂) ∧ module.finite R (multilinear_map R N M₂),
+  { casesI 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,
-  induction n with n ih,
-  { exactI (const_linear_equiv_of_is_empty R N M₂ : _).finite_dimensional, },
-  { resetI,
-    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, },
+    exact ⟨module.free.of_equiv e.symm, module.finite.equiv e.symm⟩, },
+  introsI n N _ _ _ _,
+  unfreezingI { induction n with n ih },
+  { exact ⟨module.free.of_equiv (const_linear_equiv_of_is_empty R N M₂),
+           module.finite.equiv (const_linear_equiv_of_is_empty R N M₂)⟩ },
+  { suffices :
+      module.free R (N 0 →ₗ[R] multilinear_map R (λ (i : fin n), N i.succ) M₂) ∧
+      module.finite R (N 0 →ₗ[R] multilinear_map R (λ (i : fin n), N i.succ) M₂),
+    { casesI this,
+      exact ⟨module.free.of_equiv (multilinear_curry_left_equiv R N M₂),
+            module.finite.equiv (multilinear_curry_left_equiv R N M₂)⟩ },
+    casesI ih (λ i, N i.succ),
+    exact ⟨module.free.linear_map _ _ _, module.finite.linear_map _ _⟩ },
 end
 
+instance _root_.module.finite.multilinear_map : module.finite R (multilinear_map R M₁ M₂) :=
+free_and_finite.2
+
+instance _root_.module.free.multilinear_map : module.free R (multilinear_map R M₁ M₂) :=
+free_and_finite.1
+
 end multilinear_map

src/ring_theory/noetherian.lean

@@ -674,17 +674,22 @@ lemma is_noetherian_ring_iff_ideal_fg (R : Type*) [semiring R] :
 is_noetherian_ring_iff.trans is_noetherian_def
 
 @[priority 80] -- see Note [lower instance priority]
-instance ring.is_noetherian_of_fintype (R M) [fintype M] [semiring R] [add_comm_monoid M]
-  [module R M] :
+instance is_noetherian_of_fintype (R M) [fintype M] [semiring R] [add_comm_monoid M] [module R M] :
   is_noetherian R M :=
 by letI := classical.dec; exact
 ⟨assume s, ⟨to_finset s, by rw [set.coe_to_finset, submodule.span_eq]⟩⟩
 
-theorem ring.is_noetherian_of_zero_eq_one {R} [semiring R] (h01 : (0 : R) = 1) :
+/-- Modules over the trivial ring are Noetherian. -/
+@[priority 100] -- see Note [lower instance priority]
+instance is_noetherian_of_subsingleton (R M) [subsingleton R] [semiring R] [add_comm_monoid M]
+  [module R M] : is_noetherian R M :=
+by haveI := module.subsingleton R M;
+   exact is_noetherian_of_fintype R M
+
+@[priority 100] -- see Note [lower instance priority]
+instance ring.is_noetherian_of_subsingleton {R} [semiring R] [subsingleton R] :
   is_noetherian_ring R :=
-by haveI := subsingleton_of_zero_eq_one h01;
-   haveI := fintype.of_subsingleton (0:R);
-   exact is_noetherian_ring_iff.2 (ring.is_noetherian_of_fintype R R)
+⟨⟩
 
 theorem is_noetherian_of_submodule_of_noetherian (R M) [semiring R] [add_comm_monoid M] [module R M]
   (N : submodule R M) (h : is_noetherian R M) : is_noetherian R N :=