HepLean 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] [AddCommGroup M] [Module R M] :
ℕ

The rank of a module as a natural number.

Defined by convention to be 0 if the space has infinite rank.

For a vector space M over a field R, this is the same as the finite dimension of M over R.

Note that it is possible to have M with ¬(Module.Finite R M) but finrank R M ≠ 0, for example ℤ × ℚ/ℤ has finrank equal to 1.

Equations
Instances For
    source
    @[deprecated Module.finrank]
    def FiniteDimensional.finrank (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommGroup M] [Module R M] :
    ℕ

    Alias of Module.finrank.

    The rank of a module as a natural number.

    Defined by convention to be 0 if the space has infinite rank.

    For a vector space M over a field R, this is the same as the finite dimension of M over R.

    Note that it is possible to have M with ¬(Module.Finite R M) but finrank R M ≠ 0, for example ℤ × ℚ/ℤ has finrank equal to 1.

    Equations
    Instances For
      source
      theorem Module.finrank_eq_of_rank_eq {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (h : Module.rank R M = ↑n) :
      Module.finrank R M = n
      source
      theorem Module.rank_eq_one_iff_finrank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :
      Module.rank R M = 1 ↔ Module.finrank R M = 1
      source
      theorem Module.rank_eq_ofNat_iff_finrank_eq_ofNat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (n : ℕ) [n.AtLeastTwo] :
      Module.rank R M = OfNat.ofNat n ↔ Module.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} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (h : Module.rank R M ≤ ↑n) :
      Module.finrank R M ≤ n
      source
      theorem Module.finrank_lt_of_rank_lt {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (h : Module.rank R M < ↑n) :
      Module.finrank R M < n
      source
      theorem Module.lt_rank_of_lt_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (h : n < Module.finrank R M) :
      ↑n < Module.rank R M
      source
      theorem Module.one_lt_rank_of_one_lt_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (h : 1 < Module.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} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup 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) :
      Module.finrank R M ≤ Module.finrank R N
      source
      theorem LinearEquiv.finrank_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M ≃ₗ[R] M₂) :
      Module.finrank R M = Module.finrank R M₂

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

      source
      theorem LinearEquiv.finrank_map_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M ≃ₗ[R] M₂) (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} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) :
      Module.finrank R ↥(LinearMap.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} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) :
      Module.finrank R ↥(Submodule.map p.subtype q) = Module.finrank R ↥q
      source
      @[simp]
      theorem finrank_top (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] :
      Module.finrank R ↥⊤ = Module.finrank R M