# mathlibdocumentation

linear_algebra.invariant_basis_number

# Invariant basis number property #

We say that a ring R satisfies the invariant basis number property if there is a well-defined notion of the rank of a finitely generated free (left) R-module. Since a finitely generated free module with a basis consisting of n elements is linearly equivalent to fin n → R, it is sufficient that (fin n → R) ≃ₗ[R] (fin m → R) implies n = m.

It is also useful to consider two stronger conditions, namely the rank condition, that a surjective linear map (fin n → R) →ₗ[R] (fin m → R) implies m ≤ n and the strong rank condition, that an injective linear map (fin n → R) →ₗ[R] (fin m → R) implies n ≤ m.

The strong rank condition implies the rank condition, and the rank condition implies the invariant basis number property.

## Main definitions #

strong_rank_condition R is a type class stating that R satisfies the strong rank condition. rank_condition R is a type class stating that R satisfies the rank condition. invariant_basis_number R is a type class stating that R has the invariant basis number property.

## Main results #

We show that every nontrivial left-noetherian ring satisfies the strong rank condition, (and so in particular every division ring or field), and then use this to show every nontrivial commutative ring has the invariant basis number property.

More generally, every commutative ring satisfies the strong rank condition. This is proved in linear_algebra/free_module/strong_rank_condition. We keep invariant_basis_number_of_nontrivial_of_comm_ring here since it imports fewer files.

## Future work #

So far, there is no API at all for the invariant_basis_number class. There are several natural ways to formulate that a module M is finitely generated and free, for example M ≃ₗ[R] (fin n → R), M ≃ₗ[R] (ι → R), where ι is a fintype, or providing a basis indexed by a finite type. There should be lemmas applying the invariant basis number property to each situation.

The finite version of the invariant basis number property implies the infinite analogue, i.e., that (ι →₀ R) ≃ₗ[R] (ι' →₀ R) implies that cardinal.mk ι = cardinal.mk ι'. This fact (and its variants) should be formalized.

## Tags #

free module, rank, invariant basis number, IBN