mathlib3 documentation


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 #

References #

We follow the proof given in 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.

@[protected, instance]

Any commutative ring satisfies the strong_rank_condition.