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 #

The commRing_strongRankCondition comes from CommRing.orzechProperty, proved in Mathlib/RingTheory/FiniteType.lean, which states that any commutative ring satisfies the OrzechProperty, that is, for any finitely generated R-module M, any surjective homomorphism f : N → M from a submodule N of M to M is injective.

References #

@[instance 100]

Any nontrivial commutative ring satisfies the StrongRankCondition.

Equations
  • =