# Invariant basis number property #

## Main definitions #

Let `R`

be a (not necessary commutative) ring.

`InvariantBasisNumber R`

is a type class stating that`(Fin n → R) ≃ₗ[R] (Fin m → R)`

implies`n = m`

, a property known as the*invariant basis number property.*This assumption implies that there is a well-defined notion of the rank of a finitely generated free (left)

`R`

-module.

It is also useful to consider the following stronger conditions:

the

*rank condition*, witnessed by the type class`RankCondition R`

, states that the existence of a surjective linear map`(Fin n → R) →ₗ[R] (Fin m → R)`

implies`m ≤ n`

the

*strong rank condition*, witnessed by the type class`StrongRankCondition R`

, states that the existence of an injective linear map`(Fin n → R) →ₗ[R] (Fin m → R)`

implies`n ≤ m`

.`OrzechProperty R`

, defined in`Mathlib/RingTheory/OrzechProperty.lean`

, states that for any finitely generated`R`

-module`M`

, any surjective homomorphism`f : N → M`

from a submodule`N`

of`M`

to`M`

is injective.

## Instances #

`IsNoetherianRing.orzechProperty`

(defined in`Mathlib/RingTheory/Noetherian.lean`

) : any left-noetherian ring satisfies the Orzech property. This applies in particular to division rings.`strongRankCondition_of_orzechProperty`

: the Orzech property implies the strong rank condition (for non trivial rings).`IsNoetherianRing.strongRankCondition`

: every nontrivial left-noetherian ring satisfies the strong rank condition (and so in particular every division ring or field).`rankCondition_of_strongRankCondition`

: the strong rank condition implies the rank condition.`invariantBasisNumber_of_rankCondition`

: the rank condition implies the invariant basis number property.`invariantBasisNumber_of_nontrivial_of_commRing`

: a nontrivial commutative ring satisfies the invariant basis number property.

More generally, every commutative ring satisfies the Orzech property,
hence the strong rank condition, which is proved in `Mathlib/RingTheory/FiniteType.lean`

.
We keep `invariantBasisNumber_of_nontrivial_of_commRing`

here since it imports fewer files.

## Counterexamples to converse results #

The following examples can be found in the book of Lam [Lam99] (see also https://math.stackexchange.com/questions/4711904):

- Let
`k`

be a field, then the free (non-commutative) algebra`k⟨x, y⟩`

satisfies the rank condition but not the strong rank condition. - The free (non-commutative) algebra
`ℚ⟨a, b, c, d⟩`

quotient by the two-sided ideal`(ac − 1, bd − 1, ab, cd)`

satisfies the invariant basis number property but not the rank condition.

## Future work #

So far, there is no API at all for the `InvariantBasisNumber`

class. There are several natural
ways to formulate that a module `M`

is finitely generated and free, for example
`M ≃ₗ[R] (Fin n → R)`

, `M ≃ₗ[R] (ι → R)`

, where `ι`

is a fintype, or providing a basis indexed by
a finite type. There should be lemmas applying the invariant basis number property to each
situation.

The finite version of the invariant basis number property implies the infinite analogue, i.e., that
`(ι →₀ R) ≃ₗ[R] (ι' →₀ R)`

implies that `Cardinal.mk ι = Cardinal.mk ι'`

. This fact (and its
variants) should be formalized.

## References #

- https://en.wikipedia.org/wiki/Invariant_basis_number
- https://mathoverflow.net/a/2574/
- Lam, T. Y.
*Lectures on Modules and Rings* - Orzech, Morris.
*Onto endomorphisms are isomorphisms* - Djoković, D. Ž.
*Epimorphisms of modules which must be isomorphisms* - Ribenboim, Paulo.
*Épimorphismes de modules qui sont nécessairement des isomorphismes*

## Tags #

free module, rank, Orzech property, (strong) rank condition, invariant basis number, IBN

We say that `R`

satisfies the strong rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)`

injective
implies `n ≤ m`

.

Any injective linear map from

`Rⁿ`

to`Rᵐ`

guarantees`n ≤ m`

.

## Instances

Any injective linear map from `Rⁿ`

to `Rᵐ`

guarantees `n ≤ m`

.

A ring satisfies the strong rank condition if and only if, for all `n : ℕ`

, any linear map
`(Fin (n + 1) → R) →ₗ[R] (Fin n → R)`

is not injective.

Any nontrivial ring satisfying Orzech property also satisfies strong rank condition.

## Equations

- ⋯ = ⋯

Any surjective linear map from `Rⁿ`

to `Rᵐ`

guarantees `m ≤ n`

.

By the universal property for free modules, any surjective map `(Fin n → R) →ₗ[R] (Fin m → R)`

has an injective splitting `(Fin m → R) →ₗ[R] (Fin n → R)`

from which the strong rank condition gives the necessary inequality for the rank condition.

## Equations

- ⋯ = ⋯

We say that `R`

has the invariant basis number property if `(Fin n → R) ≃ₗ[R] (Fin m → R)`

implies `n = m`

. This gives rise to a well-defined notion of rank of a finitely generated free
module.

Any linear equiv between

`Rⁿ`

and`Rᵐ`

guarantees`m = n`

.

## Instances

## Equations

- ⋯ = ⋯

Any nontrivial noetherian ring satisfies the strong rank condition, since it satisfies Orzech property.

## Equations

- ⋯ = ⋯

We want to show that nontrivial commutative rings have invariant basis number. The idea is to
take a maximal ideal `I`

of `R`

and use an isomorphism `R^n ≃ R^m`

of `R`

modules to produce an
isomorphism `(R/I)^n ≃ (R/I)^m`

of `R/I`

-modules, which will imply `n = m`

since `R/I`

is a field
and we know that fields have invariant basis number.

We construct the isomorphism in two steps:

- We construct the ring
`R^n/I^n`

, show that it is an`R/I`

-module and show that there is an isomorphism of`R/I`

-modules`R^n/I^n ≃ (R/I)^n`

. This isomorphism is called`Ideal.piQuotEquiv`

and is located in the file`RingTheory/Ideals.lean`

. - We construct an isomorphism of
`R/I`

-modules`R^n/I^n ≃ R^m/I^m`

using the isomorphism`R^n ≃ R^m`

.

Nontrivial commutative rings have the invariant basis number property.

In fact, any nontrivial commutative ring satisfies the strong rank condition, see
`commRing_strongRankCondition`

. We prove this instance separately to avoid dependency on
`LinearAlgebra.Charpoly.Basic`

.

## Equations

- ⋯ = ⋯