Results relating bases and cardinality. #
theorem
basis_finite_of_finite_spans
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Nontrivial R]
[Module R M]
(w : Set M)
(hw : w.Finite)
(s : Submodule.span R w = ⊤)
{ι : Type w}
(b : Basis ι R M)
:
Finite ι
Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
theorem
union_support_maximal_linearIndependent_eq_range_basis
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Nontrivial R]
[Module R M]
{ι : Type w}
(b : Basis ι R M)
{κ : Type w'}
(v : κ → M)
(i : LinearIndependent 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_linearIndependent'
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Nontrivial R]
[Module R M]
{ι : Type w}
(b : Basis ι R M)
[Infinite ι]
{κ : Type w'}
(v : κ → M)
(i : LinearIndependent R v)
(m : i.Maximal)
:
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_linearIndependent
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Nontrivial R]
[Module R M]
{ι : Type w}
(b : Basis ι R M)
[Infinite ι]
{κ : Type w}
(v : κ → M)
(i : LinearIndependent 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.