Conditions for rank to be finite #
Also contains characterization for when rank equals zero or rank equals one.
theorem
linearIndependent_bounded_of_finset_linearIndependent_bounded
{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)
(s : Set M)
:
LinearIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
If every finite set of linearly independent vectors has cardinality at most n,
then the same is true for arbitrary sets of linearly independent vectors.
See rank_zero_iff for a stronger version with NoZeroSMulDivisor R M.
theorem
rank_pos_of_free
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
[Nontrivial 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]
:
theorem
rank_zero_iff
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
[NoZeroSMulDivisors R 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]
:
theorem
rank_pos_iff_nontrivial
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
[NoZeroSMulDivisors R M]
:
theorem
rank_pos
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
[NoZeroSMulDivisors R M]
[Nontrivial M]
:
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]
[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]
[Free R M]
(h : Module.rank R M = 1)
:
Module.Finite R M
theorem
Module.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
Module.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
Instances For
theorem
Module.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.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)
:
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)
:
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)
:
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 ∧ LinearIndepOn R id s
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)
:
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 : ℕ}
:
theorem
natCast_le_rank_iff_finset
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
{n : ℕ}
:
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
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)
:
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)
:
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)
:
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
Instances For
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 ≠ ⊥ }]
:
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.
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 : 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 : 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]
:
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)
:
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 < 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 : 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]
:
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]
:
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]
:
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]
:
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_zero_iff
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[StrongRankCondition R]
[Module.Finite R M]
[NoZeroSMulDivisors R 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)
:
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)
:
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}
:
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]
:
@[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]
:
@[simp]
theorem
Set.finrank_empty
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
:
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) (a : Module.Basis (↑s) R M), ¬s.Finite)
:
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) (a : Module.Basis (↑↑s) R M), False)
:
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 (Module.Basis (↑↑s) R M))
:
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 : Module.Basis (↑s) R M), s.Finite)
:
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 (Module.Basis { x : M // x ∈ s } R M))
:
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)
:
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)
:
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)
:
If every vector is a multiple of some v : M, then M has dimension at most one.
@[simp]
theorem
Module.finite_finsupp_iff
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_1}
:
@[simp]