# Finite dimension of vector spaces #

Definition of the rank of a module, or dimension of a vector space, as a natural number.

## Main definitions #

Defined is `Module.finrank`, the dimension of a finite-dimensional space, returning a `Nat`, as opposed to `Module.rank`, which returns a `Cardinal`. When the space has infinite dimension, its `finrank` is by convention set to `0`.

The definition of `finrank` does not assume a `FiniteDimensional` instance, but lemmas might. Import `LinearAlgebra.FiniteDimensional` to get access to these additional lemmas.

Formulas for the dimension are given for linear equivs, in `LinearEquiv.finrank_eq`.

## Implementation notes #

Most results are deduced from the corresponding results for the general dimension (as a cardinal), in `Dimension.lean`. Not all results have been ported yet.

You should not assume that there has been any effort to state lemmas as generally as possible.

source
noncomputable def Module.finrank (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
ℕ

The rank of a module as a natural number.

For a finite-dimensional vector space `V` over a field `k`, `Module.finrank k V` is equal to the dimension of `V` over `k`.

For a general module `M` over a ring `R`, `Module.finrank R M` is defined to be the supremum of the cardinalities of the `R`-linearly independent subsets of `M`, if this supremum is finite. It is defined by convention to be `0` if this supremum is infinite. See `Module.rank` for a cardinal-valued version where infinite rank modules have rank an infinite cardinal.

Note that if `R` is not a field then there can exist modules `M` with `¬(Module.Finite R M)` but `finrank R M ≠ 0`. For example `ℚ` has `finrank` equal to `1` over `ℤ`, because the nonempty `ℤ`-linearly independent subsets of `ℚ` are precisely the nonzero singletons.

Equations

- Module.finrank R M = Cardinal.toNat (Module.rank R M)

Instances For

source
@[simp]
theorem Module.finrank_subsingleton {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] :
finrank R M = 1
source
theorem Module.finrank_eq_of_rank_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (h : Module.rank R M = ↑n) :
finrank R M = n
source
theorem Module.rank_eq_one_iff_finrank_eq_one {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
Module.rank R M = 1 ↔ finrank R M = 1
source
theorem Module.rank_eq_ofNat_iff_finrank_eq_ofNat {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) [n.AtLeastTwo] :
Module.rank R M = OfNat.ofNat n ↔ finrank R M = OfNat.ofNat n

This is like `rank_eq_one_iff_finrank_eq_one` but works for `2`, `3`, `4`, ...

source
theorem Module.finrank_le_of_rank_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (h : Module.rank R M ≤ ↑n) :
finrank R M ≤ n
source
theorem Module.finrank_lt_of_rank_lt {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (h : Module.rank R M < ↑n) :
finrank R M < n
source
theorem Module.lt_rank_of_lt_finrank {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (h : n < finrank R M) :
↑n < Module.rank R M
source
theorem Module.one_lt_rank_of_one_lt_finrank {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (h : 1 < finrank R M) :
1 < Module.rank R M
source
theorem Module.finrank_le_finrank_of_rank_le_rank {R : Type u} {M : Type v} {N : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (h : Cardinal.lift.{w, v} (Module.rank R M) ≤ Cardinal.lift.{v, w} (Module.rank R N)) (h' : Module.rank R N < Cardinal.aleph0) :
finrank R M ≤ finrank R N
source
theorem LinearEquiv.finrank_eq {R : Type u} {M : Type v} {N : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) :
Module.finrank R M = Module.finrank R N

The dimension of a finite-dimensional space is preserved under linear equivalence.

source
theorem LinearEquiv.finrank_map_eq {R : Type u} {M : Type v} {N : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) (p : Submodule R M) :
Module.finrank R ↥(Submodule.map (↑f) p) = Module.finrank R ↥p

Pushforwards of finite-dimensional submodules along a `LinearEquiv` have the same finrank.

source
theorem LinearMap.finrank_range_of_inj {R : Type u} {M : Type v} {N : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) :
Module.finrank R ↥(range f) = Module.finrank R M

The dimensions of the domain and range of an injective linear map are equal.

source
@[simp]
theorem Submodule.finrank_map_subtype_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) :
Module.finrank R ↥(map p.subtype q) = Module.finrank R ↥q
source
@[simp]
theorem finrank_top (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
Module.finrank R ↥⊤ = Module.finrank R M
source
theorem Algebra.finrank_eq_of_equiv_equiv {R₀ : Type u_1} {S₀ : Type u_2} [CommSemiring R₀] [Semiring S₀] [Algebra R₀ S₀] {R₁ : Type u_3} {S₁ : Type u_4} [CommSemiring R₁] [Semiring S₁] [Algebra R₁ S₁] (i : R₀ ≃+* R₁) (j : S₀ ≃+* S₁) (hc : (algebraMap R₁ S₁).comp i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀)) :
Module.finrank R₀ S₀ = Module.finrank R₁ S₁

If `S₀ / R₀` and `S₁ / R₁` are algebras, `i : R₀ ≃+* R₁` and `j : S₀ ≃+* S₁` are ring isomorphisms, such that `R₀ → R₁ → S₁` and `R₀ → S₀ → S₁` commute, then the `finrank` of `S₀ / R₀` is equal to the finrank of `S₁ / R₁`.