chore(linear_algebra/dimension): rename rank to linear_map.rank (#18734)

It's a bit weird having `rank` in the root namespace, defined in terms of `module.rank` which isn't.

This moves all the lemmas into a single block at the end of the file, as they were previously spread through the file.

Author: eric-wieser

docs/undergrad.yaml

@@ -28,7 +28,7 @@ Linear algebra:
   Finite-dimensional vector spaces:
     finite-dimensionality : 'finite_dimensional'
     isomorphism with $K^n$: 'basis.equiv_fun'
-    rank of a linear map: 'rank'
+    rank of a linear map: 'linear_map.rank'
     rank of a set of vectors: 'set.finrank'
     rank of a system of linear equations: 'https://www.math.tamu.edu/~fnarc/psfiles/rank2005.pdf'
     isomorphism with bidual: 'module.eval_equiv'

src/analysis/normed_space/finite_dimension.lean

@@ -244,9 +244,9 @@ lemma is_open_set_of_linear_independent {ι : Type*} [finite ι] :
   is_open {f : ι → E | linear_independent 𝕜 f} :=
 is_open_iff_mem_nhds.2 $ λ f, linear_independent.eventually
 
-lemma is_open_set_of_nat_le_rank (n : ℕ) : is_open {f : E →L[𝕜] F | ↑n ≤ rank (f : E →ₗ[𝕜] F)} :=
+lemma is_open_set_of_nat_le_rank (n : ℕ) : is_open {f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank } :=
 begin
-  simp only [le_rank_iff_exists_linear_independent_finset, set_of_exists, ← exists_prop],
+  simp only [linear_map.le_rank_iff_exists_linear_independent_finset, set_of_exists, ← exists_prop],
   refine is_open_bUnion (λ t ht, _),
   have : continuous (λ f : E →L[𝕜] F, (λ x : (t : set E), f x)),
     from continuous_pi (λ x, (continuous_linear_map.apply 𝕜 F (x : E)).continuous),

src/linear_algebra/dimension.lean

@@ -1169,61 +1169,10 @@ end
 
 end division_ring
 
-section rank
-
-section
-variables [ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
-variables [add_comm_group V'] [module K V']
-
-/-- `rank f` is the rank of a `linear_map f`, defined as the dimension of `f.range`. -/
-def rank (f : V →ₗ[K] V') : cardinal := module.rank K f.range
-
-lemma rank_le_range (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V₁ :=
-dim_submodule_le _
-
-@[simp] lemma rank_zero [nontrivial K] : rank (0 : V →ₗ[K] V') = 0 :=
-by rw [rank, linear_map.range_zero, dim_bot]
-
-variables [add_comm_group V''] [module K V'']
-
-lemma rank_comp_le1 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f :=
-begin
-  refine dim_le_of_submodule _ _ _,
-  rw [linear_map.range_comp],
-  exact linear_map.map_le_range,
-end
-
-variables [add_comm_group V'₁] [module K V'₁]
-
-lemma rank_comp_le2 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g :=
-by rw [rank, rank, linear_map.range_comp]; exact dim_map_le _ _
-
-end
-
-end rank
-
 section division_ring
 variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
 variables [add_comm_group V'] [module K V']
 
-lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V :=
-by { rw [← dim_range_add_dim_ker f], exact self_le_add_right _ _ }
-
-lemma rank_add_le (f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g :=
-calc rank (f + g) ≤ module.rank K (f.range ⊔ g.range : submodule K V') :
-  begin
-    refine dim_le_of_submodule _ _ _,
-    exact (linear_map.range_le_iff_comap.2 $ eq_top_iff'.2 $
-      assume x, show f x + g x ∈ (f.range ⊔ g.range : submodule K V'), from
-        mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩)
-  end
-  ... ≤ rank f + rank g : dim_add_le_dim_add_dim _ _
-
-lemma rank_finset_sum_le {η} (s : finset η) (f : η → V →ₗ[K] V') :
-  rank (∑ d in s, f d) ≤ ∑ d in s, rank (f d) :=
-@finset.sum_hom_rel _ _ _ _ _ (λa b, rank a ≤ b) f (λ d, rank (f d)) s (le_of_eq rank_zero)
-      (λ i g c h, le_trans (rank_add_le _ _) (add_le_add_left h _))
-
 /-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.
 
 See also `finite_dimensional.fin_basis`.
@@ -1355,6 +1304,65 @@ lemma module.rank_le_one_iff_top_is_principal :
   module.rank K V ≤ 1 ↔ (⊤ : submodule K V).is_principal :=
 by rw [← submodule.rank_le_one_iff_is_principal, dim_top]
 
+end division_ring
+
+end module
+
+/-! ### The rank of a linear map -/
+
+namespace linear_map
+
+section ring
+variables [ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
+variables [add_comm_group V'] [module K V']
+
+/-- `rank f` is the rank of a `linear_map` `f`, defined as the dimension of `f.range`. -/
+def rank (f : V →ₗ[K] V') : cardinal := module.rank K f.range
+
+lemma rank_le_range (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V₁ :=
+dim_submodule_le _
+
+@[simp] lemma rank_zero [nontrivial K] : rank (0 : V →ₗ[K] V') = 0 :=
+by rw [rank, linear_map.range_zero, dim_bot]
+
+variables [add_comm_group V''] [module K V'']
+
+lemma rank_comp_le1 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f :=
+begin
+  refine dim_le_of_submodule _ _ _,
+  rw [linear_map.range_comp],
+  exact linear_map.map_le_range,
+end
+
+variables [add_comm_group V'₁] [module K V'₁]
+
+lemma rank_comp_le2 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g :=
+by rw [rank, rank, linear_map.range_comp]; exact dim_map_le _ _
+
+end ring
+
+section division_ring
+variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
+variables [add_comm_group V'] [module K V']
+
+lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V :=
+by { rw [← dim_range_add_dim_ker f], exact self_le_add_right _ _ }
+
+lemma rank_add_le (f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g :=
+calc rank (f + g) ≤ module.rank K (f.range ⊔ g.range : submodule K V') :
+  begin
+    refine dim_le_of_submodule _ _ _,
+    exact (linear_map.range_le_iff_comap.2 $ eq_top_iff'.2 $
+      assume x, show f x + g x ∈ (f.range ⊔ g.range : submodule K V'), from
+        mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩)
+  end
+  ... ≤ rank f + rank g : dim_add_le_dim_add_dim _ _
+
+lemma rank_finset_sum_le {η} (s : finset η) (f : η → V →ₗ[K] V') :
+  rank (∑ d in s, f d) ≤ ∑ d in s, rank (f d) :=
+@finset.sum_hom_rel _ _ _ _ _ (λa b, rank a ≤ b) f (λ d, rank (f d)) s (le_of_eq rank_zero)
+      (λ i g c h, le_trans (rank_add_le _ _) (add_le_add_left h _))
+
 lemma le_rank_iff_exists_linear_independent {c : cardinal} {f : V →ₗ[K] V'} :
   c ≤ rank f ↔
   ∃ s : set V, cardinal.lift.{v'} (#s) = cardinal.lift.{v} c ∧
@@ -1391,4 +1399,4 @@ end
 
 end division_ring
 
-end module
+end linear_map