Dimension of modules and vector spaces

Main definitions

• The rank of a module is defined as Module.rank : Cardinal. This is defined as the supremum of the cardinalities of linearly independent subsets.

Main statements

• LinearMap.rank_le_of_injective: the source of an injective linear map has dimension at most that of the target.
• LinearMap.rank_le_of_surjective: the target of a surjective linear map has dimension at most that of that source.

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.

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 (ι := { x : M // x ∈ s }) R Subtype.val }), Cardinal.mk ↑↑ι

@[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

• Module.rank = wrapped✝.1

theorem rank_le_card (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Module.rank R M ≤ Cardinal.mk M

theorem nonempty_linearIndependent_set (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Nonempty { s : Set M // LinearIndependent (ι := { x : M // x ∈ s }) R Subtype.val }

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)

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

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

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

@[deprecated LinearIndependent.cardinal_lift_le_rank]

theorem cardinal_lift_le_rank_of_linearIndependent {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)

Alias of LinearIndependent.cardinal_lift_le_rank.

@[deprecated LinearIndependent.cardinal_lift_le_rank]

theorem cardinal_lift_le_rank_of_linearIndependent' {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)

Alias of LinearIndependent.cardinal_lift_le_rank.

@[deprecated LinearIndependent.cardinal_le_rank]

theorem cardinal_le_rank_of_linearIndependent {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

Alias of LinearIndependent.cardinal_le_rank.

@[deprecated LinearIndependent.cardinal_le_rank']

theorem cardinal_le_rank_of_linearIndependent' {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

Alias of LinearIndependent.cardinal_le_rank'.

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

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

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

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

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

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

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 : RingHom.comp (RingHom.comp j (algebraMap R S)) 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'.

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 : RingHom.comp (algebraMap R' S') i = RingHom.comp j (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'.

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 : RingHom.comp (algebraMap R' S') (RingEquiv.toRingHom i) = RingHom.comp (RingEquiv.toRingHom j) (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'.

theorem Algebra.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 : RingHom.comp (RingHom.comp j (algebraMap R S)) i = algebraMap R' S') : Module.rank R S ≤ Module.rank R' S'

The same-universe version of Algebra.lift_rank_le_of_injective_injective.

theorem Algebra.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 : RingHom.comp (algebraMap R' S') i = RingHom.comp j (algebraMap R S)) : Module.rank R S ≤ Module.rank R' S'

The same-universe version of Algebra.lift_rank_le_of_surjective_injective.

theorem Algebra.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 : RingHom.comp (algebraMap R' S') (RingEquiv.toRingHom i) = RingHom.comp (RingEquiv.toRingHom j) (algebraMap R S)) : Module.rank R S = Module.rank R' S'

The same-universe version of Algebra.lift_rank_eq_of_equiv_equiv.

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

theorem LinearMap.rank_le_of_injective {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (i : Function.Injective ⇑f) : Module.rank R M ≤ Module.rank R M₁

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

theorem rank_range_le {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) : Module.rank R ↥(LinearMap.range f) ≤ Module.rank R M

theorem lift_rank_map_le {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R 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)

theorem rank_map_le {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) : Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

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

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

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

theorem lift_rank_range_of_injective {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R 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)

theorem rank_range_of_injective {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (h : Function.Injective ⇑f) : Module.rank R ↥(LinearMap.range f) = Module.rank R M

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

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

@[simp]

theorem rank_top (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : Module.rank R ↥⊤ = Module.rank R M

theorem rank_range_of_surjective {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (h : Function.Surjective ⇑f) : Module.rank R ↥(LinearMap.range f) = Module.rank R M'

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

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

theorem LinearMap.rank_le_of_surjective {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (h : Function.Surjective ⇑f) : Module.rank R M₁ ≤ Module.rank R M

@[simp]

theorem rank_subsingleton {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Subsingleton R] : Module.rank R M = 1