mathlib documentation

linear_algebra.dimension

Dimension of modules and vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
The rank of a linear map is defined as the rank of its range.

Main statements #

linear_map.rank_le_of_injective: the source of an injective linear map has dimension at most that of the target.
linear_map.rank_le_of_surjective: the target of a surjective linear map has dimension at most that of that source.
basis_fintype_of_finite_spans: the existence of a finite spanning set implies that any basis is finite.
infinite_basis_le_maximal_linear_independent: if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

For modules over rings satisfying the rank condition

basis.le_span: the cardinality of a basis is bounded by the cardinality of any spanning set

For modules over rings satisfying the strong rank condition

linear_independent_le_span: For any linearly independent family v : ι → M and any finite spanning set w : set M, the cardinality of ι is bounded by the cardinality of w.
linear_independent_le_basis: If b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

For modules over rings with invariant basis number (including all commutative rings and all noetherian rings)

mk_eq_mk_of_basis: the dimension theorem, any two bases of the same vector space have the same cardinality.

For vector spaces (i.e. modules over a field), we have

rank_quotient_add_rank: if V₁ is a submodule of V, then module.rank (V/V₁) + module.rank V₁ = module.rank V.
rank_range_add_rank_ker: the rank-nullity theorem.

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

@[protected, irreducible]

noncomputable def module.rank (K : Type u) (V : Type v) [semiring K] [add_comm_monoid V] [module K V] :

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.

The definition is marked as protected to avoid conflicts with _root_.rank, the rank of a linear map.

Equations

module.rank K V = ⨆ (ι : {s // linear_independent K coe}), cardinal.mk ↥(ι.val)

theorem linear_map.lift_rank_le_of_injective {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M' : Type v'} [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') (i : function.injective ⇑f) :

(module.rank R M).lift ≤ (module.rank R M').lift

theorem linear_map.rank_le_of_injective {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group M₁] [module R M₁] (f : M →ₗ[R] M₁) (i : function.injective ⇑f) :

module.rank R M ≤ module.rank R M₁

theorem rank_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {n : ℕ} (H : ∀ (s : finset M), linear_independent R (λ (i : ↥s), ↑i) → s.card ≤ n) :

module.rank R M ≤ ↑n

theorem lift_rank_range_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M' : Type v'} [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') :

(module.rank R ↥(linear_map.range f)).lift ≤ (module.rank R M).lift

theorem rank_range_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group M₁] [module R M₁] (f : M →ₗ[R] M₁) :

module.rank R ↥(linear_map.range f) ≤ module.rank R M

theorem lift_rank_map_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M' : Type v'} [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') (p : submodule R M) :

(module.rank R ↥(submodule.map f p)).lift ≤ (module.rank R ↥p).lift

theorem rank_map_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group 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} [ring R] {M : Type v} [add_comm_group M] [module R M] (s t : submodule R M) (h : s ≤ t) :

module.rank R ↥s ≤ module.rank R ↥t

theorem linear_equiv.lift_rank_eq {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M' : Type v'} [add_comm_group M'] [module R M'] (f : M ≃ₗ[R] M') :

(module.rank R M).lift = (module.rank R M').lift

Two linearly equivalent vector spaces have the same dimension, a version with different universes.

theorem linear_equiv.rank_eq {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group 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 rank_eq_of_injective {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group M₁] [module R M₁] (f : M →ₗ[R] M₁) (h : function.injective ⇑f) :

module.rank R M = module.rank R ↥(linear_map.range f)

theorem linear_equiv.rank_map_eq {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group 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 linear_equiv have the same dimension.

@[simp]

theorem rank_top (R : Type u) [ring R] (M : Type v) [add_comm_group M] [module R M] :

module.rank R ↥⊤ = module.rank R M

theorem rank_range_of_surjective {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M' : Type v'} [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') (h : function.surjective ⇑f) :

module.rank R ↥(linear_map.range f) = module.rank R M'

theorem rank_submodule_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] (s : submodule R M) :

module.rank R ↥s ≤ module.rank R M

theorem linear_map.rank_le_of_surjective {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] {M₁ : Type v} [add_comm_group M₁] [module R M₁] (f : M →ₗ[R] M₁) (h : function.surjective ⇑f) :

module.rank R M₁ ≤ module.rank R M

theorem rank_quotient_le {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] (p : submodule R M) :

module.rank R (M ⧸ p) ≤ module.rank R M

theorem cardinal_lift_le_rank_of_linear_independent {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {ι : Type w} {v : ι → M} (hv : linear_independent R v) :

(cardinal.mk ι).lift ≤ (module.rank R M).lift

theorem cardinal_lift_le_rank_of_linear_independent' {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {ι : Type w} {v : ι → M} (hv : linear_independent R v) :

(cardinal.mk ι).lift ≤ (module.rank R M).lift

theorem cardinal_le_rank_of_linear_independent {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {ι : Type v} {v : ι → M} (hv : linear_independent R v) :

cardinal.mk ι ≤ module.rank R M

theorem cardinal_le_rank_of_linear_independent' {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {s : set M} (hs : linear_independent R (λ (x : ↥s), ↑x)) :

cardinal.mk ↥s ≤ module.rank R M

@[simp]

theorem rank_punit (R : Type u) [ring R] [nontrivial R] :

module.rank R punit = 0

@[simp]

theorem rank_bot (R : Type u) [ring R] (M : Type v) [add_comm_group M] [module R M] [nontrivial R] :

module.rank R ↥⊥ = 0

theorem exists_mem_ne_zero_of_rank_pos {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {s : submodule R M} (h : 0 < module.rank R ↥s) :

∃ (b : M), b ∈ s ∧ b ≠ 0

theorem linear_independent.finite_of_is_noetherian {ι : Type w} {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] [is_noetherian R M] {v : ι → M} (hv : linear_independent R v) :

A linearly-independent family of vectors in a module over a non-trivial ring must be finite if the module is Noetherian.

theorem linear_independent.set_finite_of_is_noetherian {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] [is_noetherian R M] {s : set M} (hi : linear_independent R coe) :

noncomputable def basis_fintype_of_finite_spans {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] (w : set M) [fintype ↥w] (s : submodule.span R w = ⊤) {ι : Type w} (b : basis ι R M) :

Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.

Equations

basis_fintype_of_finite_spans w s b = fintype_of_not_infinite _

theorem union_support_maximal_linear_independent_eq_range_basis {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {ι : Type w} (b : basis ι R M) {κ : Type w'} (v : κ → M) (i : linear_independent R v) (m : i.maximal) :

(⋃ (k : κ), ↑((⇑(b.repr) (v k)).support)) = set.univ

Over any ring R, if b is a basis for a module M, and s is a maximal linearly independent set, then the union of the supports of x ∈ s (when written out in the basis b) is all of b.

theorem infinite_basis_le_maximal_linear_independent' {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {ι : Type w} (b : basis ι R M) [infinite ι] {κ : Type w'} (v : κ → M) (i : linear_independent R v) (m : i.maximal) :

(cardinal.mk ι).lift ≤ (cardinal.mk κ).lift

Over any ring R, if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

theorem infinite_basis_le_maximal_linear_independent {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] {ι : Type w} (b : basis ι R M) [infinite ι] {κ : Type w} (v : κ → M) (i : linear_independent R v) (m : i.maximal) :

cardinal.mk ι ≤ cardinal.mk κ

Over any ring R, if b is an infinite basis for a module M, and s is a maximal linearly independent set, then the cardinality of b is bounded by the cardinality of s.

theorem complete_lattice.independent.subtype_ne_bot_le_rank {ι : Type w} {R : Type u} [ring R] {M : Type v} [add_comm_group M] [module R M] [nontrivial R] [no_zero_smul_divisors R M] {V : ι → submodule R M} (hV : complete_lattice.independent V) :

(cardinal.mk {i // V i ≠ ⊥}).lift ≤ (module.rank R M).lift

@[simp]

theorem rank_subsingleton {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [subsingleton R] :

module.rank R M = 1

theorem rank_pos {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [nontrivial M] :

0 < module.rank R M

theorem rank_zero_iff_forall_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [nontrivial R] :

module.rank R M = 0 ↔ ∀ (x : M), x = 0

theorem rank_zero_iff {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [nontrivial R] :

module.rank R M = 0 ↔ subsingleton M

See rank_subsingleton for the reason that nontrivial R is needed.

theorem rank_pos_iff_exists_ne_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [nontrivial R] :

0 < module.rank R M ↔ ∃ (x : M), x ≠ 0

theorem rank_pos_iff_nontrivial {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [nontrivial R] :

0 < module.rank R M ↔ nontrivial M

theorem mk_eq_mk_of_basis {ι : Type w} {ι' : Type w'} {R : Type u} [ring R] [invariant_basis_number R] {M : Type v} [add_comm_group M] [module R M] (v : basis ι R M) (v' : basis ι' R M) :

(cardinal.mk ι).lift = (cardinal.mk ι').lift

The dimension theorem: if v and v' are two bases, their index types have the same cardinalities.

noncomputable def basis.index_equiv {ι : Type w} {ι' : Type w'} {R : Type u} [ring R] [invariant_basis_number R] {M : Type v} [add_comm_group M] [module R M] (v : basis ι R M) (v' : basis ι' R M) :

ι ≃ ι'

Given two bases indexed by ι and ι' of an R-module, where R satisfies the invariant basis number property, an equiv ι ≃ ι'.

Equations

v.index_equiv v' = _.some

theorem mk_eq_mk_of_basis' {ι : Type w} {R : Type u} [ring R] [invariant_basis_number R] {M : Type v} [add_comm_group M] [module R M] {ι' : Type w} (v : basis ι R M) (v' : basis ι' R M) :

cardinal.mk ι = cardinal.mk ι'

theorem basis.le_span'' {R : Type u} [ring R] [rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (b : basis ι R M) {w : set M} [fintype ↥w] (s : submodule.span R w = ⊤) :

fintype.card ι ≤ fintype.card ↥w

An auxiliary lemma for basis.le_span.

If R satisfies the rank condition, then for any finite basis b : basis ι R M, and any finite spanning set w : set M, the cardinality of ι is bounded by the cardinality of w.

theorem basis_le_span' {R : Type u} [ring R] [rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) {w : set M} [fintype ↥w] (s : submodule.span R w = ⊤) :

cardinal.mk ι ≤ ↑(fintype.card ↥w)

Another auxiliary lemma for basis.le_span, which does not require assuming the basis is finite, but still assumes we have a finite spanning set.

theorem basis.le_span {ι : Type w} {R : Type u} [ring R] [rank_condition R] {M : Type v} [add_comm_group M] [module R M] {J : set M} (v : basis ι R M) (hJ : submodule.span R J = ⊤) :

cardinal.mk ↥(set.range ⇑v) ≤ cardinal.mk ↥J

If R satisfies the rank condition, then the cardinality of any basis is bounded by the cardinality of any spanning set.

theorem linear_independent_le_span_aux' {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (v : ι → M) (i : linear_independent R v) (w : set M) [fintype ↥w] (s : set.range v ≤ ↑(submodule.span R w)) :

fintype.card ι ≤ fintype.card ↥w

noncomputable def linear_independent_fintype_of_le_span_fintype {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (v : ι → M) (i : linear_independent R v) (w : set M) [fintype ↥w] (s : set.range v ≤ ↑(submodule.span R w)) :

If R satisfies the strong rank condition, then any linearly independent family v : ι → M contained in the span of some finite w : set M, is itself finite.

Equations

linear_independent_fintype_of_le_span_fintype v i w s = fintype_of_finset_card_le (fintype.card ↥w) _

theorem linear_independent_le_span' {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (v : ι → M) (i : linear_independent R v) (w : set M) [fintype ↥w] (s : set.range v ≤ ↑(submodule.span R w)) :

cardinal.mk ι ≤ ↑(fintype.card ↥w)

If R satisfies the strong rank condition, then for any linearly independent family v : ι → M contained in the span of some finite w : set M, the cardinality of ι is bounded by the cardinality of w.

theorem linear_independent_le_span {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (v : ι → M) (i : linear_independent R v) (w : set M) [fintype ↥w] (s : submodule.span R w = ⊤) :

cardinal.mk ι ≤ ↑(fintype.card ↥w)

If R satisfies the strong rank condition, then for any linearly independent family v : ι → M and any finite spanning set w : set M, the cardinality of ι is bounded by the cardinality of w.

theorem linear_independent_le_span_finset {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (v : ι → M) (i : linear_independent R v) (w : finset M) (s : submodule.span R ↑w = ⊤) :

cardinal.mk ι ≤ ↑(w.card)

A version of linear_independent_le_span for finset.

theorem linear_independent_le_infinite_basis {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) [infinite ι] {κ : Type u_1} (v : κ → M) (i : linear_independent R v) :

cardinal.mk κ ≤ cardinal.mk ι

An auxiliary lemma for linear_independent_le_basis: we handle the case where the basis b is infinite.

theorem linear_independent_le_basis {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) {κ : Type u_1} (v : κ → M) (i : linear_independent R v) :

cardinal.mk κ ≤ cardinal.mk ι

Over any ring R satisfying the strong rank condition, if b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

theorem basis.card_le_card_of_linear_independent_aux {R : Type u_1} [ring R] [strong_rank_condition R] (n : ℕ) {m : ℕ} (v : fin m → fin n → R) :

linear_independent R v → m ≤ n

In an n-dimensional space, the rank is at most m.

theorem maximal_linear_independent_eq_infinite_basis {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) [infinite ι] {κ : Type u_1} (v : κ → M) (i : linear_independent R v) (m : i.maximal) :

cardinal.mk κ = cardinal.mk ι

Over any ring R satisfying the strong rank condition, if b is an infinite basis for a module M, then every maximal linearly independent set has the same cardinality as b.

This proof (along with some of the lemmas above) comes from Les familles libres maximales d'un module ont-elles le meme cardinal?

theorem basis.mk_eq_rank'' {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type v} (v : basis ι R M) :

cardinal.mk ι = module.rank R M

theorem basis.mk_range_eq_rank {ι : Type w} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] (v : basis ι R M) :

cardinal.mk ↥(set.range ⇑v) = module.rank R M

theorem rank_eq_card_basis {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [fintype ι] (h : basis ι R M) :

module.rank R M = ↑(fintype.card ι)

If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the cardinality of the basis.

theorem basis.card_le_card_of_linear_independent {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (b : basis ι R M) {ι' : Type u_2} [fintype ι'] {v : ι' → M} (hv : linear_independent R v) :

fintype.card ι' ≤ fintype.card ι

theorem basis.card_le_card_of_submodule {ι : Type w} {ι' : Type w'} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] (N : submodule R M) [fintype ι] (b : basis ι R M) [fintype ι'] (b' : basis ι' R ↥N) :

fintype.card ι' ≤ fintype.card ι

theorem basis.card_le_card_of_le {ι : Type w} {ι' : Type w'} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {N O : submodule R M} (hNO : N ≤ O) [fintype ι] (b : basis ι R ↥O) [fintype ι'] (b' : basis ι' R ↥N) :

fintype.card ι' ≤ fintype.card ι

theorem basis.mk_eq_rank {ι : Type w} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] (v : basis ι R M) :

(cardinal.mk ι).lift = (module.rank R M).lift

theorem basis.mk_eq_rank' {ι : Type w} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] (v : basis ι R M) :

(cardinal.mk ι).lift = (module.rank R M).lift

theorem basis.nonempty_fintype_index_of_rank_lt_aleph_0 {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) (h : module.rank R M < cardinal.aleph_0) :

nonempty (fintype ι)

If a module has a finite dimension, all bases are indexed by a finite type.

noncomputable def basis.fintype_index_of_rank_lt_aleph_0 {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) (h : module.rank R M < cardinal.aleph_0) :

If a module has a finite dimension, all bases are indexed by a finite type.

Equations

b.fintype_index_of_rank_lt_aleph_0 h = classical.choice _

theorem basis.finite_index_of_rank_lt_aleph_0 {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {ι : Type u_1} {s : set ι} (b : basis ↥s R M) (h : module.rank R M < cardinal.aleph_0) :

If a module has a finite dimension, all bases are indexed by a finite set.

theorem rank_span {ι : Type w} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {v : ι → M} (hv : linear_independent R v) :

module.rank R ↥(submodule.span R (set.range v)) = cardinal.mk ↥(set.range v)

theorem rank_span_set {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] {s : set M} (hs : linear_independent R (λ (x : ↥s), ↑x)) :

module.rank R ↥(submodule.span R s) = cardinal.mk ↥s

def submodule.induction_on_rank {ι : Type w} {R : Type u} [ring R] [strong_rank_condition R] {M : Type v} [add_comm_group M] [module R M] [is_domain R] [fintype ι] (b : basis ι R M) (P : submodule R M → Sort u_1) (ih : Π (N : submodule R M), (Π (N' : submodule R M), N' ≤ N → Π (x : M), x ∈ N → (∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0) → P N') → P N) (N : submodule R M) :

P N

If N is a submodule in a free, finitely generated module, do induction on adjoining a linear independent element to a submodule.

Equations

submodule.induction_on_rank b P ih N = submodule.induction_on_rank_aux b P ih (fintype.card ι) N _

theorem ideal.rank_eq {R : Type u_1} {S : Type u_2} [comm_ring R] [strong_rank_condition R] [ring S] [is_domain S] [algebra R S] {n : Type u_3} {m : Type u_4} [fintype n] [fintype m] (b : basis n R S) {I : ideal S} (hI : I ≠ ⊥) (c : basis m R ↥I) :

fintype.card m = fintype.card n

If S a finite-dimensional ring extension of R which is free as an R-module, then the rank of an ideal I of S over R is the same as the rank of S.

@[simp]

theorem rank_self (R : Type u) [ring R] [strong_rank_condition R] :

module.rank R R = 1

theorem module.free.rank_eq_card_choose_basis_index (K : Type u) (V : Type v) [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] :

module.rank K V = cardinal.mk (module.free.choose_basis_index K V)

The rank of a free module M over R is the cardinality of choose_basis_index R M.

theorem nonempty_linear_equiv_of_lift_rank_eq {K : Type u} {V : Type v} {V' : Type v'} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V'] [module K V'] [module.free K V'] (cond : (module.rank K V).lift = (module.rank K V').lift) :

nonempty (V ≃ₗ[K] V')

Two vector spaces are isomorphic if they have the same dimension.

theorem nonempty_linear_equiv_of_rank_eq {K : Type u} {V V₁ : Type v} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V₁] [module K V₁] [module.free K V₁] (cond : module.rank K V = module.rank K V₁) :

nonempty (V ≃ₗ[K] V₁)

Two vector spaces are isomorphic if they have the same dimension.

noncomputable def linear_equiv.of_lift_rank_eq {K : Type u} (V : Type v) (V' : Type v') [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V'] [module K V'] [module.free K V'] (cond : (module.rank K V).lift = (module.rank K V').lift) :

Two vector spaces are isomorphic if they have the same dimension.

Equations

linear_equiv.of_lift_rank_eq V V' cond = classical.choice _

noncomputable def linear_equiv.of_rank_eq {K : Type u} (V V₁ : Type v) [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V₁] [module K V₁] [module.free K V₁] (cond : module.rank K V = module.rank K V₁) :

V ≃ₗ[K] V₁

Two vector spaces are isomorphic if they have the same dimension.

Equations

linear_equiv.of_rank_eq V V₁ cond = classical.choice _

theorem linear_equiv.nonempty_equiv_iff_lift_rank_eq {K : Type u} {V : Type v} {V' : Type v'} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V'] [module K V'] [module.free K V'] :

nonempty (V ≃ₗ[K] V') ↔ (module.rank K V).lift = (module.rank K V').lift

Two vector spaces are isomorphic if and only if they have the same dimension.

theorem linear_equiv.nonempty_equiv_iff_rank_eq {K : Type u} {V V₁ : Type v} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V₁] [module K V₁] [module.free K V₁] :

nonempty (V ≃ₗ[K] V₁) ↔ module.rank K V = module.rank K V₁

Two vector spaces are isomorphic if and only if they have the same dimension.

@[simp]

theorem rank_prod {K : Type u} {V : Type v} {V' : Type v'} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V'] [module K V'] [module.free K V'] :

module.rank K (V × V') = (module.rank K V).lift + (module.rank K V').lift

The rank of M × N is (module.rank R M).lift + (module.rank R N).lift.

theorem rank_prod' {K : Type u} {V V₁ : Type v} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [add_comm_group V₁] [module K V₁] [module.free K V₁] :

module.rank K (V × V₁) = module.rank K V + module.rank K V₁

If M and N lie in the same universe, the rank of M × N is (module.rank R M) + (module.rank R N).

@[simp]

theorem rank_pi {K : Type u} {η : Type u₁'} {φ : η → Type u_1} [ring K] [strong_rank_condition K] [Π (i : η), add_comm_group (φ i)] [Π (i : η), module K (φ i)] [∀ (i : η), module.free K (φ i)] [finite η] :

module.rank K (Π (i : η), φ i) = cardinal.sum (λ (i : η), module.rank K (φ i))

The rank of a finite product is the sum of the ranks.

theorem rank_fun {K : Type u} [ring K] [strong_rank_condition K] {V η : Type u} [fintype η] [add_comm_group V] [module K V] [module.free K V] :

module.rank K (η → V) = ↑(fintype.card η) * module.rank K V

theorem rank_fun_eq_lift_mul {K : Type u} {V : Type v} {η : Type u₁'} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] [fintype η] :

module.rank K (η → V) = ↑(fintype.card η) * (module.rank K V).lift

theorem rank_fun' {K : Type u} {η : Type u₁'} [ring K] [strong_rank_condition K] [fintype η] :

module.rank K (η → K) = ↑(fintype.card η)

theorem rank_fin_fun {K : Type u} [ring K] [strong_rank_condition K] (n : ℕ) :

module.rank K (fin n → K) = ↑n

noncomputable def fin_dim_vectorspace_equiv {K : Type u} {V : Type v} [ring K] [strong_rank_condition K] [add_comm_group V] [module K V] [module.free K V] (n : ℕ) (hn : module.rank K V = ↑n) :

V ≃ₗ[K] fin n → K

An n-dimensional K-vector space is equivalent to fin n → K.

Equations

fin_dim_vectorspace_equiv n hn = classical.choice _

theorem basis.finite_of_vector_space_index_of_rank_lt_aleph_0 {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (h : module.rank K V < cardinal.aleph_0) :

(basis.of_vector_space_index K V).finite

If a vector space has a finite dimension, the index set of basis.of_vector_space is finite.

theorem rank_span_le {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (s : set V) :

module.rank K ↥(submodule.span K s) ≤ cardinal.mk ↥s

theorem rank_span_of_finset {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (s : finset V) :

module.rank K ↥(submodule.span K ↑s) < cardinal.aleph_0

theorem rank_quotient_add_rank {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (p : submodule K V) :

module.rank K (V ⧸ p) + module.rank K ↥p = module.rank K V

theorem rank_range_add_rank_ker {K : Type u} {V V₁ : Type v} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁] (f : V →ₗ[K] V₁) :

module.rank K ↥(linear_map.range f) + module.rank K ↥(linear_map.ker f) = module.rank K V

rank-nullity theorem

theorem rank_eq_of_surjective {K : Type u} {V V₁ : Type v} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁] (f : V →ₗ[K] V₁) (h : function.surjective ⇑f) :

module.rank K V = module.rank K V₁ + module.rank K ↥(linear_map.ker f)

theorem rank_add_rank_split {K : Type u} {V V₁ V₂ V₃ : Type v} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module K V₂] [add_comm_group V₃] [module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂) (ce : V₁ →ₗ[K] V₃) (hde : ⊤ ≤ linear_map.range db ⊔ linear_map.range eb) (hgd : linear_map.ker cd = ⊥) (eq : db.comp cd = eb.comp ce) (eq₂ : ∀ (d : V₂) (e : V₃), ⇑db d = ⇑eb e → (∃ (c : V₁), ⇑cd c = d ∧ ⇑ce c = e)) :

module.rank K V + module.rank K V₁ = module.rank K V₂ + module.rank K V₃

This is mostly an auxiliary lemma for submodule.rank_sup_add_rank_inf_eq.

theorem submodule.rank_sup_add_rank_inf_eq {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (s t : submodule K V) :

module.rank K ↥(s ⊔ t) + module.rank K ↥(s ⊓ t) = module.rank K ↥s + module.rank K ↥t

theorem submodule.rank_add_le_rank_add_rank {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (s t : submodule K V) :

module.rank K ↥(s ⊔ t) ≤ module.rank K ↥s + module.rank K ↥t

noncomputable def basis.of_rank_eq_zero {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [is_empty ι] (hV : module.rank K V = 0) :

basis ι K V

The ι indexed basis on V, where ι is an empty type and V is zero-dimensional.

See also finite_dimensional.fin_basis.

Equations

basis.of_rank_eq_zero hV = basis.empty V

@[simp]

theorem basis.of_rank_eq_zero_apply {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [is_empty ι] (hV : module.rank K V = 0) (i : ι) :

⇑(basis.of_rank_eq_zero hV) i = 0

theorem le_rank_iff_exists_linear_independent {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {c : cardinal} :

c ≤ module.rank K V ↔ ∃ (s : set V), cardinal.mk ↥s = c ∧ linear_independent K coe

theorem le_rank_iff_exists_linear_independent_finset {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {n : ℕ} :

↑n ≤ module.rank K V ↔ ∃ (s : finset V), s.card = n ∧ linear_independent K coe

theorem rank_le_one_iff {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] :

module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

A vector space has dimension at most 1 if and only if there is a single vector of which all vectors are multiples.

theorem rank_submodule_le_one_iff {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (s : submodule K V) :

module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V) (H : v₀ ∈ s), s ≤ submodule.span K {v₀}

A submodule has dimension at most 1 if and only if there is a single vector in the submodule such that the submodule is contained in its span.

theorem rank_submodule_le_one_iff' {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (s : submodule K V) :

module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ submodule.span K {v₀}

A submodule has dimension at most 1 if and only if there is a single vector, not necessarily in the submodule, such that the submodule is contained in its span.

theorem submodule.rank_le_one_iff_is_principal {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (W : submodule K V) :

module.rank K ↥W ≤ 1 ↔ W.is_principal

theorem module.rank_le_one_iff_top_is_principal {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] :

module.rank K V ≤ 1 ↔ ⊤.is_principal

The rank of a linear map #

noncomputable def linear_map.rank {K : Type u} {V : Type v} {V' : Type v'} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] (f : V →ₗ[K] V') :

rank f is the rank of a linear_map f, defined as the dimension of f.range.

Equations

f.rank = module.rank K ↥(linear_map.range f)

theorem linear_map.rank_le_range {K : Type u} {V : Type v} {V' : Type v'} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] (f : V →ₗ[K] V') :

f.rank ≤ module.rank K V'

theorem linear_map.rank_le_domain {K : Type u} {V V₁ : Type v} [ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁] (f : V →ₗ[K] V₁) :

f.rank ≤ module.rank K V

@[simp]

theorem linear_map.rank_zero {K : Type u} {V : Type v} {V' : Type v'} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] [nontrivial K] :

0.rank = 0

theorem linear_map.rank_comp_le_left {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] [add_comm_group V''] [module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :

(f.comp g).rank ≤ f.rank

theorem linear_map.lift_rank_comp_le_right {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] [add_comm_group V''] [module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :

(f.comp g).rank.lift ≤ g.rank.lift

theorem linear_map.lift_rank_comp_le {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] [add_comm_group V''] [module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :

(f.comp g).rank.lift ≤ linear_order.min f.rank.lift g.rank.lift

The rank of the composition of two maps is less than the minimum of their ranks.

theorem linear_map.rank_comp_le_right {K : Type u} {V : Type v} {V' V'₁ : Type v'} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] [add_comm_group V'₁] [module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :

(f.comp g).rank ≤ g.rank

theorem linear_map.rank_comp_le {K : Type u} {V : Type v} {V' V'₁ : Type v'} [ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] [add_comm_group V'₁] [module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :

(f.comp g).rank ≤ linear_order.min f.rank g.rank

The rank of the composition of two maps is less than the minimum of their ranks.

See lift_rank_comp_le for the universe-polymorphic version.

theorem linear_map.rank_add_le {K : Type u} {V : Type v} {V' : Type v'} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] (f g : V →ₗ[K] V') :

(f + g).rank ≤ f.rank + g.rank

theorem linear_map.rank_finset_sum_le {K : Type u} {V : Type v} {V' : Type v'} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] {η : Type u_1} (s : finset η) (f : η → (V →ₗ[K] V')) :

(s.sum (λ (d : η), f d)).rank ≤ s.sum (λ (d : η), (f d).rank)

theorem linear_map.le_rank_iff_exists_linear_independent {K : Type u} {V : Type v} {V' : Type v'} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] {c : cardinal} {f : V →ₗ[K] V'} :

c ≤ f.rank ↔ ∃ (s : set V), (cardinal.mk ↥s).lift = c.lift ∧ linear_independent K (λ (x : ↥s), ⇑f ↑x)

theorem linear_map.le_rank_iff_exists_linear_independent_finset {K : Type u} {V : Type v} {V' : Type v'} [division_ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V'] {n : ℕ} {f : V →ₗ[K] V'} :

↑n ≤ f.rank ↔ ∃ (s : finset V), s.card = n ∧ linear_independent K (λ (x : ↥↑s), ⇑f ↑x)