Dimension of vector spaces

In this file we provide results about Module.rank and Module.finrank of vector spaces over division rings.

Main statements

For vector spaces (i.e. modules over a division ring), we have

• rank_quotient_add_rank_of_divisionRing: if V₁ is a submodule of V, then Module.rank (V/V₁) + Module.rank V₁ = Module.rank V.
• DivisionRing.hasRankNullity: The rank-nullity theorem for division rings.
• Submodule.rank_span_le_rank: The K-rank of the K-span of an R-submodule M of V is at most the R-rank of M.

See also Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean for the Erdős-Kaplansky theorem.

theorem Module.Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V < Cardinal.aleph0) : (ofVectorSpaceIndex K V).Finite

If a vector space has a finite dimension, the index set of Basis.ofVectorSpace is finite.

theorem rank_quotient_add_rank_of_divisionRing {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (p : Submodule K V) : Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Also see rank_quotient_add_rank.

instance DivisionRing.hasRankNullity {K : Type u} [DivisionRing K] : HasRankNullity.{u₀, u} K

theorem rank_add_rank_split {K : Type u} {V V₁ V₂ V₃ : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂) (ce : V₁ →ₗ[K] V₃) (hde : ⊤ ≤ db.range ⊔ eb.range) (hgd : cd.ker = ⊥) (eq : db ∘ₗ cd = eb ∘ₗ ce) (eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ (c : V₁), cd c = d ∧ ce c = e) : Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

This is mostly an auxiliary lemma for Submodule.rank_sup_add_rank_inf_eq.

theorem Submodule.rank_span_le_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (M : Submodule R V) : Module.rank K ↥(span K ↑M) ≤ Module.rank R ↥M

The K-rank of the K-span of an R-submodule M of V is at most the R-rank of M.

theorem Submodule.rank_span_le_rank_span {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (s : Set V) : Module.rank K ↥(span K s) ≤ Module.rank R ↥(span R s)

The K-rank of the K-span of a set s in V is at most the R-rank of the R-span of s.

theorem Submodule.finrank_span_le_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (M : Submodule R V) (h : M.FG) : Module.finrank K ↥(span K ↑M) ≤ Module.finrank R ↥M

The K-rank of the K-span of a finitely generated R-submodule M of V is at most the R-rank of M. This is the Module.finrank version of Submodule.rank_span_le_rank.

theorem Submodule.finrank_span_le_finrank_span {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] {s : Set V} (hs : s.Finite) : Module.finrank K ↥(span K s) ≤ Module.finrank R ↥(span R s)

The K-rank of the K-span of a finite set s in V is at most the R-rank of the R-span of s. This is the Module.finrank version of Submodule.rank_span_le_rank_span.

theorem Submodule.rank_span_eq_rank_of_linearIndepOn {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (M : Submodule R V) (H : ∀ s ⊆ ↑M, LinearIndepOn R id s → LinearIndepOn K id s) : Module.rank K ↥(span K ↑M) = Module.rank R ↥M

If every R-linearly independent subset of M is K-linearly independent, then the K-rank of the K-span of M equals the R-rank of M.

theorem Submodule.finrank_span_eq_finrank_of_linearIndepOn {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (M : Submodule R V) (H : ∀ s ⊆ ↑M, LinearIndepOn R id s → LinearIndepOn K id s) : Module.finrank K ↥(span K ↑M) = Module.finrank R ↥M

If every R-linearly independent subset of M is K-linearly independent, then the K-rank of the K-span of M equals the R-rank of M.

This is the Module.finrank version of Submodule.rank_span_eq_rank_of_linearIndepOn; see also Submodule.finrank_span_eq_finrank for an equality in a different setting.

theorem Submodule.linearIndepOn_of_finrank_le_finrank_span {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (M : Submodule R V) (hfg : M.FG) (h : Module.finrank R ↥M ≤ Module.finrank K ↥(span K ↑M)) {s : Set V} (hsM : s ⊆ ↑M) (hs : LinearIndepOn R id s) : LinearIndepOn K id s

If the R-rank of a finitely generated R-module M is at most the K-rank of the K-span of M, then every R-linearly independent subset of M is K-linearly independent.

theorem Submodule.finrank_span_eq_finrank_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {R : Type u_1} [CommRing R] [Nontrivial R] [SMulWithZero R K] [FaithfulSMul R K] [IsScalarTower R K K] [Module R V] [IsScalarTower R K V] (M : Submodule R V) (hfg : M.FG) : Module.finrank K ↥(span K ↑M) = Module.finrank R ↥M ↔ ∀ s ⊆ ↑M, LinearIndepOn R id s → LinearIndepOn K id s

The K-rank of the K-span of a finitely generated M is equal to the R-rank of M if and only if every R-linearly independent subset of M is K-linearly independent. See also Submodule.finrank_span_eq_finrank for an equality in a different setting.