Documentation

Mathlib.LinearAlgebra.Basis.Cardinality

Results relating bases and cardinality. #

theorem basis_finite_of_finite_spans {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [Nontrivial R] [Module R M] (w : Set M) (hw : w.Finite) (s : Submodule.span R w = ) {ι : Type w} (b : Basis ι R M) :

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) :

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.