Documentation

Mathlib.LinearAlgebra.Dimension.Basic

Dimension of modules and vector spaces #

Main definitions #

Main statements #

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 M, M', ... all live in different universes, and M₁, M₂, ... all live in the same universe.

source
theorem Module.rank_def (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
Module.rank R M = ⨆ (ι : { s : Set M // LinearIndependent R Subtype.val }), Cardinal.mk ↑↑ι
source
@[irreducible]
def Module.rank (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
Cardinal.{u_2}

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.

Equations
Instances For
    source
    theorem rank_le_card (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
    Module.rank R M ≤ Cardinal.mk M
    source
    theorem nonempty_linearIndependent_set (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :
    Nonempty { s : Set M // LinearIndependent R Subtype.val }
    source
    theorem LinearIndependent.cardinal_lift_le_rank {R : Type u} {M : Type v} [Ring R] [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)
    source
    theorem LinearIndependent.aleph0_le_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type w} [Infinite ι] {v : ι → M} (hv : LinearIndependent R v) :
    Cardinal.aleph0 ≤ Module.rank R M
    source
    theorem LinearIndependent.cardinal_le_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type v} {v : ι → M} (hv : LinearIndependent R v) :
    Cardinal.mk ι ≤ Module.rank R M
    source
    theorem LinearIndependent.cardinal_le_rank' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {s : Set M} (hs : LinearIndependent R fun (x : ↑s) => ↑x) :
    Cardinal.mk ↑s ≤ Module.rank R M
    source
    theorem lift_rank_le_of_injective_injective {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [Ring R'] [AddCommGroup M'] [Module R' M'] (i : R' → R) (j : M →+ M') (hi : ∀ (r : R'), i r = 0 → r = 0) (hj : Function.Injective ⇑j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')

    If M / R and M' / R' are modules, i : R' → R is a map which sends non-zero elements to non-zero elements, j : M →+ M' is an injective group homomorphism, such that the scalar multiplications on M and M' are compatible, then the rank of M / R is smaller than or equal to the rank of M' / R'. As a special case, taking R = R' it is LinearMap.lift_rank_le_of_injective.

    source
    theorem lift_rank_le_of_surjective_injective {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [Ring R'] [AddCommGroup M'] [Module R' M'] (i : ZeroHom R R') (j : M →+ M') (hi : Function.Surjective ⇑i) (hj : Function.Injective ⇑j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')

    If M / R and M' / R' are modules, i : R → R' is a surjective map which maps zero to zero, j : M →+ M' is an injective group homomorphism, such that the scalar multiplications on M and M' are compatible, then the rank of M / R is smaller than or equal to the rank of M' / R'. As a special case, taking R = R' it is LinearMap.lift_rank_le_of_injective.

    source
    theorem lift_rank_eq_of_equiv_equiv {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [Ring R'] [AddCommGroup M'] [Module R' M'] (i : ZeroHom R R') (j : M ≃+ M') (hi : Function.Bijective ⇑i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R' M')

    If M / R and M' / R' are modules, i : R → R' is a bijective map which maps zero to zero, j : M ≃+ M' is a group isomorphism, such that the scalar multiplications on M and M' are compatible, then the rank of M / R is equal to the rank of M' / R'. As a special case, taking R = R' it is LinearEquiv.lift_rank_eq.

    source
    theorem rank_le_of_injective_injective {R : Type u} {R' : Type u'} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [Ring R'] [AddCommGroup M₁] [Module R' M₁] (i : R' → R) (j : M →+ M₁) (hi : ∀ (r : R'), i r = 0 → r = 0) (hj : Function.Injective ⇑j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    Module.rank R M ≤ Module.rank R' M₁

    The same-universe version of lift_rank_le_of_injective_injective.

    source
    theorem rank_le_of_surjective_injective {R : Type u} {R' : Type u'} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [Ring R'] [AddCommGroup M₁] [Module R' M₁] (i : ZeroHom R R') (j : M →+ M₁) (hi : Function.Surjective ⇑i) (hj : Function.Injective ⇑j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Module.rank R M ≤ Module.rank R' M₁

    The same-universe version of lift_rank_le_of_surjective_injective.

    source
    theorem rank_eq_of_equiv_equiv {R : Type u} {R' : Type u'} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [Ring R'] [AddCommGroup M₁] [Module R' M₁] (i : ZeroHom R R') (j : M ≃+ M₁) (hi : Function.Bijective ⇑i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Module.rank R M = Module.rank R' M₁

    The same-universe version of lift_rank_eq_of_equiv_equiv.

    source
    theorem Algebra.lift_rank_le_of_injective_injective {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {R' : Type w'} {S' : Type v'} [CommRing R'] [Ring S'] [Algebra R' S'] (i : R' →+* R) (j : S →+* S') (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') :
    Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')

    If S / R and S' / R' are algebras, i : R' →+* R and j : S →+* S' are injective ring homomorphisms, such that R' → R → S → S' and R' → S' commute, then the rank of S / R is smaller than or equal to the rank of S' / R'.

    source
    theorem Algebra.lift_rank_le_of_surjective_injective {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {R' : Type w'} {S' : Type v'} [CommRing R'] [Ring S'] [Algebra R' S'] (i : R →+* R') (j : S →+* S') (hi : Function.Surjective ⇑i) (hj : Function.Injective ⇑j) (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) :
    Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')

    If S / R and S' / R' are algebras, i : R →+* R' is a surjective ring homomorphism, j : S →+* S' is an injective ring homomorphism, such that R → R' → S' and R → S → S' commute, then the rank of S / R is smaller than or equal to the rank of S' / R'.

    source
    theorem Algebra.lift_rank_eq_of_equiv_equiv {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {R' : Type w'} {S' : Type v'} [CommRing R'] [Ring S'] [Algebra R' S'] (i : R ≃+* R') (j : S ≃+* S') (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) :
    Cardinal.lift.{v', v} (Module.rank R S) = Cardinal.lift.{v, v'} (Module.rank 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 rank of S / R is equal to the rank of S' / R'.

    source
    theorem Algebra.rank_le_of_injective_injective {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {R' : Type w'} [CommRing R'] {S' : Type v} [Ring S'] [Algebra R' S'] (i : R' →+* R) (j : S →+* S') (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') :
    Module.rank R S ≤ Module.rank R' S'

    The same-universe version of Algebra.lift_rank_le_of_injective_injective.

    source
    theorem Algebra.rank_le_of_surjective_injective {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {R' : Type w'} [CommRing R'] {S' : Type v} [Ring S'] [Algebra R' S'] (i : R →+* R') (j : S →+* S') (hi : Function.Surjective ⇑i) (hj : Function.Injective ⇑j) (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) :
    Module.rank R S ≤ Module.rank R' S'

    The same-universe version of Algebra.lift_rank_le_of_surjective_injective.

    source
    theorem Algebra.rank_eq_of_equiv_equiv {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {R' : Type w'} [CommRing R'] {S' : Type v} [Ring S'] [Algebra R' S'] (i : R ≃+* R') (j : S ≃+* S') (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) :
    Module.rank R S = Module.rank R' S'

    The same-universe version of Algebra.lift_rank_eq_of_equiv_equiv.

    source
    theorem LinearMap.lift_rank_le_of_injective {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [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')
    source
    theorem LinearMap.rank_le_of_injective {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (i : Function.Injective ⇑f) :
    Module.rank R M ≤ Module.rank R M₁
    source
    theorem lift_rank_range_le {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [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.

    source
    theorem rank_range_le {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) :
    Module.rank R ↥(LinearMap.range f) ≤ Module.rank R M
    source
    theorem lift_rank_map_le {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [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)
    source
    theorem rank_map_le {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) :
    Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p
    source
    theorem Submodule.rank_mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {t : Submodule R M} (h : s ≤ t) :
    Module.rank R ↥s ≤ Module.rank R ↥t
    source
    @[deprecated Submodule.rank_mono]
    theorem rank_le_of_submodule {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {t : Submodule R M} (h : s ≤ t) :
    Module.rank R ↥s ≤ Module.rank R ↥t

    Alias of Submodule.rank_mono.

    source
    theorem LinearEquiv.lift_rank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [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.

    source
    theorem LinearEquiv.rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [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.

    source
    theorem lift_rank_range_of_injective {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (h : Function.Injective ⇑f) :
    Cardinal.lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) = Cardinal.lift.{v', v} (Module.rank R M)
    source
    theorem rank_range_of_injective {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (h : Function.Injective ⇑f) :
    Module.rank R ↥(LinearMap.range f) = Module.rank R M
    source
    theorem LinearEquiv.lift_rank_map_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [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)
    source
    theorem LinearEquiv.rank_map_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [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.

    source
    @[simp]
    theorem rank_top (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] :
    Module.rank R ↥⊤ = Module.rank R M
    source
    theorem rank_range_of_surjective {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (h : Function.Surjective ⇑f) :
    Module.rank R ↥(LinearMap.range f) = Module.rank R M'
    source
    theorem Submodule.rank_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (s : Submodule R M) :
    Module.rank R ↥s ≤ Module.rank R M
    source
    @[deprecated Submodule.rank_le]
    theorem rank_submodule_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (s : Submodule R M) :
    Module.rank R ↥s ≤ Module.rank R M

    Alias of Submodule.rank_le.

    source
    theorem LinearMap.lift_rank_le_of_surjective {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (h : Function.Surjective ⇑f) :
    Cardinal.lift.{v, v'} (Module.rank R M') ≤ Cardinal.lift.{v', v} (Module.rank R M)
    source
    theorem LinearMap.rank_le_of_surjective {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] (f : M →ₗ[R] M₁) (h : Function.Surjective ⇑f) :
    Module.rank R M₁ ≤ Module.rank R M
    source
    @[simp]
    theorem rank_subsingleton {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Subsingleton R] :
    Module.rank R M = 1