chore(linear_algebra/*): changes to finsupp_vectorspaces and move mod…

…ule doc dual (#6516)

This PR does the following:

- move the module doc of `linear_algebra.dual` so that it is recognised by the linter.
- add `ker_eq_bot_iff_range_eq_top_of_findim_eq_findim` to `linear_algebra.finite_dimensional`, this replaces `injective_of_surjective` in `linear_algebra.finsupp_vectorspaces`
- remove `eq_bot_iff_dim_eq_zero` from `linear_algebra.finsupp_vectorspaces`, this already exists as `dim_eq_zero` in `linear_algebra.finite_dimensional`
- changed `cardinal_mk_eq_cardinal_mk_field_pow_dim` and `cardinal_lt_omega_of_dim_lt_omega` to assume `finite_dimensional K V` instead of `dim < omega`.
- renamed `cardinal_lt_omega_of_dim_lt_omega` to `cardinal_lt_omega_of_finite_dimensional` since the assumption changed.
- provided a module doc for `linear_algebra.finsupp_vectorspaces` which should remove `linear_algebra.*` from the style exceptions file.

This file should probably be looked at again by someone more experienced in the linear_algebra part of the library. It seems to me that most of the statements in this file in fact would better fit in other files.




Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

src/field_theory/finite/polynomial.lean

@@ -8,6 +8,7 @@ import field_theory.finite.basic
 import field_theory.mv_polynomial
 import data.mv_polynomial.expand
 import linear_algebra.basic
+import linear_algebra.finite_dimensional
 
 /-!
 ## Polynomials over finite fields
@@ -177,6 +178,13 @@ calc vector_space.dim K (R σ K) =
   end
   ... = fintype.card (σ → K) : cardinal.fintype_card _
 
+instance : finite_dimensional K (R σ K) :=
+finite_dimensional.finite_dimensional_iff_dim_lt_omega.mpr
+  (by simpa only [dim_R] using cardinal.nat_lt_omega (fintype.card (σ → K)))
+
+lemma findim_R : finite_dimensional.findim K (R σ K) = fintype.card (σ → K) :=
+finite_dimensional.findim_eq_of_dim_eq (dim_R σ K)
+
 def evalᵢ : R σ K →ₗ[K] (σ → K) → K :=
 ((evalₗ K σ).comp (restrict_degree σ K (fintype.card K - 1)).subtype)
 
@@ -188,9 +196,8 @@ end
 
 lemma ker_evalₗ : (evalᵢ σ K).ker = ⊥ :=
 begin
-  refine injective_of_surjective _ _ _ (range_evalᵢ _ _),
-  { rw [dim_R], exact cardinal.nat_lt_omega _ },
-  { rw [dim_R, dim_fun, dim_of_field, mul_one] }
+  refine (ker_eq_bot_iff_range_eq_top_of_findim_eq_findim _).mpr (range_evalᵢ _ _),
+  rw [finite_dimensional.findim_fintype_fun_eq_card, findim_R]
 end
 
 lemma eq_zero_of_eval_eq_zero (p : mv_polynomial σ K)

src/linear_algebra/dual.lean

@@ -6,8 +6,6 @@ Authors: Johan Commelin, Fabian Glöckle
 import linear_algebra.finite_dimensional
 import linear_algebra.projection
 
-noncomputable theory
-
 /-!
 # Dual vector spaces
 
@@ -32,8 +30,13 @@ The dual space of an R-module M is the R-module of linear maps `M → R`.
 
 We sometimes use `V'` as local notation for `dual K V`.
 
+## TODO
+
+Erdös-Kaplansky theorem about the dimension of a dual vector space in case of infinite dimension.
 -/
 
+noncomputable theory
+
 namespace module
 
 variables (R : Type*) (M : Type*)

src/linear_algebra/finite_dimensional.lean

@@ -191,6 +191,13 @@ lemma findim_eq_dim (K : Type u) (V : Type v) [field K]
   (findim K V : cardinal.{v}) = dim K V :=
 by rw [findim, cast_to_nat_of_lt_omega (dim_lt_omega K V)]
 
+lemma findim_eq_of_dim_eq {n : ℕ} (h : dim K V = ↑ n) : findim K V = n :=
+begin
+  apply_fun to_nat at h,
+  rw to_nat_cast at h,
+  exact_mod_cast h,
+end
+
 lemma findim_of_infinite_dimensional {K V : Type*} [field K] [add_comm_group V] [vector_space K V]
   (h : ¬finite_dimensional K V) : findim K V = 0 :=
 dif_neg $ mt finite_dimensional_iff_dim_lt_omega.2 h
@@ -884,6 +891,11 @@ begin
   { rw [h, findim_top, H] at this, exact findim_eq_zero.1 (add_right_injective _ this) }
 end
 
+lemma ker_eq_bot_iff_range_eq_top_of_findim_eq_findim [finite_dimensional K V]
+  [finite_dimensional K V₂] (H : findim K V = findim K V₂) {f : V →ₗ[K] V₂} :
+  f.ker = ⊥ ↔ f.range = ⊤ :=
+by rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_findim_eq_findim H]
+
 theorem findim_le_findim_of_injective [finite_dimensional K V] [finite_dimensional K V₂]
   {f : V →ₗ[K] V₂} (hf : function.injective f) : findim K V ≤ findim K V₂ :=
 calc  findim K V

src/linear_algebra/finsupp_vector_space.lean

@@ -2,12 +2,26 @@
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Johannes Hölzl
-
-Linear structures on function with finite support `ι →₀ β`.
 -/
+
 import data.mv_polynomial
 import linear_algebra.dimension
 import linear_algebra.direct_sum.finsupp
+import linear_algebra.finite_dimensional
+
+/-!
+# Linear structures on function with finite support `ι →₀ M`
+
+This file contains results on the `R`-module structure on functions of finite support from a type
+`ι` to an `R`-module `M`, in particular in the case that `R` is a field.
+
+Furthermore, it contains some facts about isomorphisms of vector spaces from equality of dimension
+as well as the cardinality of finite dimensional vector spaces.
+
+## TODO
+
+Move the second half of this file to more appropriate other files.
+-/
 
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
@@ -147,53 +161,34 @@ begin
   exact classical.choice (equiv_of_dim_eq_lift_dim hn),
 end
 
-lemma eq_bot_iff_dim_eq_zero (p : submodule K V) (h : dim K p = 0) : p = ⊥ :=
-begin
-  have : dim K p = dim K (⊥ : submodule K V) := by rwa [dim_bot],
-  let e := equiv_of_dim_eq_dim this,
-  exact e.eq_bot_of_equiv _
-end
-
-lemma injective_of_surjective (f : V₁ →ₗ[K] V₂)
-  (hV₁ : dim K V₁ < cardinal.omega) (heq : dim K V₂ = dim K V₁) (hf : f.range = ⊤) : f.ker = ⊥ :=
-have hk : dim K f.ker < cardinal.omega := lt_of_le_of_lt (dim_submodule_le _) hV₁,
-begin
-  rcases cardinal.lt_omega.1 hV₁ with ⟨d₁, eq₁⟩,
-  rcases cardinal.lt_omega.1 hk with ⟨d₂, eq₂⟩,
-  have : 0 = d₂,
-  { have := dim_eq_of_surjective f (linear_map.range_eq_top.1 hf),
-    rw [heq, eq₁, eq₂, ← nat.cast_add, cardinal.nat_cast_inj] at this,
-    exact nat.add_left_cancel this },
-  refine eq_bot_iff_dim_eq_zero _ _,
-  rw [eq₂, ← this, nat.cast_zero]
-end
-
 end vector_space
 
 section vector_space
 universes u
 
 open vector_space
 
-variables {K V : Type u} [field K] [add_comm_group V] [vector_space K V]
+variables (K V : Type u) [field K] [add_comm_group V] [vector_space K V]
 
-lemma cardinal_mk_eq_cardinal_mk_field_pow_dim (h : dim K V < cardinal.omega) :
+lemma cardinal_mk_eq_cardinal_mk_field_pow_dim [finite_dimensional K V] :
   cardinal.mk V = cardinal.mk K ^ dim K V :=
 begin
   rcases exists_is_basis K V with ⟨s, hs⟩,
   have : nonempty (fintype s),
-  { rwa [← cardinal.lt_omega_iff_fintype, cardinal.lift_inj.1 hs.mk_eq_dim] },
+  { rw [← cardinal.lt_omega_iff_fintype, cardinal.lift_inj.1 hs.mk_eq_dim],
+    exact finite_dimensional.dim_lt_omega K V },
   cases this with hsf, letI := hsf,
   calc cardinal.mk V = cardinal.mk (s →₀ K) : quotient.sound ⟨(module_equiv_finsupp hs).to_equiv⟩
     ... = cardinal.mk (s → K) : quotient.sound ⟨finsupp.equiv_fun_on_fintype⟩
     ... = _ : by rw [← cardinal.lift_inj.1 hs.mk_eq_dim, cardinal.power_def]
 end
 
-lemma cardinal_lt_omega_of_dim_lt_omega [fintype K] (h : dim K V < cardinal.omega) :
+lemma cardinal_lt_omega_of_finite_dimensional [fintype K] [finite_dimensional K V] :
   cardinal.mk V < cardinal.omega :=
 begin
-  rw [cardinal_mk_eq_cardinal_mk_field_pow_dim h],
-  exact cardinal.power_lt_omega (cardinal.lt_omega_iff_fintype.2 ⟨infer_instance⟩) h
+  rw cardinal_mk_eq_cardinal_mk_field_pow_dim K V,
+  exact cardinal.power_lt_omega (cardinal.lt_omega_iff_fintype.2 ⟨infer_instance⟩)
+    (finite_dimensional.dim_lt_omega K V),
 end
 
 end vector_space