Strong rank condition for commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove that any nontrivial commutative ring satisfies strong_rank_condition, 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 invariant_basis_number: the rank of a finitely generated free module is well defined.

Main result #

• comm_ring_strong_rank_condition R : R has the strong_rank_condition.

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.