feat(linear_algebra/finite_dimensional): finite dimensional vector sp…

…aces (#1241)

* feat(linear_algebra/finite_dimensional): finite dimensional vector spaces

* rw `of_span_finite_eq_top` to `of_fg`

* prove infinite.nat_embedding

* generalize finite_of_linear_independent to noetherian modules

* fix build

* fix build (ring_theory/polynomial)

src/data/fintype.lean

@@ -6,6 +6,7 @@ Author: Mario Carneiro
 Finite types.
 -/
 import data.finset algebra.big_operators data.array.lemmas logic.unique
+import tactic.wlog
 universes u v
 
 variables {α : Type*} {β : Type*} {γ : Type*}
@@ -723,6 +724,30 @@ lemma of_injective [infinite β] (f : β → α) (hf : injective f) : infinite 
 lemma of_surjective [infinite β] (f : α → β) (hf : surjective f) : infinite α :=
 ⟨λ I, by classical; exactI not_fintype (fintype.of_surjective f hf)⟩
 
+private noncomputable def nat_embedding_aux (α : Type*) [infinite α] : ℕ → α
+| n := by letI := classical.dec_eq α; exact classical.some (exists_not_mem_finset
+  ((multiset.range n).pmap (λ m (hm : m < n), nat_embedding_aux m)
+    (λ _, multiset.mem_range.1)).to_finset)
+
+private lemma nat_embedding_aux_injective (α : Type*) [infinite α] :
+  function.injective (nat_embedding_aux α) :=
+begin
+  assume m n h,
+  letI := classical.dec_eq α,
+  wlog hmlen : m ≤ n using m n,
+  by_contradiction hmn,
+  have hmn : m < n, from lt_of_le_of_ne hmlen hmn,
+  refine (classical.some_spec (exists_not_mem_finset
+    ((multiset.range n).pmap (λ m (hm : m < n), nat_embedding_aux α m)
+      (λ _, multiset.mem_range.1)).to_finset)) _,
+  refine multiset.mem_to_finset.2 (multiset.mem_pmap.2
+    ⟨m, multiset.mem_range.2 hmn, _⟩),
+  rw [h, nat_embedding_aux]
+end
+
+noncomputable def nat_embedding (α : Type*) [infinite α] : ℕ ↪ α :=
+⟨_, nat_embedding_aux_injective α⟩
+
 end infinite
 
 instance nat.infinite : infinite ℕ :=

src/linear_algebra/basis.lean

@@ -486,12 +486,12 @@ begin
   exact hi'.2
 end
 
-lemma eq_of_linear_independent_of_span_subtype {s t : set β} (zero_ne_one : (1 : α) ≠ 0)
+lemma eq_of_linear_independent_of_span_subtype {s t : set β} (zero_ne_one : (0 : α) ≠ 1)
   (hs : linear_independent α (λ x, x : s → β)) (h : t ⊆ s) (hst : s ⊆ span α t) : s = t :=
 begin
   let f : t ↪ s := ⟨λ x, ⟨x.1, h x.2⟩, λ a b hab, subtype.val_injective (subtype.mk.inj hab)⟩,
   have h_surj : surjective f,
-  { apply surjective_of_linear_independent_of_span hs f _ zero_ne_one.symm,
+  { apply surjective_of_linear_independent_of_span hs f _ zero_ne_one,
     convert hst; simp [f, comp], },
   show s = t,
   { apply subset.antisymm _ h,
@@ -570,6 +570,22 @@ begin
         apply linear_map.map_le_range } } }
 end
 
+lemma le_of_span_le_span {s t u: set β} (zero_ne_one : (0 : α) ≠ 1)
+  (hl : linear_independent α (subtype.val : u → β )) (hsu : s ⊆ u) (htu : t ⊆ u)
+  (hst : span α s ≤ span α t) : s ⊆ t :=
+begin
+  have := eq_of_linear_independent_of_span_subtype zero_ne_one
+    (hl.mono (set.union_subset hsu htu))
+    (set.subset_union_right _ _)
+    (set.union_subset (set.subset.trans subset_span hst) subset_span),
+  rw ← this, apply set.subset_union_left
+end
+
+lemma span_le_span_iff {s t u: set β} (zero_ne_one : (0 : α) ≠ 1)
+  (hl : linear_independent α (subtype.val : u → β )) (hsu : s ⊆ u) (htu : t ⊆ u) :
+  span α s ≤ span α t ↔ s ⊆ t :=
+⟨le_of_span_le_span zero_ne_one hl hsu htu, span_mono⟩
+
 variables (α) (v)
 /-- A set of vectors is a basis if it is linearly independent and all vectors are in the span α. -/
 def is_basis := linear_independent α v ∧ span α (range v) = ⊤
@@ -876,7 +892,7 @@ have ∀t, ∀(s' : finset β), ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ (span
 assume t, finset.induction_on t
   (assume s' hs' _ hss',
     have s = ↑s',
-      from eq_of_linear_independent_of_span_subtype (@one_ne_zero α _) hs hs' $
+      from eq_of_linear_independent_of_span_subtype (@zero_ne_one α _) hs hs' $
           by simpa using hss',
     ⟨s', by simp [this]⟩)
   (assume b₁ t hb₁t ih s' hs' hst hss',

src/linear_algebra/dimension.lean

@@ -112,11 +112,14 @@ letI := classical.dec_eq γ; exact
 let ⟨b, hb⟩ := exists_is_basis α β in
 cardinal.lift_inj.1 $ hb.mk_eq_dim.symm.trans (f.is_basis hb).mk_eq_dim
 
-lemma dim_bot : dim α (⊥ : submodule α β) = 0 :=
+@[simp] lemma dim_bot : dim α (⊥ : submodule α β) = 0 :=
 by letI := classical.dec_eq β;
   rw [← cardinal.lift_inj, ← (@is_basis_empty_bot pempty α β _ _ _ _ _ _ nonempty_pempty).mk_eq_dim,
     cardinal.mk_pempty]
 
+@[simp] lemma dim_top : dim α (⊤ : submodule α β) = dim α β :=
+linear_equiv.dim_eq (linear_equiv.of_top _ rfl)
+
 lemma dim_of_field (α : Type*) [discrete_field α] : dim α α = 1 :=
 by rw [←cardinal.lift_inj, ← (@is_basis_singleton_one punit _ α _ _ _).mk_eq_dim, cardinal.mk_punit]
 

src/linear_algebra/finite_dimensional.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+
+Definition and basic properties of finite dimensional vector spaces.
+
+The class `finite_dimensional` is defined to be `is_noetherian`, for ease of transfer of proofs.
+However an additional constructor `finite_dimensional.of_fg` is provided to prove
+finite dimensionality in a conventional manner.
+
+Also defined is `findim`, the dimension of a finite dimensional space, returning a `nat`,
+as opposed to `dim`, which returns a `cardinal`,
+-/
+
+import ring_theory.noetherian linear_algebra.dimension
+import ring_theory.principal_ideal_domain
+
+universes u v w
+
+open vector_space cardinal submodule module function
+
+variables {K : Type u} {V : Type v} [discrete_field K] [add_comm_group V] [vector_space K V]
+
+/-- `finite_dimensional` vector spaces are defined to be noetherian modules.
+  Use `finite_dimensional.of_fg` to prove finite dimensional from a conventional
+  definition. -/
+@[reducible] def finite_dimensional (K V : Type*) [discrete_field K]
+  [add_comm_group V] [vector_space K V] := is_noetherian K V
+
+namespace finite_dimensional
+
+open is_noetherian
+
+lemma finite_dimensional_iff_dim_lt_omega : finite_dimensional K V ↔ dim K V < omega.{v} :=
+begin
+  letI := classical.dec_eq V,
+  cases exists_is_basis K V with b hb,
+  have := is_basis.mk_eq_dim hb,
+  simp only [lift_id] at this,
+  rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ b, ← subtype.val_range],
+  split,
+  { intro, convert finite_of_linear_independent hb.1, simp },
+  { 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, ← hb.2], refl }
+end
+
+lemma dim_lt_omega (K V : Type*) [discrete_field K] [add_comm_group V] [vector_space K V] :
+  ∀ [finite_dimensional K V], dim K V < omega.{v} :=
+finite_dimensional_iff_dim_lt_omega.1
+
+set_option pp.universes true
+
+lemma of_fg [decidable_eq V] (hfg : (⊤ : submodule K V).fg) : finite_dimensional K V :=
+let ⟨s, hs⟩ := hfg in
+begin
+  rw [finite_dimensional_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
+
+lemma exists_is_basis_finite (K V : Type*) [discrete_field K]
+  [add_comm_group V] [vector_space K V] [finite_dimensional K V] [decidable_eq V] :
+  ∃ s : set V, (is_basis K (subtype.val : s → V)) ∧ s.finite :=
+begin
+  cases exists_is_basis K V with s hs,
+  exact ⟨s, hs, finite_of_linear_independent hs.1⟩
+end
+
+instance [finite_dimensional K V] (S : submodule K V) : finite_dimensional K S :=
+finite_dimensional_iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))
+
+noncomputable def findim (K V : Type*) [discrete_field K]
+  [add_comm_group V] [vector_space K V] [finite_dimensional K V] : ℕ :=
+classical.some (lt_omega.1 (dim_lt_omega K V))
+
+lemma findim_eq_dim (K : Type u) (V : Type v) [discrete_field K]
+  [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
+  (findim K V : cardinal.{v}) = dim K V :=
+(classical.some_spec (lt_omega.1 (dim_lt_omega K V))).symm
+
+lemma card_eq_findim [finite_dimensional K V] [decidable_eq V] {s : set V} {hfs : fintype s}
+  (hs : is_basis K (λ x : s, x.val)) : fintype.card s = findim K V :=
+by rw [← nat_cast_inj.{v}, findim_eq_dim, ← fintype_card, ← lift_inj, ← hs.mk_eq_dim]
+
+lemma eq_top_of_findim_eq [finite_dimensional K V] {S : submodule K V}
+  (h : findim K S = findim K V) : S = ⊤ :=
+begin
+  letI := classical.dec_eq V,
+  cases exists_is_basis K S with bS hbS,
+  have : linear_independent K (subtype.val : (subtype.val '' bS : set V) → V),
+    from @linear_independent.image_subtype _ _ _ _ _ _ _ _ _ _ _ _
+      (submodule.subtype S) hbS.1 (by simp),
+  cases exists_subset_is_basis this with b hb,
+  letI : fintype b := classical.choice (finite_of_linear_independent hb.2.1),
+  letI : fintype (subtype.val '' bS) := classical.choice (finite_of_linear_independent this),
+  letI : fintype bS := classical.choice (finite_of_linear_independent hbS.1),
+  have : subtype.val '' bS = b, from set.eq_of_subset_of_card_le hb.1
+    (by rw [set.card_image_of_injective _ subtype.val_injective, card_eq_findim hbS,
+         card_eq_findim hb.2, h]; apply_instance),
+  erw [← hb.2.2, subtype.val_range, ← this, set.set_of_mem_eq, ← subtype_eq_val, span_image],
+  have := hbS.2,
+  erw [subtype.val_range, set.set_of_mem_eq] at this,
+  rw [this, map_top (submodule.subtype S), range_subtype],
+end
+
+end finite_dimensional
+
+namespace linear_map
+
+open finite_dimensional
+
+lemma surjective_of_injective [finite_dimensional K V] {f : V →ₗ[K] V}
+  (hinj : injective f) : surjective f :=
+begin
+  have h := dim_eq_injective _ hinj,
+  rw [← findim_eq_dim, ← findim_eq_dim, nat_cast_inj] at h,
+  exact range_eq_top.1 (eq_top_of_findim_eq h.symm)
+end
+
+lemma injective_iff_surjective [finite_dimensional K V] {f : V →ₗ[K] V} :
+  injective f ↔ surjective f :=
+by classical; exact
+⟨surjective_of_injective,
+  λ hsurj, let ⟨g, hg⟩ := exists_right_inverse_linear_map_of_surjective
+    (range_eq_top.2 hsurj) in
+  have function.right_inverse g f,
+    from λ x, show (linear_map.comp f g) x = (@linear_map.id K V _ _ _ : V → V) x, by rw hg,
+  injective_of_has_left_inverse ⟨g, left_inverse_of_surjective_of_right_inverse
+    (surjective_of_injective (injective_of_has_left_inverse ⟨_, this⟩))
+      this⟩⟩
+
+lemma ker_eq_bot_iff_range_eq_top [finite_dimensional K V] {f : V →ₗ[K] V} :
+  f.ker = ⊥ ↔ f.range = ⊤ :=
+by rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
+
+lemma mul_eq_one_of_mul_eq_one [finite_dimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) :
+  g * f = 1 :=
+by classical; exact
+have ginj : injective g, from injective_of_has_left_inverse
+  ⟨f, λ x, show (f * g) x = (1 : V →ₗ[K] V) x, by rw hfg; refl⟩,
+let ⟨i, hi⟩ := exists_right_inverse_linear_map_of_surjective
+  (range_eq_top.2 (injective_iff_surjective.1 ginj)) in
+have f * (g * i) = f * 1, from congr_arg _ hi,
+by rw [← mul_assoc, hfg, one_mul, mul_one] at this; rwa ← this
+
+lemma mul_eq_one_comm [finite_dimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1 :=
+⟨mul_eq_one_of_mul_eq_one, mul_eq_one_of_mul_eq_one⟩
+
+end linear_map

src/ring_theory/noetherian.lean

@@ -8,6 +8,7 @@ import data.equiv.algebra
 import linear_algebra.finsupp
 import ring_theory.ideal_operations
 import ring_theory.subring
+import linear_algebra.basis
 
 open set lattice
 
@@ -234,7 +235,7 @@ end
 
 end
 
-open is_noetherian
+open is_noetherian submodule function
 
 theorem is_noetherian_iff_well_founded
   {α β} [ring α] [add_comm_group β] [module α β] :
@@ -289,10 +290,31 @@ theorem is_noetherian_iff_well_founded
       rw [← hs₂, sup_assoc, ← submodule.span_union], simp }
   end⟩
 
-lemma well_founded_submodule_gt {α β} [ring α] [add_comm_group β] [module α β] :
+lemma well_founded_submodule_gt (α β) [ring α] [add_comm_group β] [module α β] :
   ∀ [is_noetherian α β], well_founded ((>) : submodule α β → submodule α β → Prop) :=
 is_noetherian_iff_well_founded.mp
 
+lemma finite_of_linear_independent {α β} [nonzero_comm_ring α] [add_comm_group β] [module α β]
+  [decidable_eq α] [decidable_eq β] [is_noetherian α β] {s : set β}
+  (hs : linear_independent α (subtype.val : s → β)) : s.finite :=
+begin
+  refine classical.by_contradiction (λ hf, order_embedding.well_founded_iff_no_descending_seq.1
+    (well_founded_submodule_gt α β) ⟨_⟩),
+  have f : ℕ ↪ s, from @infinite.nat_embedding s ⟨λ f, hf ⟨f⟩⟩,
+  have : ∀ n, (subtype.val ∘ f) '' {m | m ≤ n} ⊆ s,
+  { rintros n x ⟨y, hy₁, hy₂⟩, subst hy₂, exact (f y).2 },
+  have : ∀ a b : ℕ, a ≤ b ↔
+    span α ((subtype.val ∘ f) '' {m | m ≤ a}) ≤ span α ((subtype.val ∘ f) '' {m | m ≤ b}),
+  { assume a b,
+    rw [span_le_span_iff (@zero_ne_one α _) hs (this a) (this b),
+      set.image_subset_image_iff (injective_comp subtype.val_injective f.inj'),
+      set.subset_def],
+    exact ⟨λ hab x (hxa : x ≤ a), le_trans hxa hab, λ hx, hx a (le_refl a)⟩ },
+  exact ⟨⟨λ n, span α ((subtype.val ∘ f) '' {m | m ≤ n}),
+      λ x y, by simp [le_antisymm_iff, (this _ _).symm] {contextual := tt}⟩,
+    by dsimp [gt]; simp only [lt_iff_le_not_le, (this _ _).symm]; tauto⟩
+end
+
 @[class] def is_noetherian_ring (α) [ring α] : Prop := is_noetherian α α
 
 instance is_noetherian_ring.to_is_noetherian {α : Type*} [ring α] :
@@ -382,7 +404,7 @@ local attribute [elab_as_eliminator] well_founded.fix
 
 lemma well_founded_dvd_not_unit : well_founded (λ a b : α, a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x ) :=
 by simp only [ideal.span_singleton_lt_span_singleton.symm];
-   exact inv_image.wf (λ a, ideal.span ({a} : set α)) well_founded_submodule_gt
+   exact inv_image.wf (λ a, ideal.span ({a} : set α)) (well_founded_submodule_gt _ _)
 
 lemma exists_irreducible_factor {a : α} (ha : ¬ is_unit a) (ha0 : a ≠ 0) :
   ∃ i, irreducible i ∧ i ∣ a :=

src/ring_theory/polynomial.lean

@@ -234,7 +234,7 @@ have hm2 : ∀ k, I.leading_coeff_nth k ≤ M := λ k, or.cases_on (le_or_lt k N
   (λ h, HN ▸ I.leading_coeff_nth_mono h)
   (λ h x hx, classical.by_contradiction $ λ hxm,
     have ¬M < I.leading_coeff_nth k, by refine well_founded.not_lt_min
-      well_founded_submodule_gt _ _ _; exact ⟨k, rfl⟩,
+      (well_founded_submodule_gt _ _) _ _ _; exact ⟨k, rfl⟩,
     this ⟨HN ▸ I.leading_coeff_nth_mono (le_of_lt h), λ H, hxm (H hx)⟩),
 have hs2 : ∀ {x}, x ∈ I.degree_le N → x ∈ ideal.span (↑s : set (polynomial R)),
 from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx) (ideal.zero_mem _)