From 920ec123defd714a4b932de5304497a55dd09a6c Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 18 Apr 2023 03:37:03 +0000 Subject: [PATCH] doc: add and clarify some docstrings in LinearAlgebra.Dimension (#3488) --- Mathlib/LinearAlgebra/Dimension.lean | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/Mathlib/LinearAlgebra/Dimension.lean b/Mathlib/LinearAlgebra/Dimension.lean index d61d543c3d259..27f11fa4c2ddc 100644 --- a/Mathlib/LinearAlgebra/Dimension.lean +++ b/Mathlib/LinearAlgebra/Dimension.lean @@ -152,7 +152,11 @@ theorem rank_le {n : ℕ} exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li #align rank_le rank_le + set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074 +/-- The rank of the range of a linear map is at most the rank of the source. -/ +-- The proof is: a free submodule of the range lifts to a free submodule of the +-- source, by arbitrarily lifting a basis. theorem lift_rank_range_le (f : M →ₗ[R] M') : Cardinal.lift.{v} (Module.rank R (LinearMap.range f)) ≤ Cardinal.lift.{v'} (Module.rank R M) := by simp only [Module.rank_def] @@ -770,7 +774,8 @@ theorem linearIndependent_le_basis {ι : Type _} (b : Basis ι R M) {κ : Type _ exact linearIndependent_le_infinite_basis b v i #align linear_independent_le_basis linearIndependent_le_basis -/-- In an `n`-dimensional space, the rank is at most `m`. -/ +/-- Let `R` satisfy the strong rank condition. If `m` elements of a free rank `n` `R`-module are +linearly independent, then `m ≤ n`. -/ theorem Basis.card_le_card_of_linearIndependent_aux {R : Type _} [Ring R] [StrongRankCondition R] (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n := fun h => by simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h @@ -884,8 +889,10 @@ theorem rank_span_set {s : Set M} (hs : LinearIndependent R (fun x => x : s → exact rank_span hs #align rank_span_set rank_span_set -/-- If `N` is a submodule in a free, finitely generated module, -do induction on adjoining a linear independent element to a submodule. -/ +/-- An induction (and recursion) principle for proving results about all submodules of a fixed +finite free module `M`. A property is true for all submodules of `M` if it satisfies the following +"inductive step": the property is true for a submodule `N` if it's true for all submodules `N'` +of `N` with the property that there exists `0 ≠ x ∈ N` such that the sum `N' + Rx` is direct. -/ def Submodule.inductionOnRank [IsDomain R] [Fintype ι] (b : Basis ι R M) (P : Submodule R M → Sort _) (ih : ∀ N : Submodule R M, (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N) @@ -895,9 +902,8 @@ def Submodule.inductionOnRank [IsDomain R] [Fintype ι] (b : Basis ι R M) #align submodule.induction_on_rank Submodule.inductionOnRank set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074 -/-- If `S` a finite-dimensional ring extension of `R` which is free as an `R`-module, -then the rank of an ideal `I` of `S` over `R` is the same as the rank of `S`. --/ +/-- If `S` a module-finite free `R`-algebra, then the `R`-rank of a nonzero `R`-free +ideal `I` of `S` is the same as the rank of `S`. -/ theorem Ideal.rank_eq {R S : Type _} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S] [Algebra R S] {n m : Type _} [Fintype n] [Fintype m] (b : Basis n R S) {I : Ideal S} (hI : I ≠ ⊥) (c : Basis m R I) : Fintype.card m = Fintype.card n := by @@ -1002,7 +1008,8 @@ theorem LinearEquiv.nonempty_equiv_iff_rank_eq : ⟨fun ⟨h⟩ => LinearEquiv.rank_eq h, fun h => nonempty_linearEquiv_of_rank_eq h⟩ #align linear_equiv.nonempty_equiv_iff_rank_eq LinearEquiv.nonempty_equiv_iff_rank_eq -/-- The rank of `M × N` is `(Module.rank R M).lift + (Module.rank R N).lift`. -/ +/-- If `M` and `N` are free, then the rank of `M × N` is +`(module.rank R M).lift + (module.rank R N).lift`. -/ @[simp] theorem rank_prod : Module.rank K (V × V') = Cardinal.lift.{v'} (Module.rank K V) + Cardinal.lift.{v, v'} (Module.rank K V') := by @@ -1010,7 +1017,7 @@ theorem rank_prod : Module.rank K (V × V') = lift_umax'] using ((chooseBasis K V).prod (chooseBasis K V')).mk_eq_rank.symm #align rank_prod rank_prod -/-- If `M` and `N` lie in the same universe, the rank of `M × N` is +/-- If `M` and `N` are free (and lie in the same universe), the rank of `M × N` is `(Module.rank R M) + (Module.rank R N)`. -/ theorem rank_prod' : Module.rank K (V × V₁) = Module.rank K V + Module.rank K V₁ := by simp #align rank_prod' rank_prod' @@ -1021,7 +1028,8 @@ variable [∀ i, AddCommGroup (φ i)] [∀ i, Module K (φ i)] [∀ i, Module.Fr open LinearMap -/-- The rank of a finite product is the sum of the ranks. -/ +/-- The rank of a finite product of free modules is the sum of the ranks. -/ +-- this result is not true without the freeness assumption @[simp] theorem rank_pi [Finite η] : Module.rank K (∀ i, φ i) = Cardinal.sum fun i => Module.rank K (φ i) := by