Documentation

Mathlib.LinearAlgebra.FreeModule.StrongRankCondition

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 #

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.