refactor(linear_algebra/finite_dimensional): universe polymorphism, …

…doc (#1784)

* refactor(linear_algebra/finite_dimensional): universe polymorphism, doc

* docstrings

* improvements

* typo

* Update src/linear_algebra/dimension.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/finite_dimensional.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/finite_dimensional.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* fix comments

* fix build

* fix build

* remove pp.universe

* keep docstring in sync

archive/sensitivity.lean

@@ -236,11 +236,11 @@ def dual_pair_e_ε (n : ℕ) : dual_pair (@e n) (@ε n) :=
 
 lemma dim_V : vector_space.dim ℝ (V n) = 2^n :=
 have vector_space.dim ℝ (V n) = ↑(2^n : ℕ),
-  by { rw [dim_eq_card (dual_pair_e_ε _).is_basis, Q.card]; apply_instance },
+  by { rw [dim_eq_card_basis (dual_pair_e_ε _).is_basis, Q.card]; apply_instance },
 by assumption_mod_cast
 
 instance : finite_dimensional ℝ (V n) :=
-finite_dimensional_of_finite_basis (dual_pair_e_ε _).is_basis
+finite_dimensional.of_finite_basis (dual_pair_e_ε _).is_basis
 
 lemma findim_V : findim ℝ (V n) = 2^n :=
 have _ := @dim_V n,

src/analysis/normed_space/finite_dimension.lean

@@ -34,13 +34,9 @@ on a single space, which is not the way type classes work. However, if one has a
 finite-dimensional vector space `E` with a norm, and a copy `E'` of this type with another norm,
 then the identities from `E` to `E'` and from `E'`to `E` are continuous thanks to
 `linear_map.continuous_of_finite_dimensional`. This gives the desired norm equivalence.
-
-The proofs rely on linear equivalences, which are only defined in mathlib for types in the same
-universe. Therefore, all the results in this file are restricted to spaces living in the same
-universe as their base field.
 -/
 
-universes u v
+universes u v w
 
 open set finite_dimensional
 open_locale classical
@@ -54,7 +50,7 @@ local attribute [instance, priority 10000] pi.module normed_space.to_vector_spac
 set_option class.instance_max_depth 100
 
 /-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
-lemma linear_map.continuous_on_pi {ι : Type u} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
+lemma linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
   {E : Type v} [normed_group E] [normed_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) : continuous f :=
 begin
   -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
@@ -69,21 +65,20 @@ end
 
 section complete_field
 
--- we use linear equivs, which require all the types to live in the same universe
 variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
-{E : Type u} [normed_group E] [normed_space 𝕜 E]
-{F : Type v} [normed_group F] [normed_space 𝕜 F]
+{E : Type v} [normed_group E] [normed_space 𝕜 E]
+{F : Type w} [normed_group F] [normed_space 𝕜 F]
 [complete_space 𝕜]
 
 set_option class.instance_max_depth 150
 
 /-- In finite dimension over a complete field, the canonical identification (in terms of a basis)
-with 𝕜^n together with its sup norm is continuous. This is the nontrivial part in the fact that all
-norms are equivalent in finite dimension.
-Do not use this statement as its formulation is awkward (in terms of the dimension n, as the proof
-is done by induction over n) and it is superceded by the fact that every linear map on a
+with `𝕜^n` together with its sup norm is continuous. This is the nontrivial part in the fact that
+all norms are equivalent in finite dimension.
+Do not use this statement as its formulation is awkward (in terms of the dimension `n`, as the proof
+is done by induction over `n`) and it is superceded by the fact that every linear map on a
 finite-dimensional space is continuous, in `linear_map.continuous_of_finite_dimensional`. -/
-lemma continuous_equiv_fun_basis {n : ℕ} {ι : Type u} [fintype ι] (ξ : ι → E)
+lemma continuous_equiv_fun_basis {n : ℕ} {ι : Type v} [fintype ι] (ξ : ι → E)
   (hn : fintype.card ι = n) (hξ : is_basis 𝕜 ξ) : continuous (equiv_fun_basis hξ) :=
 begin
   unfreezeI,
@@ -94,7 +89,7 @@ begin
     change ∥equiv_fun_basis hξ x∥ ≤ 0 * ∥x∥,
     rw this,
     simp [norm_nonneg] },
-  { haveI : finite_dimensional 𝕜 E := finite_dimensional_of_finite_basis hξ,
+  { haveI : finite_dimensional 𝕜 E := of_finite_basis hξ,
     -- first step: thanks to the inductive assumption, any n-dimensional subspace is equivalent
     -- to a standard space of dimension n, hence it is complete and therefore closed.
     have H₁ : ∀s : submodule 𝕜 E, findim 𝕜 s = n → is_closed (s : set E),
@@ -103,7 +98,7 @@ begin
       letI : fintype b := finite.fintype b_finite,
       have U : uniform_embedding (equiv_fun_basis b_basis).symm,
       { have : fintype.card b = n,
-          by { rw ← s_dim, exact (findim_eq_card b_basis).symm },
+          by { rw ← s_dim, exact (findim_eq_card_basis b_basis).symm },
         have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) this b_basis,
         exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
       have : is_complete (range ((equiv_fun_basis b_basis).symm)),
@@ -123,10 +118,10 @@ begin
     { assume f,
       have : findim 𝕜 f.ker = n ∨ findim 𝕜 f.ker = n.succ,
       { have Z := f.findim_range_add_findim_ker,
-        rw [findim_eq_card hξ, hn] at Z,
+        rw [findim_eq_card_basis hξ, hn] at Z,
         have : findim 𝕜 f.range = 0 ∨ findim 𝕜 f.range = 1,
         { have I : ∀(k : ℕ), k ≤ 1 ↔ k = 0 ∨ k = 1, by omega manual,
-          have : findim 𝕜 f.range ≤ findim 𝕜 𝕜 := findim_submodule_le _,
+          have : findim 𝕜 f.range ≤ findim 𝕜 𝕜 := submodule.findim_le _,
           rwa [findim_of_field, I] at this },
         cases this,
         { rw this at Z,
@@ -139,7 +134,7 @@ begin
       { cases this,
         { exact H₁ _ this },
         { have : f.ker = ⊤,
-            by { apply eq_top_of_findim_eq, rw [findim_eq_card hξ, hn, this] },
+            by { apply eq_top_of_findim_eq, rw [findim_eq_card_basis hξ, hn, this] },
           simp [this] } },
       exact linear_map.continuous_iff_is_closed_ker.2 this },
     -- third step: applying the continuity to the linear form corresponding to a coefficient in the
@@ -183,8 +178,8 @@ end
 
 /-- Any finite-dimensional vector space over a complete field is complete.
 We do not register this as an instance to avoid an instance loop when trying to prove the
-completeness of 𝕜, and the search for 𝕜 as an unknown metavariable. Declare the instance explicitly
-when needed. -/
+completeness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
+explicitly when needed. -/
 variables (𝕜 E)
 lemma finite_dimensional.complete [finite_dimensional 𝕜 E] : complete_space E :=
 begin
@@ -220,14 +215,13 @@ is_closed_of_is_complete s.complete_of_finite_dimensional
 end complete_field
 
 section proper_field
--- we use linear equivs, which require all the types to live in the same universe
 variables (𝕜 : Type u) [nondiscrete_normed_field 𝕜]
-(E : Type u) [normed_group E] [normed_space 𝕜 E] [proper_space 𝕜]
+(E : Type v) [normed_group E] [normed_space 𝕜 E] [proper_space 𝕜]
 
 /-- Any finite-dimensional vector space over a proper field is proper.
 We do not register this as an instance to avoid an instance loop when trying to prove the
-properness of 𝕜, and the search for 𝕜 as an unknown metavariable. Declare the instance explicitly
-when needed. -/
+properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
+explicitly when needed. -/
 lemma finite_dimensional.proper [finite_dimensional 𝕜 E] : proper_space E :=
 begin
   rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
@@ -250,7 +244,7 @@ end proper_field
 /- Over the real numbers, we can register the previous statement as an instance as it will not
 cause problems in instance resolution since the properness of `ℝ` is already known. -/
 instance finite_dimensional.proper_real
-  (E : Type) [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] : proper_space E :=
+  (E : Type u) [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] : proper_space E :=
 finite_dimensional.proper ℝ E
 
 attribute [instance, priority 900] finite_dimensional.proper_real

src/linear_algebra/basic.lean

@@ -214,7 +214,7 @@ open_locale classical
 
 /-- A linear map `f` applied to `x : ι → R` can be computed using the image under `f` of elements
 of the canonical basis. -/
-lemma pi_apply_eq_sum_univ {ι : Type u} [fintype ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
+lemma pi_apply_eq_sum_univ [fintype ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
   f x = finset.sum finset.univ (λi:ι, x i • (f (λj, if i = j then 1 else 0))) :=
 begin
   conv_lhs { rw [pi_eq_sum_univ x, f.map_sum] },
@@ -1118,6 +1118,11 @@ by simpa using map_comap_subtype p ⊤
 lemma map_subtype_le (p' : submodule R p) : map p.subtype p' ≤ p :=
 by simpa using (map_mono le_top : map p.subtype p' ≤ p.subtype.range)
 
+/-- Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the
+maximal submodule of `p` is just `p `. -/
+@[simp] lemma map_subtype_top : map p.subtype (⊤ : submodule R p) = p :=
+by simp
+
 @[simp] theorem ker_of_le (p p' : submodule R M) (h : p ≤ p') : (of_le h).ker = ⊥ :=
 by rw [of_le, ker_cod_restrict, ker_subtype]
 
@@ -1187,12 +1192,13 @@ by rw [range, ← prod_top, prod_map_fst]
 @[simp] theorem range_snd : (snd R M M₂).range = ⊤ :=
 by rw [range, ← prod_top, prod_map_snd]
 
-/-- The map from a module `M` to the quotient of `M` by a submodule `p` is a linear map. -/
+/-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
 def mkq : M →ₗ[R] p.quotient := ⟨quotient.mk, by simp, by simp⟩
 
 @[simp] theorem mkq_apply (x : M) : p.mkq x = quotient.mk x := rfl
 
-/-- The map from the quotient of `M` by a submodule `p` to `M₂` along `f : M → M₂` is linear. -/
+/-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
+vanishing on `p`, as a linear map. -/
 def liftq (f : M →ₗ[R] M₂) (h : p ≤ f.ker) : p.quotient →ₗ[R] M₂ :=
 ⟨λ x, _root_.quotient.lift_on' x f $
    λ a b (ab : a - b ∈ p), eq_of_sub_eq_zero $ by simpa using h ab,

src/linear_algebra/basis.lean

@@ -858,7 +858,7 @@ begin
     simp [submodule.mem_span_singleton] }
 end
 
-lemma linear_equiv.is_basis (hs : is_basis R v)
+protected lemma linear_equiv.is_basis (hs : is_basis R v)
   (f : M ≃ₗ[R] M') : is_basis R (f ∘ v) :=
 begin
   split,

src/linear_algebra/dimension.lean

@@ -168,15 +168,19 @@ begin
       ⟨equiv.ulift.trans (equiv.sum_congr (@equiv.ulift b) (@equiv.ulift c)).symm ⟩),
 end
 
-theorem dim_quotient (p : submodule K V) :
+theorem dim_quotient_add_dim (p : submodule K V) :
   dim K p.quotient + dim K p = dim K V :=
 by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in dim_prod.symm.trans f.dim_eq
 
+theorem dim_quotient_le (p : submodule K V) :
+  dim K p.quotient ≤ dim K V :=
+by { rw ← dim_quotient_add_dim p, exact cardinal.le_add_right _ _ }
+
 /-- rank-nullity theorem -/
 theorem dim_range_add_dim_ker (f : V →ₗ[K] V₂) : dim K f.range + dim K f.ker = dim K V :=
 begin
   haveI := λ (p : submodule K V), classical.dec_eq p.quotient,
-  rw [← f.quot_ker_equiv_range.dim_eq, dim_quotient]
+  rw [← f.quot_ker_equiv_range.dim_eq, dim_quotient_add_dim]
 end
 
 lemma dim_range_le (f : V →ₗ[K] V₂) : dim K f.range ≤ dim K V :=
@@ -204,32 +208,12 @@ by rw [dim_eq_surjective f h]; refine le_add_right (le_refl _)
 lemma dim_eq_injective (f : V →ₗ[K] V₂) (h : injective f) : dim K V = dim K f.range :=
 by rw [← dim_range_add_dim_ker f, linear_map.ker_eq_bot.2 h]; simp [dim_bot]
 
-set_option class.instance_max_depth 37
 lemma dim_submodule_le (s : submodule K V) : dim K s ≤ dim K V :=
-begin
-  letI := classical.dec_eq V,
-  rcases exists_is_basis K s with ⟨bs, hbs⟩,
-  have : linear_independent K (λ (i : bs), submodule.subtype s i.val) :=
-    (linear_independent.image hbs.1) (linear_map.disjoint_ker'.2
-        (λ _ _ _ _ h, subtype.val_injective h)),
-  rcases exists_subset_is_basis (this.to_subtype_range) with ⟨b, hbs_b, hb⟩,
-  rw [←cardinal.lift_le, ← is_basis.mk_eq_dim hbs, ← is_basis.mk_eq_dim hb, cardinal.lift_le],
-  have : subtype.val '' bs ⊆ b,
-  { convert hbs_b,
-    rw [@range_comp _ _ _ (λ (i : bs), (i.val)) (submodule.subtype s),
-      ←image_univ, submodule.subtype],
-    simp only [subtype.val_image_univ],
-    refl },
-  calc cardinal.mk ↥bs = cardinal.mk ((subtype.val : s → V) '' bs) :
-      (cardinal.mk_image_eq $ subtype.val_injective).symm
-    ... ≤ cardinal.mk ↥b :
-      nonempty.intro (embedding_of_subset this),
-end
-set_option class.instance_max_depth 32
+by { rw ← dim_quotient_add_dim s, exact cardinal.le_add_left _ _ }
 
 lemma dim_le_injective (f : V →ₗ[K] V₂) (h : injective f) :
   dim K V ≤ dim K V₂ :=
-by rw [dim_eq_injective f h]; exact dim_submodule_le _
+by { rw [dim_eq_injective f h], exact dim_submodule_le _ }
 
 lemma dim_le_of_submodule (s t : submodule K V) (h : s ≤ t) : dim K s ≤ dim K t :=
 dim_le_injective (of_le h) $ assume ⟨x, hx⟩ ⟨y, hy⟩ eq,