refactor(linear_algebra/finite_dimensional): generalize finite_dimensional.iff_fg to division rings (#7644)

Replace `finite_dimensional.iff_fg` (working over a field) with `is_noetherian.iff_fg` (working over a division ring). Also, use the `module.finite` predicate.



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

Author: kim-em

src/analysis/normed_space/inner_product.lean

@@ -2817,7 +2817,7 @@ lemma orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] :
 (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2
 
 instance [finite_dimensional 𝕜 E] : fintype (orthonormal_basis_index 𝕜 E) :=
-finite_dimensional.fintype_basis_index (orthonormal_basis 𝕜 E)
+is_noetherian.fintype_basis_index (orthonormal_basis 𝕜 E)
 
 variables {𝕜 E}
 

src/data/complex/is_R_or_C.lean

@@ -626,7 +626,7 @@ library_note "is_R_or_C instance"
 
 /-- An `is_R_or_C` field is finite-dimensional over `ℝ`, since it is spanned by `{1, I}`. -/
 @[nolint dangerous_instance] instance is_R_or_C_to_real : finite_dimensional ℝ K :=
-finite_dimensional.iff_fg.mpr ⟨{1, I},
+is_noetherian.iff_fg.mpr ⟨⟨{1, I},
   begin
     rw eq_top_iff,
     intros a _,
@@ -635,7 +635,7 @@ finite_dimensional.iff_fg.mpr ⟨{1, I},
     { rw submodule.mem_span_singleton,
       use im a },
     simp [re_add_im a, algebra.smul_def, algebra_map_eq_of_real]
-  end⟩
+  end⟩⟩
 
 /-- Over an `is_R_or_C` field, we can register the properness of finite-dimensional normed spaces as
 an instance. -/

src/field_theory/finite/polynomial.lean

@@ -176,7 +176,7 @@ calc module.rank K (R σ K) =
   ... = fintype.card (σ → K) : cardinal.fintype_card _
 
 instance : finite_dimensional K (R σ K) :=
-finite_dimensional.finite_dimensional_iff_dim_lt_omega.mpr
+is_noetherian.iff_dim_lt_omega.mpr
   (by simpa only [dim_R] using cardinal.nat_lt_omega (fintype.card (σ → K)))
 
 lemma finrank_R : finite_dimensional.finrank K (R σ K) = fintype.card (σ → K) :=

src/field_theory/finiteness.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import ring_theory.finiteness
+import linear_algebra.dimension
+
+/-!
+# A module over a division ring is noetherian if and only if it is finite.
+
+-/
+
+universes u v
+
+open_locale classical
+open cardinal submodule module function
+
+namespace is_noetherian
+
+variables {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V]
+
+-- PROJECT: Show all division rings are noetherian.
+-- This is currently annoying because we only have ideal of commutative rings.
+variables [is_noetherian_ring K]
+
+/--
+A module over a division ring is noetherian if and only if
+its dimension (as a cardinal) is strictly less than the first infinite cardinal `omega`.
+-/
+lemma iff_dim_lt_omega : is_noetherian K V ↔ module.rank K V < omega.{v} :=
+begin
+  let b := basis.of_vector_space K V,
+  have := b.mk_eq_dim,
+  simp only [lift_id] at this,
+  rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ (basis.of_vector_space_index K V),
+      ← subtype.range_coe_subtype],
+  split,
+  { intro,
+    resetI,
+    simpa using finite_of_linear_independent (basis.of_vector_space_index.linear_independent K V) },
+  { assume hbfinite,
+    refine @is_noetherian_of_linear_equiv K (⊤ : submodule K V) V _
+      _ _ _ _ (linear_equiv.of_top _ rfl) (id _),
+    refine is_noetherian_of_fg_of_noetherian _ ⟨set.finite.to_finset hbfinite, _⟩,
+    rw [set.finite.coe_to_finset, ← b.span_eq, basis.coe_of_vector_space] }
+end
+
+variables (K V)
+
+/-- The dimension of a noetherian module over a division ring, as a cardinal,
+is strictly less than the first infinite cardinal `omega`. -/
+lemma dim_lt_omega : ∀ [is_noetherian K V], module.rank K V < omega.{v} :=
+is_noetherian.iff_dim_lt_omega.1
+
+variables {K V}
+
+/-- In a noetherian module over a division ring, all bases are indexed by a finite type. -/
+noncomputable def fintype_basis_index {ι : Type*} [is_noetherian K V] (b : basis ι K V) :
+  fintype ι :=
+b.fintype_index_of_dim_lt_omega (dim_lt_omega K V)
+
+/-- In a noetherian module over a division ring,
+`basis.of_vector_space` is indexed by a finite type. -/
+noncomputable instance [is_noetherian K V] : fintype (basis.of_vector_space_index K V) :=
+fintype_basis_index (basis.of_vector_space K V)
+
+/-- In a noetherian module over a division ring,
+if a basis is indexed by a set, that set is finite. -/
+lemma finite_basis_index {ι : Type*} {s : set ι} [is_noetherian K V] (b : basis s K V) :
+  s.finite :=
+b.finite_index_of_dim_lt_omega (dim_lt_omega K V)
+
+variables (K V)
+
+/-- In a noetherian module over a division ring,
+there exists a finite basis. This is the indexing `finset`. -/
+noncomputable def finset_basis_index [is_noetherian K V] :
+  finset V :=
+(finite_basis_index (basis.of_vector_space K V)).to_finset
+
+@[simp] lemma coe_finset_basis_index [is_noetherian K V] :
+  (↑(finset_basis_index K V) : set V) = basis.of_vector_space_index K V :=
+set.finite.coe_to_finset _
+
+/--
+In a noetherian module over a division ring, there exists a finite basis.
+This is indexed by the `finset` `finite_dimensional.finset_basis_index`.
+This is in contrast to the result `finite_basis_index (basis.of_vector_space K V)`,
+which provides a set and a `set.finite`.
+-/
+noncomputable def finset_basis [is_noetherian K V] :
+  basis (↑(finset_basis_index K V) : set V) K V :=
+(basis.of_vector_space K V).reindex (by simp)
+
+@[simp] lemma range_finset_basis [is_noetherian K V] :
+  set.range (finset_basis K V) = basis.of_vector_space_index K V :=
+by rw [finset_basis, basis.range_reindex, basis.range_of_vector_space]
+
+variables {K V}
+
+/-- A module over a division ring is noetherian if and only if it is finitely generated. -/
+lemma iff_fg :
+  is_noetherian K V ↔ module.finite K V :=
+begin
+  split,
+  { introI h,
+    exact ⟨⟨finset_basis_index K V, by { convert (finset_basis K V).span_eq, simp }⟩⟩ },
+  { rintros ⟨s, hs⟩,
+    rw [is_noetherian.iff_dim_lt_omega, ← dim_top, ← hs],
+    exact lt_of_le_of_lt (dim_span_le _) (lt_omega_iff_finite.2 (set.finite_mem_finset s)) }
+end
+
+end is_noetherian

src/field_theory/fixed.lean

@@ -204,7 +204,7 @@ begin
 end
 
 instance : finite_dimensional (fixed_points G F) F :=
-finite_dimensional.finite_dimensional_iff_dim_lt_omega.2 $
+is_noetherian.iff_dim_lt_omega.2 $
 lt_of_le_of_lt (dim_le_card G F) (cardinal.nat_lt_omega _)
 
 lemma finrank_le_card : finrank (fixed_points G F) F ≤ fintype.card G :=

src/field_theory/splitting_field.lean

@@ -759,12 +759,12 @@ alg_hom.comp (by { rw ← adjoin_roots L f, exact classical.choice (lift_of_spli
   algebra.to_top
 
 theorem finite_dimensional (f : polynomial K) [is_splitting_field K L f] : finite_dimensional K L :=
-finite_dimensional.iff_fg.2 $ @algebra.top_to_submodule K L _ _ _ ▸ adjoin_roots L f ▸
+is_noetherian.iff_fg.2 ⟨@algebra.top_to_submodule K L _ _ _ ▸ adjoin_roots L f ▸
   fg_adjoin_of_finite (set.finite_mem_finset _) (λ y hy,
   if hf : f = 0
   then by { rw [hf, map_zero, roots_zero] at hy, cases hy }
   else (is_algebraic_iff_is_integral _).1 ⟨f, hf, (eval₂_eq_eval_map _).trans $
-    (mem_roots $ by exact map_ne_zero hf).1 (multiset.mem_to_finset.mp hy)⟩)
+    (mem_roots $ by exact map_ne_zero hf).1 (multiset.mem_to_finset.mp hy)⟩)⟩
 
 instance (f : polynomial K) : _root_.finite_dimensional K f.splitting_field :=
 finite_dimensional f.splitting_field f

src/field_theory/tower.lean

@@ -62,15 +62,17 @@ by convert dim_mul_dim' F K A; rw lift_id
 
 namespace finite_dimensional
 
+open is_noetherian
+
 theorem trans [finite_dimensional F K] [finite_dimensional K A] : finite_dimensional F A :=
 let b := basis.of_vector_space F K, c := basis.of_vector_space K A in
 of_fintype_basis $ b.smul c
 
 lemma right [hf : finite_dimensional F A] : finite_dimensional K A :=
-let ⟨b, hb⟩ := iff_fg.1 hf in
-iff_fg.2 ⟨b, submodule.restrict_scalars_injective F _ _ $
+let ⟨⟨b, hb⟩⟩ := iff_fg.1 hf in
+iff_fg.2 ⟨⟨b, submodule.restrict_scalars_injective F _ _ $
 by { rw [submodule.restrict_scalars_top, eq_top_iff, ← hb, submodule.span_le],
-  exact submodule.subset_span }⟩
+  exact submodule.subset_span }⟩⟩
 
 /-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then
 `dim_F(A) = dim_F(K) * dim_K(A)`. -/

src/linear_algebra/dimension.lean

@@ -168,6 +168,32 @@ cardinal.card_le_of (λ s, @finset.card_map _ _ ⟨_, subtype.val_injective⟩ s
 H _ (by { refine (of_vector_space_index.linear_independent K V).mono (λ y h, _),
           rw [finset.mem_coe, finset.mem_map] at h, rcases h with ⟨x, hx, rfl⟩, exact x.2 }))
 
+/-- If a vector space has a finite dimension, all bases are indexed by a finite type. -/
+lemma basis.nonempty_fintype_index_of_dim_lt_omega {ι : Type*}
+  (b : basis ι K V) (h : module.rank K V < cardinal.omega) :
+  nonempty (fintype ι) :=
+by rwa [← cardinal.lift_lt, ← b.mk_eq_dim,
+        -- ensure `omega` has the correct universe
+        cardinal.lift_omega, ← cardinal.lift_omega.{u_1 v},
+        cardinal.lift_lt, cardinal.lt_omega_iff_fintype] at h
+
+/-- If a vector space has a finite dimension, all bases are indexed by a finite type. -/
+noncomputable def basis.fintype_index_of_dim_lt_omega {ι : Type*}
+  (b : basis ι K V) (h : module.rank K V < cardinal.omega) :
+  fintype ι :=
+classical.choice (b.nonempty_fintype_index_of_dim_lt_omega h)
+
+/-- If a vector space has a finite dimension, all bases are indexed by a finite set. -/
+lemma basis.finite_index_of_dim_lt_omega {ι : Type*} {s : set ι}
+  (b : basis s K V) (h : module.rank K V < cardinal.omega) :
+  s.finite :=
+b.nonempty_fintype_index_of_dim_lt_omega h
+
+/-- If a vector space has a finite dimension, the index set of `basis.of_vector_space` is finite. -/
+lemma basis.finite_of_vector_space_index_of_dim_lt_omega (h : module.rank K V < cardinal.omega) :
+  (basis.of_vector_space_index K V).finite :=
+(basis.of_vector_space K V).nonempty_fintype_index_of_dim_lt_omega h
+
 variables [add_comm_group V'] [module K V']
 
 /-- Two linearly equivalent vector spaces have the same dimension, a version with different
@@ -485,32 +511,6 @@ lemma exists_mem_ne_zero_of_dim_pos {s : submodule K V} (h : 0 < module.rank K s
   ∃ b : V, b ∈ s ∧ b ≠ 0 :=
 exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [eq, dim_bot] at h; exact lt_irrefl _ h
 
-/-- If a vector space has a finite dimension, all bases are indexed by a finite type. -/
-lemma basis.nonempty_fintype_index_of_dim_lt_omega {ι : Type*}
-  (b : basis ι K V) (h : module.rank K V < cardinal.omega) :
-  nonempty (fintype ι) :=
-by rwa [← cardinal.lift_lt, ← b.mk_eq_dim,
-        -- ensure `omega` has the correct universe
-        cardinal.lift_omega, ← cardinal.lift_omega.{u_1 v},
-        cardinal.lift_lt, cardinal.lt_omega_iff_fintype] at h
-
-/-- If a vector space has a finite dimension, all bases are indexed by a finite type. -/
-noncomputable def basis.fintype_index_of_dim_lt_omega {ι : Type*}
-  (b : basis ι K V) (h : module.rank K V < cardinal.omega) :
-  fintype ι :=
-classical.choice (b.nonempty_fintype_index_of_dim_lt_omega h)
-
-/-- If a vector space has a finite dimension, all bases are indexed by a finite set. -/
-lemma basis.finite_index_of_dim_lt_omega {ι : Type*} {s : set ι}
-  (b : basis s K V) (h : module.rank K V < cardinal.omega) :
-  s.finite :=
-b.nonempty_fintype_index_of_dim_lt_omega h
-
-/-- If a vector space has a finite dimension, the index set of `basis.of_vector_space` is finite. -/
-lemma basis.finite_of_vector_space_index_of_dim_lt_omega (h : module.rank K V < cardinal.omega) :
-  (basis.of_vector_space_index K V).finite :=
-(basis.of_vector_space K V).nonempty_fintype_index_of_dim_lt_omega h
-
 section rank
 
 /-- `rank f` is the rank of a `linear_map f`, defined as the dimension of `f.range`. -/

src/linear_algebra/dual.lean

@@ -198,8 +198,8 @@ lemma total_dual_basis [fintype ι] (f : ι →₀ R) (i : ι) :
   finsupp.total ι (dual R M) R b.dual_basis f (b i) = f i :=
 begin
   rw [finsupp.total_apply, finsupp.sum_fintype, linear_map.sum_apply],
-  { simp_rw [smul_apply, smul_eq_mul, dual_basis_apply_self, mul_boole,
-             finset.sum_ite_eq, if_pos (finset.mem_univ i)] },
+  { simp_rw [linear_map.smul_apply, smul_eq_mul, dual_basis_apply_self, mul_boole,
+      finset.sum_ite_eq, if_pos (finset.mem_univ i)] },
   { intro, rw zero_smul },
 end