Mathlib.LinearAlgebra.Dimension.Finrank

Module docstring

{"# 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. "}

Module.finrank definition

(R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] : ℕ

Full source

/-- 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. -/
noncomputable def finrank (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] : ℕ :=
  Cardinal.toNat (Module.rank R M)

Finite rank of a module

Informal description

The finite rank of a module $M$ over a ring $R$ is defined as the natural number corresponding to the supremum of the cardinalities of all $R$-linearly independent subsets of $M$. If this supremum is infinite, the finite rank is defined to be $0$ by convention. For a finite-dimensional vector space $V$ over a field $k$, this coincides with the dimension of $V$ over $k$.

Module.finrank_eq_of_rank_eq theorem

{n : ℕ} (h : Module.rank R M = ↑n) : finrank R M = n

Full source

theorem finrank_eq_of_rank_eq {n : ℕ} (h : Module.rank R M = ↑n) : finrank R M = n := by
  simp [finrank, h]

Finite Rank Equals Rank for Finite-Dimensional Modules

Informal description

Let $M$ be a module over a ring $R$ such that the rank of $M$ is equal to a natural number $n$ (i.e., $\text{rank}_R M = n$). Then the finite rank of $M$ is also equal to $n$ (i.e., $\text{finrank}_R M = n$).

Module.rank_eq_one_iff_finrank_eq_one theorem

: Module.rank R M = 1 ↔ finrank R M = 1

Full source

lemma rank_eq_one_iff_finrank_eq_one : Module.rankModule.rank R M = 1 ↔ finrank R M = 1 :=
  Cardinal.toNat_eq_one.symm

Equivalence of Rank and Finite Rank for Dimension One

Informal description

For a module $M$ over a ring $R$, the rank of $M$ is equal to $1$ if and only if the finite rank of $M$ is equal to $1$. In other words: \[ \text{rank}_R M = 1 \leftrightarrow \text{finrank}_R M = 1 \]

Module.rank_eq_ofNat_iff_finrank_eq_ofNat theorem

(n : ℕ) [Nat.AtLeastTwo n] : Module.rank R M = OfNat.ofNat n ↔ finrank R M = OfNat.ofNat n

Full source

/-- This is like `rank_eq_one_iff_finrank_eq_one` but works for `2`, `3`, `4`, ... -/
lemma rank_eq_ofNat_iff_finrank_eq_ofNat (n : ℕ) [Nat.AtLeastTwo n] :
    Module.rankModule.rank R M = OfNat.ofNat n ↔ finrank R M = OfNat.ofNat n :=
  Cardinal.toNat_eq_ofNat.symm

Equivalence of Rank and Finite Rank for Natural Numbers $n \geq 2$

Informal description

For any natural number $n \geq 2$, the rank of a module $M$ over a ring $R$ equals $n$ if and only if the finite rank of $M$ over $R$ equals $n$. In other words: \[ \text{rank}_R M = n \leftrightarrow \text{finrank}_R M = n \]

Module.finrank_le_of_rank_le theorem

{n : ℕ} (h : Module.rank R M ≤ ↑n) : finrank R M ≤ n

Full source

theorem finrank_le_of_rank_le {n : ℕ} (h : Module.rank R M ≤ ↑n) : finrank R M ≤ n := by
  rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans_lt (nat_lt_aleph0 n)
  · exact nat_lt_aleph0 n

Finite Rank Bound from Rank Bound: $\text{rank}_R M \leq n \Rightarrow \text{finrank}_R M \leq n$

Informal description

For any natural number $n$, if the rank of a module $M$ over a ring $R$ is at most $n$ (as a cardinal), then the finite rank of $M$ over $R$ is at most $n$.

Module.finrank_lt_of_rank_lt theorem

{n : ℕ} (h : Module.rank R M < ↑n) : finrank R M < n

Full source

theorem finrank_lt_of_rank_lt {n : ℕ} (h : Module.rank R M < ↑n) : finrank R M < n := by
  rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans (nat_lt_aleph0 n)
  · exact nat_lt_aleph0 n

Finite Rank Bound from Rank Bound: $\text{rank}_R M < n \Rightarrow \text{finrank}_R M < n$

Informal description

For any natural number $n$, if the rank of a module $M$ over a ring $R$ is less than $n$ (as a cardinal), then the finite rank of $M$ over $R$ is less than $n$.

Module.lt_rank_of_lt_finrank theorem

{n : ℕ} (h : n < finrank R M) : ↑n < Module.rank R M

Full source

theorem lt_rank_of_lt_finrank {n : ℕ} (h : n < finrank R M) : ↑n < Module.rank R M := by
  rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]
  · exact nat_lt_aleph0 n
  · contrapose! h
    rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
    exact n.zero_le

Finite Rank Implies Rank Bound: $n < \text{finrank}_R M \Rightarrow \aleph_0 > n < \text{rank}_R M$

Informal description

For any natural number $n$, if $n$ is less than the finite rank of a module $M$ over a ring $R$, then the cardinality of $n$ is less than the rank of $M$.

Module.one_lt_rank_of_one_lt_finrank theorem

(h : 1 < finrank R M) : 1 < Module.rank R M

Full source

theorem one_lt_rank_of_one_lt_finrank (h : 1 < finrank R M) : 1 < Module.rank R M := by
  simpa using lt_rank_of_lt_finrank h

Finite Rank Greater Than One Implies Rank Greater Than One

Informal description

For a module $M$ over a ring $R$, if the finite rank of $M$ is greater than $1$, then the rank of $M$ is also greater than $1$.

Module.finrank_le_finrank_of_rank_le_rank theorem

 (h : lift.{w} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R N)) (h' : Module.rank R N < ℵ₀) :
  finrank R M ≤ finrank R N

Full source

theorem finrank_le_finrank_of_rank_le_rank
    (h : lift.{w} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R N))
    (h' : Module.rank R N < ℵ₀) : finrank R M ≤ finrank R N := by
  simpa only [toNat_lift] using toNat_le_toNat h (lift_lt_aleph0.mpr h')

Finite Rank Comparison under Rank Inequality: $\text{rank}_R M \leq \text{rank}_R N \Rightarrow \text{finrank}_R M \leq \text{finrank}_R N$ when $\text{rank}_R N$ is finite

Informal description

Let $M$ and $N$ be modules over a ring $R$. If the rank of $M$ (lifted to universe $w$) is less than or equal to the rank of $N$ (lifted to universe $v$), and the rank of $N$ is finite (i.e., less than $\aleph_0$), then the finite rank of $M$ is less than or equal to the finite rank of $N$.

LinearEquiv.finrank_eq theorem

(f : M ≃ₗ[R] N) : finrank R M = finrank R N

Full source

/-- The dimension of a finite dimensional space is preserved under linear equivalence. -/
theorem finrank_eq (f : M ≃ₗ[R] N) : finrank R M = finrank R N := by
  unfold finrank
  rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]

Finite Rank Preservation under Linear Equivalence: $\text{finrank}_R(M) = \text{finrank}_R(N)$

Informal description

For any linear equivalence $f \colon M \simeq_R N$ between modules $M$ and $N$ over a ring $R$, the finite rank of $M$ is equal to the finite rank of $N$, i.e., $\text{finrank}_R(M) = \text{finrank}_R(N)$.

LinearEquiv.finrank_map_eq theorem

(f : M ≃ₗ[R] N) (p : Submodule R M) : finrank R (p.map (f : M →ₗ[R] N)) = finrank R p

Full source

/-- Pushforwards of finite-dimensional submodules along a `LinearEquiv` have the same finrank. -/
theorem finrank_map_eq (f : M ≃ₗ[R] N) (p : Submodule R M) :
    finrank R (p.map (f : M →ₗ[R] N)) = finrank R p :=
  (f.submoduleMap p).finrank_eq.symm

Finite Rank Preservation under Linear Equivalence Pushforward: $\text{finrank}_R(f(p)) = \text{finrank}_R(p)$

Informal description

Let $f \colon M \simeq_R N$ be a linear equivalence between modules $M$ and $N$ over a ring $R$, and let $p$ be a submodule of $M$. Then the finite rank of the pushforward submodule $f(p)$ is equal to the finite rank of $p$, i.e., $\text{finrank}_R(f(p)) = \text{finrank}_R(p)$.

LinearMap.finrank_range_of_inj theorem

{f : M →ₗ[R] N} (hf : Function.Injective f) : finrank R (LinearMap.range f) = finrank R M

Full source

/-- The dimensions of the domain and range of an injective linear map are equal. -/
theorem LinearMap.finrank_range_of_inj {f : M →ₗ[R] N} (hf : Function.Injective f) :
    finrank R (LinearMap.range f) = finrank R M := by rw [(LinearEquiv.ofInjective f hf).finrank_eq]

Finite Rank Preservation under Injective Linear Maps: $\text{finrank}_R(\text{range}(f)) = \text{finrank}_R(M)$

Informal description

Let $R$ be a semiring, and let $M$ and $N$ be modules over $R$. For any injective linear map $f \colon M \to N$, the finite rank of the range of $f$ is equal to the finite rank of $M$, i.e., $\text{finrank}_R(\text{range}(f)) = \text{finrank}_R(M)$.

Submodule.finrank_map_subtype_eq theorem

(p : Submodule R M) (q : Submodule R p) : finrank R (q.map p.subtype) = finrank R q

Full source

@[simp]
theorem Submodule.finrank_map_subtype_eq (p : Submodule R M) (q : Submodule R p) :
    finrank R (q.map p.subtype) = finrank R q :=
  (Submodule.equivSubtypeMap p q).symm.finrank_eq

Finite Rank Preservation under Submodule Inclusion: $\text{finrank}_R(q.\text{map}(p.\text{subtype})) = \text{finrank}_R(q)$

Informal description

For any submodule $p$ of an $R$-module $M$ and any submodule $q$ of $p$, the finite rank of the image of $q$ under the inclusion map $p \hookrightarrow M$ is equal to the finite rank of $q$, i.e., $\text{finrank}_R(q.\text{map}(p.\text{subtype})) = \text{finrank}_R(q)$.

finrank_top theorem

: finrank R (⊤ : Submodule R M) = finrank R M

Full source

@[simp]
theorem finrank_top : finrank R (⊤ : Submodule R M) = finrank R M := by
  unfold finrank
  simp

Finite Rank of Top Submodule Equals Finite Rank of Module: $\text{finrank}_R(\top) = \text{finrank}_R(M)$

Informal description

The finite rank of the top submodule of an $R$-module $M$ is equal to the finite rank of $M$ itself, i.e., $\text{finrank}_R(\top) = \text{finrank}_R(M)$.