Results relating bases and cardinality. #
theorem
finite_of_span_finite_eq_top_finsupp
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Nontrivial M]
{ι : Type u_1}
{s : Set (ι →₀ M)}
(hs : s.Finite)
(hsspan : Submodule.span R s = ⊤)
:
Finite ι
theorem
basis_finite_of_finite_spans
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Nontrivial R]
{s : Set M}
(hs : s.Finite)
(hsspan : Submodule.span R s = ⊤)
{ι : 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}
[Semiring R]
[AddCommMonoid M]
[Nontrivial R]
[Module R M]
{ι : Type w}
(b : Basis ι R M)
{κ : Type w'}
(v : κ → M)
(ind : LinearIndependent R v)
(m : ind.Maximal)
:
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}
[Semiring R]
[AddCommMonoid 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}
[Semiring R]
[AddCommMonoid 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.