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 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.
  • infinite_basis_le_maximal_linear_independent: 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.
  • 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: If R satisfies the strong rank condition, then for any linearly independent family v : ι → M and any finite spanning set w : set M, the cardinality of ι is bounded by the cardinality of w.
  • linear_independent_le_basis: Over any ring R satisfying the strong rank condition, if b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

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

Estimated changes

added theorem basis.le_span''
modified theorem basis.le_span
modified theorem basis.mk_eq_dim''
modified theorem basis.mk_eq_dim
modified theorem basis.mk_range_eq_dim
added theorem basis_le_span'
modified theorem dim_bot
modified theorem dim_eq_of_injective
deleted theorem dim_le_of_injective
modified theorem dim_le_of_submodule
deleted theorem dim_le_of_surjective
modified theorem dim_map_le
deleted theorem dim_of_field
added theorem dim_of_ring
added theorem dim_punit
modified theorem dim_range_le
modified theorem dim_range_of_surjective
modified theorem dim_span
modified theorem dim_span_set
modified theorem dim_submodule_le
modified theorem dim_top
modified theorem linear_equiv.dim_eq
deleted theorem linear_equiv.dim_eq_lift
modified theorem linear_equiv.lift_dim_eq
deleted theorem linear_independent_le_dim
modified theorem mk_eq_mk_of_basis'
modified theorem mk_eq_mk_of_basis
modified theorem {m}
deleted theorem {u₁}