Conditions for rank to be finite #

Also contains characterization for when rank equals zero or rank equals one.

theorem rank_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (H : ∀ (s : Finset M), (LinearIndependent R fun (i : { x : M // x ∈ s }) => ↑i) → s.card ≤ n) :

Module.rank R M ≤ ↑n

source

theorem rank_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :

Module.rank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0

See rank_zero_iff for a stronger version with NoZeroSMulDivisor R M.

source

theorem rank_zero_iff_forall_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :

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

source

theorem rank_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :

Module.rank R M = 0 ↔ Subsingleton M

See rank_subsingleton for the reason that Nontrivial R is needed. Also see rank_eq_zero_iff for the version without NoZeroSMulDivisor R M.

source

theorem rank_pos_iff_exists_ne_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :

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

source

theorem rank_pos_iff_nontrivial {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :

0 < Module.rank R M ↔ Nontrivial M

source

theorem rank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] [Nontrivial M] :

0 < Module.rank R M

source

theorem rank_eq_zero_iff_isTorsion {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] :

Module.rank R M = 0 ↔ Module.IsTorsion R M

source

theorem rank_subsingleton' (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [Subsingleton M] :

Module.rank R M = 0

See rank_subsingleton that assumes Subsingleton R instead.

source

@[simp]

theorem rank_punit (R : Type u) [Ring R] [Nontrivial R] :

Module.rank R PUnit.{u_1 + 1} = 0

source

@[simp]

theorem rank_bot (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] :

Module.rank R ↥⊥ = 0

source

theorem exists_mem_ne_zero_of_rank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {s : Submodule R M} (h : 0 < Module.rank R ↥s) :

∃ b ∈ s, b ≠ 0

source

theorem Module.finite_of_rank_eq_nat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] {n : ℕ} (h : Module.rank R M = ↑n) :

Module.Finite R M

source

theorem Module.finite_of_rank_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (h : Module.rank R M = 0) :

Module.Finite R M

source

theorem Module.finite_of_rank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : Module.rank R M = 1) :

Module.Finite R M

source

theorem Basis.nonempty_fintype_index_of_rank_lt_aleph0 {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (b : Basis ι R M) (h : Module.rank R M < Cardinal.aleph0) :

Nonempty (Fintype ι)

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

source

noncomputable def Basis.fintypeIndexOfRankLtAleph0 {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (b : Basis ι R M) (h : Module.rank R M < Cardinal.aleph0) :

Fintype ι

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

Equations

b.fintypeIndexOfRankLtAleph0 h = Classical.choice ⋯

Instances For

source

theorem Basis.finite_index_of_rank_lt_aleph0 {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} {s : Set ι} (b : Basis (↑s) R M) (h : Module.rank R M < Cardinal.aleph0) :

s.Finite

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

source

theorem LinearIndependent.cardinalMk_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type w} {b : ι → M} (h : LinearIndependent R b) :

Cardinal.mk ι ≤ ↑(Module.finrank R M)

source

@[deprecated LinearIndependent.cardinalMk_le_finrank]

theorem LinearIndependent.cardinal_mk_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type w} {b : ι → M} (h : LinearIndependent R b) :

Cardinal.mk ι ≤ ↑(Module.finrank R M)

Alias of LinearIndependent.cardinalMk_le_finrank.

source

theorem LinearIndependent.fintype_card_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type u_1} [Fintype ι] {b : ι → M} (h : LinearIndependent R b) :

Fintype.card ι ≤ Module.finrank R M

source

theorem LinearIndependent.finset_card_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Finset M} (h : LinearIndependent R fun (x : { x : M // x ∈ b }) => ↑x) :

b.card ≤ Module.finrank R M

source

theorem LinearIndependent.lt_aleph0_of_finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} [Module.Finite R M] {v : ι → M} (h : LinearIndependent R v) :

Cardinal.mk ι < Cardinal.aleph0

source

theorem LinearIndependent.finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type u_1} {f : ι → M} (h : LinearIndependent R f) :

Finite ι

source

theorem LinearIndependent.setFinite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Set M} (h : LinearIndependent R fun (x : ↑b) => ↑x) :

b.Finite

source

theorem exists_set_linearIndependent_of_lt_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : Cardinal.{v}} (hn : n < Module.rank R M) :

∃ (s : Set M), Cardinal.mk ↑s = n ∧ LinearIndependent R Subtype.val

source

theorem exists_finset_linearIndependent_of_le_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : ↑n ≤ Module.rank R M) :

∃ (s : Finset M), s.card = n ∧ LinearIndependent R Subtype.val

source

theorem exists_linearIndependent_of_le_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : ↑n ≤ Module.rank R M) :

∃ (f : Fin n → M), LinearIndependent R f

source

theorem natCast_le_rank_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {n : ℕ} :

↑n ≤ Module.rank R M ↔ ∃ (f : Fin n → M), LinearIndependent R f

source

theorem natCast_le_rank_iff_finset {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {n : ℕ} :

↑n ≤ Module.rank R M ↔ ∃ (s : Finset M), s.card = n ∧ LinearIndependent R Subtype.val

source

theorem exists_finset_linearIndependent_of_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : n ≤ Module.finrank R M) :

∃ (s : Finset M), s.card = n ∧ LinearIndependent R Subtype.val

source

theorem exists_linearIndependent_of_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} (hn : n ≤ Module.finrank R M) :

∃ (f : Fin n → M), LinearIndependent R f

source

theorem Module.Finite.not_linearIndependent_of_infinite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [StrongRankCondition R] {ι : Type u_1} [Infinite ι] (v : ι → M) :

¬LinearIndependent R v

source

theorem iSupIndep.subtype_ne_bot_le_rank {R : Type u} {M : Type v} {ι : Type w} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial R] {V : ι → Submodule R M} (hV : iSupIndep V) :

Cardinal.lift.{v, w} (Cardinal.mk { i : ι // V i ≠ ⊥ }) ≤ Cardinal.lift.{w, v} (Module.rank R M)

source

@[deprecated iSupIndep.subtype_ne_bot_le_rank]

theorem CompleteLattice.Independent.subtype_ne_bot_le_rank {R : Type u} {M : Type v} {ι : Type w} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial R] {V : ι → Submodule R M} (hV : iSupIndep V) :

Cardinal.lift.{v, w} (Cardinal.mk { i : ι // V i ≠ ⊥ }) ≤ Cardinal.lift.{w, v} (Module.rank R M)

Alias of iSupIndep.subtype_ne_bot_le_rank.

source

theorem iSupIndep.subtype_ne_bot_le_finrank_aux {R : Type u} {M : Type v} {ι : Type w} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M} (hp : iSupIndep p) :

Cardinal.mk { i : ι // p i ≠ ⊥ } ≤ ↑(Module.finrank R M)

source

noncomputable def iSupIndep.fintypeNeBotOfFiniteDimensional {R : Type u} {M : Type v} {ι : Type w} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M} (hp : iSupIndep p) :

Fintype { i : ι // p i ≠ ⊥ }

If p is an independent family of submodules of a R-finite module M, then the number of nontrivial subspaces in the family p is finite.

Equations

hp.fintypeNeBotOfFiniteDimensional = ⋯.some

Instances For

source

theorem iSupIndep.subtype_ne_bot_le_finrank {R : Type u} {M : Type v} {ι : Type w} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M} (hp : iSupIndep p) [Fintype { i : ι // p i ≠ ⊥ }] :

Fintype.card { i : ι // p i ≠ ⊥ } ≤ Module.finrank R M

If p is an independent family of submodules of a R-finite module M, then the number of nontrivial subspaces in the family p is bounded above by the dimension of M.

Note that the Fintype hypothesis required here can be provided by iSupIndep.fintypeNeBotOfFiniteDimensional.

source

theorem Module.exists_nontrivial_relation_of_finrank_lt_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [StrongRankCondition R] {t : Finset M} (h : Module.finrank R M < t.card) :

∃ (f : M → R), ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

If a finset has cardinality larger than the rank of a module, then there is a nontrivial linear relation amongst its elements.

source

theorem Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [StrongRankCondition R] {t : Finset M} (h : Module.finrank R M + 1 < t.card) :

∃ (f : M → R), ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

If a finset has cardinality larger than finrank + 1, then there is a nontrivial linear relation amongst its elements, such that the coefficients of the relation sum to zero.

source

theorem Module.finrank_zero_of_subsingleton {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [Subsingleton M] :

Module.finrank R M = 0

A (finite dimensional) space that is a subsingleton has zero finrank.

source

theorem LinearIndependent.finrank_eq_zero_of_infinite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {ι : Type u_1} [Infinite ι] {v : ι → M} (hv : LinearIndependent R v) :

Module.finrank R M = 0

source

theorem Module.nontrivial_of_finrank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] (h : 0 < Module.finrank R M) :

Nontrivial M

A finite dimensional space is nontrivial if it has positive finrank.

source

theorem Module.nontrivial_of_finrank_eq_succ {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] {n : ℕ} (hn : Module.finrank R M = n.succ) :

Nontrivial M

A finite dimensional space is nontrivial if it has finrank equal to the successor of a natural number.

source

@[simp]

theorem finrank_bot (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] :

Module.finrank R ↥⊥ = 0

source

theorem Module.finrank_pos_iff_exists_ne_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] :

0 < Module.finrank R M ↔ ∃ (x : M), x ≠ 0

A finite rank torsion-free module has positive finrank iff it has a nonzero element.

source

theorem Module.finrank_pos_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] :

0 < Module.finrank R M ↔ Nontrivial M

An R-finite torsion-free module has positive finrank iff it is nontrivial.

source

theorem Module.finrank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] [h : Nontrivial M] :

0 < Module.finrank R M

A nontrivial finite dimensional space has positive finrank.

source

theorem Module.finrank_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] :

Module.finrank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0

See Module.finrank_zero_iff for the stronger version with NoZeroSMulDivisors R M.

source

theorem Module.finrank_eq_zero_iff_isTorsion {M : Type v} [AddCommGroup M] {R : Type u_1} [CommRing R] [StrongRankCondition R] [IsDomain R] [Module R M] [Module.Finite R M] :

Module.finrank R M = 0 ↔ Module.IsTorsion R M

The StrongRankCondition is automatic. See commRing_strongRankCondition.

source

theorem Module.finrank_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] :

Module.finrank R M = 0 ↔ Subsingleton M

A finite dimensional space has zero finrank iff it is a subsingleton. This is the finrank version of rank_zero_iff.

source

theorem Module.finrank_quotient_add_finrank_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) :

Module.finrank R (M ⧸ N) + Module.finrank R ↥N ≤ Module.finrank R M

Similar to rank_quotient_add_rank_le but for finrank and a finite M.

source

theorem Module.finrank_eq_zero_of_rank_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (h : Module.rank R M = 0) :

Module.finrank R M = 0

source

theorem Submodule.bot_eq_top_of_rank_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (h : Module.rank R M = 0) :

⊥ = ⊤

source

@[simp]

theorem Submodule.rank_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] {S : Submodule R M} :

Module.rank R ↥S = 0 ↔ S = ⊥

See rank_subsingleton for the reason that Nontrivial R is needed.

source

@[simp]

theorem Submodule.finrank_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [NoZeroSMulDivisors R M] {S : Submodule R M} [Module.Finite R ↥S] :

Module.finrank R ↥S = 0 ↔ S = ⊥

source

@[simp]

theorem Submodule.one_le_finrank_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [NoZeroSMulDivisors R M] {S : Submodule R M} [Module.Finite R ↥S] :

1 ≤ Module.finrank R ↥S ↔ S ≠ ⊥

source

theorem finrank_eq_zero_of_basis_imp_not_finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite) :

Module.finrank R M = 0

source

theorem finrank_eq_zero_of_basis_imp_false {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ∀ (s : Finset M), Basis (↑↑s) R M → False) :

Module.finrank R M = 0

source

theorem finrank_eq_zero_of_not_exists_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬∃ (s : Finset M), Nonempty (Basis (↑↑s) R M)) :

Module.finrank R M = 0

source

theorem finrank_eq_zero_of_not_exists_basis_finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬∃ (s : Set M) (x : Basis (↑s) R M), s.Finite) :

Module.finrank R M = 0

source

theorem finrank_eq_zero_of_not_exists_basis_finset {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬∃ (s : Finset M), Nonempty (Basis { x : M // x ∈ s } R M)) :

Module.finrank R M = 0

source

theorem rank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [StrongRankCondition R] (v : M) (n : v ≠ 0) (h : ∀ (w : M), ∃ (c : R), c • v = w) :

Module.rank R M = 1

If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

source

theorem finrank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [StrongRankCondition R] (v : M) (n : v ≠ 0) (h : ∀ (w : M), ∃ (c : R), c • v = w) :

Module.finrank R M = 1

If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

source

theorem finrank_le_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [StrongRankCondition R] (v : M) (h : ∀ (w : M), ∃ (c : R), c • v = w) :

Module.finrank R M ≤ 1

If every vector is a multiple of some v : M, then M has dimension at most one.

Documentation

Mathlib.LinearAlgebra.Dimension.Finite

Conditions for rank to be finite #