Strong rank condition for commutative rings

We prove that any nontrivial commutative ring satisfies StrongRankCondition, meaning that if there is an injective linear map (Fin n → R) →ₗ[R] Fin m → R, then n ≤ m. This implies that any commutative ring satisfies InvariantBasisNumber: the rank of a finitely generated free module is well defined.

Main result

• commRing_strongRankCondition R : R has the StrongRankCondition.

References

We follow the proof given in https://mathoverflow.net/a/47846/7845. The argument is the following: it is enough to prove that for all n, there is no injective linear map (Fin (n + 1) → R) →ₗ[R] Fin n → R. Given such an f, we get by extension an injective linear map g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R. Injectivity implies that P, the minimal polynomial of g, has non-zero constant term a₀ ≠ 0. But evaluating 0 = P(g) at the vector (0,...,0,1) gives a₀, contradiction.

instance commRing_strongRankCondition (R : Type u_1) [CommRing R] [Nontrivial R] : StrongRankCondition R

Any commutative ring satisfies the StrongRankCondition.

Equations

• commRing_strongRankCondition = commRing_strongRankCondition.proof_1