Commit 2021-08-20 14:42 7265a4ee
View on Github →feat(linear_algebra/dimension): generalize inequalities and invariance of dimension to arbitrary rings (#8343) We implement some of the results of Les familles libres maximales d'un module ont-elles le meme cardinal?. We also generalize many theorems which were previously proved only for vector spaces, but are true for modules over arbitrary rings or rings satisfying the (strong) rank condition or have invariant basis number. (These typically need entire new proofs, as the original proofs e.g. used rank-nullity.) The main new results are:
basis_fintype_of_finite_spans
: Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.union_support_maximal_linear_independent_eq_range_basis
: Over any ringR
, ifb
is a basis for a moduleM
, ands
is a maximal linearly independent set, then the union of the supports ofx ∈ s
(when written out in the basisb
) is all ofb
.infinite_basis_le_maximal_linear_independent
: Over any ringR
, ifb
is an infinite basis for a moduleM
, ands
is a maximal linearly independent set, then the cardinality ofb
is bounded by the cardinality ofs
.mk_eq_mk_of_basis
: We generalize the invariance of dimension theorem to any ring with the invariant basis number property.basis.le_span
: We generalize this statement (the size of a basis is bounded by the size of any spanning set) to any ring satisfying the rank condition.linear_independent_le_span
: IfR
satisfies the strong rank condition, then for any linearly independent familyv : ι → M
and any finite spanning setw : set M
, the cardinality ofι
is bounded by the cardinality ofw
.linear_independent_le_basis
: Over any ringR
satisfying the strong rank condition, ifb
is a basis for a moduleM
, ands
is a linearly independent set, then the cardinality ofs
is bounded by the cardinality ofb
.
There is a naming discrepancy: most of the theorem names refer to dim
,
even though the definition is of module.rank
.
This reflects that module.rank
was originally called dim
, and only defined for vector spaces.
I would prefer to address this in a separate PR (note this discrepancy wasn't introduced in this PR).