Dimension of modules and vector spaces

Main definitions

• The rank of a module is defined as Module.rank : Cardinal. This is defined as the supremum of the cardinalities of linearly independent subsets.

• The rank of a linear map is defined as the rank of its range.

Main statements

• LinearMap.rank_le_of_injective: the source of an injective linear map has dimension at most that of the target.
• LinearMap.rank_le_of_surjective: the target of a surjective linear map has dimension at most that of that source.
• basis_finite_of_finite_spans: the existence of a finite spanning set implies that any basis is finite.
• infinite_basis_le_maximal_linearIndependent: if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

For modules over rings satisfying the rank condition

• Basis.le_span: the cardinality of a basis is bounded by the cardinality of any spanning set

For modules over rings satisfying the strong rank condition

• linearIndependent_le_span: For any linearly independent family v : ι → M and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.
• linearIndependent_le_basis: If b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

For modules over rings with invariant basis number (including all commutative rings and all noetherian rings)

• mk_eq_mk_of_basis: the dimension theorem, any two bases of the same vector space have the same cardinality.

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

• rank_quotient_add_rank: if V₁ is a submodule of V, then Module.rank (V/V₁) + Module.rank V₁ = Module.rank V.
• rank_range_add_rank_ker: the rank-nullity theorem.

Implementation notes

Many theorems in this file are not universe-generic when they relate dimensions in different universes. They should be as general as they can be without inserting lifts. The types V, V', ... all live in different universes, and V₁, V₂, ... all live in the same universe.

@[irreducible]

def Module.rank (K : Type u_2) (V : Type u_3) [Semiring K] [AddCommMonoid V] [Module K V] : Cardinal.{u_3}

The rank of a module, defined as a term of type Cardinal.

We define this as the supremum of the cardinalities of linearly independent subsets.

For a free module over any ring satisfying the strong rank condition (e.g. left-noetherian rings, commutative rings, and in particular division rings and fields), this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

The definition is marked as protected to avoid conflicts with _root_.rank, the rank of a linear map.

Equations

• Module.rank = wrapped✝.1

theorem Module.rank_def (K : Type u_2) (V : Type u_3) [Semiring K] [AddCommMonoid V] [Module K V] : Module.rank K V = ⨆ (ι : { s : Set V // LinearIndependent (ι := { x : V // x ∈ s }) K Subtype.val }), Cardinal.mk ↑↑ι

theorem LinearMap.lift_rank_le_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type v'} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (i : Function.Injective ⇑f) : Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R M')

theorem LinearMap.rank_le_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (i : Function.Injective ⇑f) : Module.rank R M ≤ Module.rank R M₁

theorem rank_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {n : ℕ} (H : ∀ (s : Finset M), (LinearIndependent R fun (i : { x : M // x ∈ s }) => ↑i) → Finset.card s ≤ n) : Module.rank R M ≤ ↑n

theorem lift_rank_range_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type v'} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') : Cardinal.lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) ≤ Cardinal.lift.{v', v} (Module.rank R M)

The rank of the range of a linear map is at most the rank of the source.

theorem rank_range_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) : Module.rank R ↥(LinearMap.range f) ≤ Module.rank R M

theorem lift_rank_map_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type v'} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) : Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ Cardinal.lift.{v', v} (Module.rank R ↥p)

theorem rank_map_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) : Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

theorem rank_le_of_submodule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : Submodule R M) (t : Submodule R M) (h : s ≤ t) : Module.rank R ↥s ≤ Module.rank R ↥t

theorem LinearEquiv.lift_rank_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type v'} [AddCommGroup M'] [Module R M'] (f : M ≃ₗ[R] M') : Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')

Two linearly equivalent vector spaces have the same dimension, a version with different universes.

theorem LinearEquiv.rank_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M ≃ₗ[R] M₁) : Module.rank R M = Module.rank R M₁

Two linearly equivalent vector spaces have the same dimension.

theorem rank_range_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (h : Function.Injective ⇑f) : Module.rank R ↥(LinearMap.range f) = Module.rank R M

theorem LinearEquiv.rank_map_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M ≃ₗ[R] M₁) (p : Submodule R M) : Module.rank R ↥(Submodule.map (↑f) p) = Module.rank R ↥p

Pushforwards of submodules along a LinearEquiv have the same dimension.

@[simp]

theorem rank_top (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] : Module.rank R ↥⊤ = Module.rank R M

theorem rank_range_of_surjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M' : Type v'} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (h : Function.Surjective ⇑f) : Module.rank R ↥(LinearMap.range f) = Module.rank R M'

theorem rank_submodule_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : Submodule R M) : Module.rank R ↥s ≤ Module.rank R M

theorem LinearMap.rank_le_of_surjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (h : Function.Surjective ⇑f) : Module.rank R M₁ ≤ Module.rank R M

theorem rank_quotient_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (p : Submodule R M) : Module.rank R (M ⧸ p) ≤ Module.rank R M

theorem cardinal_lift_le_rank_of_linearIndependent {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type w} {v : ι → M} (hv : LinearIndependent R v) : Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)

theorem cardinal_lift_le_rank_of_linearIndependent' {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type w} {v : ι → M} (hv : LinearIndependent R v) : Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)

theorem cardinal_le_rank_of_linearIndependent {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type v} {v : ι → M} (hv : LinearIndependent R v) : Cardinal.mk ι ≤ Module.rank R M

theorem cardinal_le_rank_of_linearIndependent' {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {s : Set M} (hs : LinearIndependent R fun (x : ↑s) => ↑x) : Cardinal.mk ↑s ≤ Module.rank R M

@[simp]

theorem rank_punit (R : Type u) [Ring R] [Nontrivial R] : Module.rank R PUnit.{u_2 + 1} = 0

@[simp]

theorem rank_bot (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [Nontrivial R] : Module.rank R ↥⊥ = 0

theorem exists_mem_ne_zero_of_rank_pos {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {s : Submodule R M} (h : 0 < Module.rank R ↥s) : ∃ b ∈ s, b ≠ 0

theorem LinearIndependent.finite_of_isNoetherian {ι : Type w} {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] [IsNoetherian R M] {v : ι → M} (hv : LinearIndependent R v) : Finite ι

A linearly-independent family of vectors in a module over a non-trivial ring must be finite if the module is Noetherian.

theorem LinearIndependent.set_finite_of_isNoetherian {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] [IsNoetherian R M] {s : Set M} (hi : LinearIndependent (ι := { x : M // x ∈ s }) R Subtype.val) : Set.Finite s

theorem basis_finite_of_finite_spans {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] (w : Set M) (hw : Set.Finite w) (s : Submodule.span R w = ⊤) {ι : Type w} (b : Basis ι R M) : Finite ι

Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.

theorem union_support_maximal_linearIndependent_eq_range_basis {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type w} (b : Basis ι R M) {κ : Type w'} (v : κ → M) (i : LinearIndependent R v) (m : LinearIndependent.Maximal i) : ⋃ (k : κ), ↑(b.repr (v k)).support = Set.univ

Over any ring R, if b is a basis for a module M, and s is a maximal linearly independent set, then the union of the supports of x ∈ s (when written out in the basis b) is all of b.

theorem infinite_basis_le_maximal_linearIndependent' {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w'} (v : κ → M) (i : LinearIndependent R v) (m : LinearIndependent.Maximal i) : Cardinal.lift.{w', w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, w'} (Cardinal.mk κ)

Over any ring R, if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

theorem infinite_basis_le_maximal_linearIndependent {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) (m : LinearIndependent.Maximal i) : Cardinal.mk ι ≤ Cardinal.mk κ

Over any ring R, if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

theorem CompleteLattice.Independent.subtype_ne_bot_le_rank {ι : Type w} {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] {V : ι → Submodule R M} (hV : CompleteLattice.Independent V) : Cardinal.lift.{v, w} (Cardinal.mk { i : ι // V i ≠ ⊥ }) ≤ Cardinal.lift.{w, v} (Module.rank R M)

@[simp]

theorem rank_subsingleton {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Subsingleton R] : Module.rank R M = 1

theorem rank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial M] : 0 < Module.rank R M

theorem rank_zero_iff_forall_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial R] : Module.rank R M = 0 ↔ ∀ (x : M), x = 0

theorem rank_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial R] : Module.rank R M = 0 ↔ Subsingleton M

See rank_subsingleton for the reason that Nontrivial R is needed.

theorem rank_pos_iff_exists_ne_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial R] : 0 < Module.rank R M ↔ ∃ (x : M), x ≠ 0

theorem rank_pos_iff_nontrivial {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial R] : 0 < Module.rank R M ↔ Nontrivial M

theorem mk_eq_mk_of_basis {ι : Type w} {ι' : Type w'} {R : Type u} [Ring R] [InvariantBasisNumber R] {M : Type v} [AddCommGroup M] [Module R M] (v : Basis ι R M) (v' : Basis ι' R M) : Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')

The dimension theorem: if v and v' are two bases, their index types have the same cardinalities.

def Basis.indexEquiv {ι : Type w} {ι' : Type w'} {R : Type u} [Ring R] [InvariantBasisNumber R] {M : Type v} [AddCommGroup M] [Module R M] (v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι'

Given two bases indexed by ι and ι' of an R-module, where R satisfies the invariant basis number property, an equiv ι ≃ ι'.

Equations

• Basis.indexEquiv v v' = Nonempty.some (_ : Nonempty (ι ≃ ι'))

theorem mk_eq_mk_of_basis' {ι : Type w} {R : Type u} [Ring R] [InvariantBasisNumber R] {M : Type v} [AddCommGroup M] [Module R M] {ι' : Type w} (v : Basis ι R M) (v' : Basis ι' R M) : Cardinal.mk ι = Cardinal.mk ι'

theorem Basis.le_span'' {R : Type u} [Ring R] [RankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} [Fintype ι] (b : Basis ι R M) {w : Set M} [Fintype ↑w] (s : Submodule.span R w = ⊤) : Fintype.card ι ≤ Fintype.card ↑w

An auxiliary lemma for Basis.le_span.

If R satisfies the rank condition, then for any finite basis b : Basis ι R M, and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.

theorem basis_le_span' {R : Type u} [Ring R] [RankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (b : Basis ι R M) {w : Set M} [Fintype ↑w] (s : Submodule.span R w = ⊤) : Cardinal.mk ι ≤ ↑(Fintype.card ↑w)

Another auxiliary lemma for Basis.le_span, which does not require assuming the basis is finite, but still assumes we have a finite spanning set.

theorem Basis.le_span {ι : Type w} {R : Type u} [Ring R] [RankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {J : Set M} (v : Basis ι R M) (hJ : Submodule.span R J = ⊤) : Cardinal.mk ↑(Set.range ⇑v) ≤ Cardinal.mk ↑J

If R satisfies the rank condition, then the cardinality of any basis is bounded by the cardinality of any spanning set.

theorem linearIndependent_le_span_aux' {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} [Fintype ι] (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Set.range v ≤ ↑(Submodule.span R w)) : Fintype.card ι ≤ Fintype.card ↑w

def linearIndependentFintypeOfLeSpanFintype {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Set.range v ≤ ↑(Submodule.span R w)) : Fintype ι

If R satisfies the strong rank condition, then any linearly independent family v : ι → M contained in the span of some finite w : Set M, is itself finite.

Equations

• linearIndependentFintypeOfLeSpanFintype v i w s = fintypeOfFinsetCardLe (Fintype.card ↑w) (_ : ∀ (t : Finset ι), Finset.card t ≤ Fintype.card ↑w)

theorem linearIndependent_le_span' {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Set.range v ≤ ↑(Submodule.span R w)) : Cardinal.mk ι ≤ ↑(Fintype.card ↑w)

If R satisfies the strong rank condition, then for any linearly independent family v : ι → M contained in the span of some finite w : Set M, the cardinality of ι is bounded by the cardinality of w.

theorem linearIndependent_le_span {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Submodule.span R w = ⊤) : Cardinal.mk ι ≤ ↑(Fintype.card ↑w)

If R satisfies the strong rank condition, then for any linearly independent family v : ι → M and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.

theorem linearIndependent_le_span_finset {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (v : ι → M) (i : LinearIndependent R v) (w : Finset M) (s : Submodule.span R ↑w = ⊤) : Cardinal.mk ι ≤ ↑(Finset.card w)

A version of linearIndependent_le_span for Finset.

theorem linearIndependent_le_infinite_basis {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) : Cardinal.mk κ ≤ Cardinal.mk ι

An auxiliary lemma for linearIndependent_le_basis: we handle the case where the basis b is infinite.

theorem linearIndependent_le_basis {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type w} (b : Basis ι R M) {κ : Type w} (v : κ → M) (i : LinearIndependent R v) : Cardinal.mk κ ≤ Cardinal.mk ι

Over any ring R satisfying the strong rank condition, if b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

theorem Basis.card_le_card_of_linearIndependent_aux {R : Type u_2} [Ring R] [StrongRankCondition R] (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n

Let R satisfy the strong rank condition. If m elements of a free rank n R-module are linearly independent, then m ≤ n.

theorem maximal_linearIndependent_eq_infinite_basis {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) (m : LinearIndependent.Maximal i) : Cardinal.mk κ = Cardinal.mk ι

Over any ring R satisfying the strong rank condition, if b is an infinite basis for a module M, then every maximal linearly independent set has the same cardinality as b.

This proof (along with some of the lemmas above) comes from [Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]

theorem Basis.mk_eq_rank'' {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type v} (v : Basis ι R M) : Cardinal.mk ι = Module.rank R M

theorem Basis.mk_range_eq_rank {ι : Type w} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] (v : Basis ι R M) : Cardinal.mk ↑(Set.range ⇑v) = Module.rank R M

theorem rank_eq_card_basis {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type w} [Fintype ι] (h : Basis ι R M) : Module.rank R M = ↑(Fintype.card ι)

If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the cardinality of the basis.

theorem Basis.card_le_card_of_linearIndependent {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} [Fintype ι] (b : Basis ι R M) {ι' : Type u_3} [Fintype ι'] {v : ι' → M} (hv : LinearIndependent R v) : Fintype.card ι' ≤ Fintype.card ι

theorem Basis.card_le_card_of_submodule {ι : Type w} {ι' : Type w'} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] (N : Submodule R M) [Fintype ι] (b : Basis ι R M) [Fintype ι'] (b' : Basis ι' R ↥N) : Fintype.card ι' ≤ Fintype.card ι

theorem Basis.card_le_card_of_le {ι : Type w} {ι' : Type w'} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {N : Submodule R M} {O : Submodule R M} (hNO : N ≤ O) [Fintype ι] (b : Basis ι R ↥O) [Fintype ι'] (b' : Basis ι' R ↥N) : Fintype.card ι' ≤ Fintype.card ι

theorem Basis.mk_eq_rank {ι : Type w} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] (v : Basis ι R M) : Cardinal.lift.{v, w} (Cardinal.mk ι) = Cardinal.lift.{w, v} (Module.rank R M)

theorem Basis.mk_eq_rank' {ι : Type w} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] (v : Basis ι R M) : Cardinal.lift.{max v m, w} (Cardinal.mk ι) = Cardinal.lift.{max w m, v} (Module.rank R M)

theorem Basis.nonempty_fintype_index_of_rank_lt_aleph0 {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (b : Basis ι R M) (h : Module.rank R M < Cardinal.aleph0) : Nonempty (Fintype ι)

If a module has a finite dimension, all bases are indexed by a finite type.

noncomputable def Basis.fintypeIndexOfRankLtAleph0 {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} (b : Basis ι R M) (h : Module.rank R M < Cardinal.aleph0) : Fintype ι

If a module has a finite dimension, all bases are indexed by a finite type.

Equations

• Basis.fintypeIndexOfRankLtAleph0 b h = Classical.choice (_ : Nonempty (Fintype ι))

theorem Basis.finite_index_of_rank_lt_aleph0 {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {ι : Type u_2} {s : Set ι} (b : Basis (↑s) R M) (h : Module.rank R M < Cardinal.aleph0) : Set.Finite s

If a module has a finite dimension, all bases are indexed by a finite set.

theorem rank_span {ι : Type w} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {v : ι → M} (hv : LinearIndependent R v) : Module.rank R ↥(Submodule.span R (Set.range v)) = Cardinal.mk ↑(Set.range v)

theorem rank_span_set {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] {s : Set M} (hs : LinearIndependent R fun (x : ↑s) => ↑x) : Module.rank R ↥(Submodule.span R s) = Cardinal.mk ↑s

def Submodule.inductionOnRank {ι : Type w} {R : Type u} [Ring R] [StrongRankCondition R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] [Fintype ι] (b : Basis ι R M) (P : Submodule R M → Sort u_2) (ih : (N : Submodule R M) → ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N) (N : Submodule R M) : P N

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.

Equations

• Submodule.inductionOnRank b P ih N = Submodule.inductionOnRankAux b P ih (Fintype.card ι) N (_ : ∀ {m : ℕ} (hs : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ hs) → m ≤ Fintype.card ι)

theorem Ideal.rank_eq {R : Type u_2} {S : Type u_3} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S] [Algebra R S] {n : Type u_4} {m : Type u_5} [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

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.

@[simp]

theorem rank_self (R : Type u) [Ring R] [StrongRankCondition R] : Module.rank R R = 1

theorem Module.Free.rank_eq_card_chooseBasisIndex (K : Type u) (V : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] : Module.rank K V = Cardinal.mk (Module.Free.ChooseBasisIndex K V)

The rank of a free module M over R is the cardinality of ChooseBasisIndex R M.

theorem Module.Free.rank_eq_mk_of_infinite_lt (K : Type u) (V : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Infinite K] (h_lt : Cardinal.lift.{v, u} (Cardinal.mk K) < Cardinal.lift.{u, v} (Cardinal.mk V)) : Module.rank K V = Cardinal.mk V

The rank of a free module V over an infinite scalar ring K is the cardinality of V whenever #R < #V.

theorem nonempty_linearEquiv_of_lift_rank_eq {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V'] [Module K V'] [Module.Free K V'] (cnd : Cardinal.lift.{v', v} (Module.rank K V) = Cardinal.lift.{v, v'} (Module.rank K V')) : Nonempty (V ≃ₗ[K] V')

Two vector spaces are isomorphic if they have the same dimension.

theorem nonempty_linearEquiv_of_rank_eq {K : Type u} {V : Type v} {V₁ : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V₁] [Module K V₁] [Module.Free K V₁] (cond : Module.rank K V = Module.rank K V₁) : Nonempty (V ≃ₗ[K] V₁)

Two vector spaces are isomorphic if they have the same dimension.

def LinearEquiv.ofLiftRankEq {K : Type u} (V : Type v) (V' : Type v') [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V'] [Module K V'] [Module.Free K V'] (cond : Cardinal.lift.{v', v} (Module.rank K V) = Cardinal.lift.{v, v'} (Module.rank K V')) : V ≃ₗ[K] V'

Two vector spaces are isomorphic if they have the same dimension.

Equations

• LinearEquiv.ofLiftRankEq V V' cond = Classical.choice (_ : Nonempty (V ≃ₗ[K] V'))

def LinearEquiv.ofRankEq {K : Type u} (V : Type v) (V₁ : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V₁] [Module K V₁] [Module.Free K V₁] (cond : Module.rank K V = Module.rank K V₁) : V ≃ₗ[K] V₁

Two vector spaces are isomorphic if they have the same dimension.

Equations

• LinearEquiv.ofRankEq V V₁ cond = Classical.choice (_ : Nonempty (V ≃ₗ[K] V₁))

theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V'] [Module K V'] [Module.Free K V'] : Nonempty (V ≃ₗ[K] V') ↔ Cardinal.lift.{v', v} (Module.rank K V) = Cardinal.lift.{v, v'} (Module.rank K V')

Two vector spaces are isomorphic if and only if they have the same dimension.

theorem LinearEquiv.nonempty_equiv_iff_rank_eq {K : Type u} {V : Type v} {V₁ : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V₁] [Module K V₁] [Module.Free K V₁] : Nonempty (V ≃ₗ[K] V₁) ↔ Module.rank K V = Module.rank K V₁

Two vector spaces are isomorphic if and only if they have the same dimension.

@[simp]

theorem rank_prod {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V'] [Module K V'] [Module.Free K V'] : Module.rank K (V × V') = Cardinal.lift.{v', v} (Module.rank K V) + Cardinal.lift.{v, v'} (Module.rank K V')

If M and N are free, then the rank of M × N is (Module.rank R M).lift + (Module.rank R N).lift.

theorem rank_prod' {K : Type u} {V : Type v} {V₁ : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [AddCommGroup V₁] [Module K V₁] [Module.Free K V₁] : Module.rank K (V × V₁) = Module.rank K V + Module.rank K V₁

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).

@[simp]

theorem rank_ulift {K : Type u} {V : Type v} [Ring K] [AddCommGroup V] [Module K V] : Module.rank K (ULift.{w, v} V) = Cardinal.lift.{w, v} (Module.rank K V)

@[simp]

theorem rank_pi {K : Type u} {η : Type u₁'} {φ : η → Type u_1} [Ring K] [StrongRankCondition K] [(i : η) → AddCommGroup (φ i)] [(i : η) → Module K (φ i)] [∀ (i : η), Module.Free K (φ i)] [Finite η] : Module.rank K ((i : η) → φ i) = Cardinal.sum fun (i : η) => Module.rank K (φ i)

The rank of a finite product of free modules is the sum of the ranks.

theorem rank_fun {K : Type u} [Ring K] [StrongRankCondition K] {V : Type u} {η : Type u} [Fintype η] [AddCommGroup V] [Module K V] [Module.Free K V] : Module.rank K (η → V) = ↑(Fintype.card η) * Module.rank K V

theorem rank_fun_eq_lift_mul {K : Type u} {V : Type v} {η : Type u₁'} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Fintype η] : Module.rank K (η → V) = ↑(Fintype.card η) * Cardinal.lift.{u₁', v} (Module.rank K V)

theorem rank_fun' {K : Type u} {η : Type u₁'} [Ring K] [StrongRankCondition K] [Fintype η] : Module.rank K (η → K) = ↑(Fintype.card η)

theorem rank_fin_fun {K : Type u} [Ring K] [StrongRankCondition K] (n : ℕ) : Module.rank K (Fin n → K) = ↑n

def finDimVectorspaceEquiv {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] (n : ℕ) (hn : Module.rank K V = ↑n) : V ≃ₗ[K] Fin n → K

An n-dimensional K-vector space is equivalent to Fin n → K.

Equations

• One or more equations did not get rendered due to their size.

theorem 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) : Set.Finite (Basis.ofVectorSpaceIndex K V)

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

theorem rank_span_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Set V) : Module.rank K ↥(Submodule.span K s) ≤ Cardinal.mk ↑s

theorem rank_span_of_finset {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Finset V) : Module.rank K ↥(Submodule.span K ↑s) < Cardinal.aleph0

theorem rank_quotient_add_rank {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

theorem rank_range_add_rank_ker {K : Type u} {V : Type v} {V₁ : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] (f : V →ₗ[K] V₁) : Module.rank K ↥(LinearMap.range f) + Module.rank K ↥(LinearMap.ker f) = Module.rank K V

The rank-nullity theorem

theorem rank_eq_of_surjective {K : Type u} {V : Type v} {V₁ : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] (f : V →ₗ[K] V₁) (h : Function.Surjective ⇑f) : Module.rank K V = Module.rank K V₁ + Module.rank K ↥(LinearMap.ker f)

theorem exists_linearIndependent_cons_of_lt_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (h : ↑n < Module.rank K V) : ∃ (x : V), LinearIndependent K (Fin.cons x v)

Given a family of n linearly independent vectors in a space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_snoc_of_lt_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (h : ↑n < Module.rank K V) : ∃ (x : V), LinearIndependent K (Fin.snoc v x)

Given a family of n linearly independent vectors in a space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_pair_of_one_lt_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : 1 < Module.rank K V) {x : V} (hx : x ≠ 0) : ∃ (y : V), LinearIndependent K ![x, y]

Given a nonzero vector in a space of dimension > 1, one may find another vector linearly independent of the first one.

theorem rank_add_rank_split {K : Type u} {V : Type v} {V₁ : Type v} {V₂ : Type 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 : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb) (hgd : LinearMap.ker cd = ⊥) (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_sup_add_rank_inf_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t

theorem Submodule.rank_add_le_rank_add_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) : Module.rank K ↥(s ⊔ t) ≤ Module.rank K ↥s + Module.rank K ↥t

def Basis.ofRankEqZero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [IsEmpty ι] (hV : Module.rank K V = 0) : Basis ι K V

The ι indexed basis on V, where ι is an empty type and V is zero-dimensional.

See also FiniteDimensional.finBasis.

Equations

• Basis.ofRankEqZero hV = Basis.empty V

@[simp]

theorem Basis.ofRankEqZero_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [IsEmpty ι] (hV : Module.rank K V = 0) (i : ι) : (Basis.ofRankEqZero hV) i = 0

theorem le_rank_iff_exists_linearIndependent {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {c : Cardinal.{v}} : c ≤ Module.rank K V ↔ ∃ (s : Set V), Cardinal.mk ↑s = c ∧ LinearIndependent (ι := { x : V // x ∈ s }) K Subtype.val

theorem le_rank_iff_exists_linearIndependent_finset {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} : ↑n ≤ Module.rank K V ↔ ∃ (s : Finset V), Finset.card s = n ∧ LinearIndependent (ι := { x : V // x ∈ ↑s }) K Subtype.val

theorem rank_le_one_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

A vector space has dimension at most 1 if and only if there is a single vector of which all vectors are multiples.

theorem rank_submodule_le_one_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ Submodule.span K {v₀}

A submodule has dimension at most 1 if and only if there is a single vector in the submodule such that the submodule is contained in its span.

theorem rank_submodule_le_one_iff' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ Submodule.span K {v₀}

A submodule has dimension at most 1 if and only if there is a single vector, not necessarily in the submodule, such that the submodule is contained in its span.

theorem Submodule.rank_le_one_iff_isPrincipal {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (W : Submodule K V) : Module.rank K ↥W ≤ 1 ↔ Submodule.IsPrincipal W

theorem Module.rank_le_one_iff_top_isPrincipal {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : Module.rank K V ≤ 1 ↔ Submodule.IsPrincipal ⊤

The rank of a linear map

@[inline, reducible]

abbrev LinearMap.rank {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] (f : V →ₗ[K] V') : Cardinal.{v'}

rank f is the rank of a LinearMap f, defined as the dimension of f.range.

Equations

• LinearMap.rank f = Module.rank K ↥(LinearMap.range f)

theorem LinearMap.rank_le_range {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] (f : V →ₗ[K] V') : LinearMap.rank f ≤ Module.rank K V'

theorem LinearMap.rank_le_domain {K : Type u} {V : Type v} {V₁ : Type v} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] (f : V →ₗ[K] V₁) : LinearMap.rank f ≤ Module.rank K V

@[simp]

theorem LinearMap.rank_zero {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [Nontrivial K] : LinearMap.rank 0 = 0

theorem LinearMap.rank_comp_le_left {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : LinearMap.rank (f ∘ₗ g) ≤ LinearMap.rank f

theorem LinearMap.lift_rank_comp_le_right {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : Cardinal.lift.{v', v''} (LinearMap.rank (f ∘ₗ g)) ≤ Cardinal.lift.{v'', v'} (LinearMap.rank g)

theorem LinearMap.lift_rank_comp_le {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : Cardinal.lift.{v', v''} (LinearMap.rank (f ∘ₗ g)) ≤ min (Cardinal.lift.{v', v''} (LinearMap.rank f)) (Cardinal.lift.{v'', v'} (LinearMap.rank g))

The rank of the composition of two maps is less than the minimum of their ranks.

theorem LinearMap.rank_comp_le_right {K : Type u} {V : Type v} {V' : Type v'} {V'₁ : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V'₁] [Module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : LinearMap.rank (f ∘ₗ g) ≤ LinearMap.rank g

theorem LinearMap.rank_comp_le {K : Type u} {V : Type v} {V' : Type v'} {V'₁ : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V'₁] [Module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : LinearMap.rank (f ∘ₗ g) ≤ min (LinearMap.rank f) (LinearMap.rank g)

The rank of the composition of two maps is less than the minimum of their ranks.

See lift_rank_comp_le for the universe-polymorphic version.

theorem LinearMap.rank_add_le {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] (f : V →ₗ[K] V') (g : V →ₗ[K] V') : LinearMap.rank (f + g) ≤ LinearMap.rank f + LinearMap.rank g

theorem LinearMap.rank_finset_sum_le {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {η : Type u_2} (s : Finset η) (f : η → V →ₗ[K] V') : LinearMap.rank (Finset.sum s fun (d : η) => f d) ≤ Finset.sum s fun (d : η) => LinearMap.rank (f d)

theorem LinearMap.le_rank_iff_exists_linearIndependent {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {c : Cardinal.{v'}} {f : V →ₗ[K] V'} : c ≤ LinearMap.rank f ↔ ∃ (s : Set V), Cardinal.lift.{v', v} (Cardinal.mk ↑s) = Cardinal.lift.{v, v'} c ∧ LinearIndependent K fun (x : ↑s) => f ↑x

theorem LinearMap.le_rank_iff_exists_linearIndependent_finset {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {n : ℕ} {f : V →ₗ[K] V'} : ↑n ≤ LinearMap.rank f ↔ ∃ (s : Finset V), Finset.card s = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x