Documentation

Mathlib.LinearAlgebra.Dimension.Finrank

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