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
See rank_zero_iff for a stronger version with NoZeroSMulDivisor R M.
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
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.
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
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
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
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
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.
@[simp]
@[simp]
theorem
rank_bot
(R : Type u)
(M : Type v)
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
:
Module.rank R ↥⊥ = 0
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
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
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
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
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)
:
If a module has a finite dimension, all bases are indexed by a finite type.
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
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.
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)
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
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
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)
:
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 ι
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
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
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
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
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
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
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
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
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)
:
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 : CompleteLattice.Independent V)
:
Cardinal.lift.{v, w} (Cardinal.mk { i : ι // V i ≠ ⊥ }) ≤ Cardinal.lift.{w, v} (Module.rank R M)
theorem
CompleteLattice.Independent.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 : CompleteLattice.Independent p)
:
Cardinal.mk { i : ι // p i ≠ ⊥ } ≤ ↑(Module.finrank R M)
noncomputable def
CompleteLattice.Independent.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 : CompleteLattice.Independent p)
:
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
theorem
CompleteLattice.Independent.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 : CompleteLattice.Independent 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
CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional.
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)
:
If a finset has cardinality larger than the rank of a module, then there is a nontrivial linear relation amongst its elements.
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)
:
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.
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.
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
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)
:
A finite dimensional space is nontrivial if it has positive finrank.
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)
:
A finite dimensional space is nontrivial if it has finrank equal to the successor of a
natural number.
@[simp]
theorem
finrank_bot
(R : Type u)
(M : Type v)
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
:
Module.finrank R ↥⊥ = 0
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.
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.
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.
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]
:
See Module.finrank_zero_iff
for the stronger version with NoZeroSMulDivisors R M.
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.
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.
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.
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
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)
:
@[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.
@[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 = ⊥
@[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 ≠ ⊥
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
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
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
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
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
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.
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.
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.