# 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 [lam_1999] (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][lam_1999]
- [Orzech, Morris. Onto endomorphisms are isomorphisms][orzech1971]
- [Djoković, D. Ž. Epimorphisms of modules which must be isomorphisms][djokovic1973]
- [Ribenboim, Paulo. Épimorphismes de modules qui sont nécessairement des isomorphismes][ribenboim1971]

## Tags #

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

source
class StrongRankCondition (R : Type u) [Semiring R] :
Prop

We say that `R` satisfies the strong rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)` injective implies `n ≤ m`.

- le_of_fin_injective {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) : Function.Injective ⇑f → n ≤ m

  Any injective linear map from `Rⁿ` to `Rᵐ` guarantees `n ≤ m`.

Instances

source
theorem strongRankCondition_iff (R : Type u) [Semiring R] :
StrongRankCondition R ↔ ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Injective ⇑f → n ≤ m
source
theorem le_of_fin_injective (R : Type u) [Semiring R] [StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) :
Function.Injective ⇑f → n ≤ m
source
theorem strongRankCondition_iff_succ (R : Type u) [Semiring R] :
StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective ⇑f

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.

source
@[instance 100]
instance strongRankCondition_of_orzechProperty (R : Type u) [Semiring R] [Nontrivial R] [OrzechProperty R] :
StrongRankCondition R

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

source
theorem card_le_of_injective (R : Type u) [Semiring R] [StrongRankCondition R] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : (α → R) →ₗ[R] β → R) (i : Function.Injective ⇑f) :
Fintype.card α ≤ Fintype.card β
source
theorem card_le_of_injective' (R : Type u) [Semiring R] [StrongRankCondition R] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Function.Injective ⇑f) :
Fintype.card α ≤ Fintype.card β
source
class RankCondition (R : Type u) [Semiring R] :
Prop

We say that `R` satisfies the rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)` surjective implies `m ≤ n`.

- le_of_fin_surjective {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) : Function.Surjective ⇑f → m ≤ n

  Any surjective linear map from `Rⁿ` to `Rᵐ` guarantees `m ≤ n`.

Instances

source
theorem le_of_fin_surjective (R : Type u) [Semiring R] [RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) :
Function.Surjective ⇑f → m ≤ n
source
theorem card_le_of_surjective (R : Type u) [Semiring R] [RankCondition R] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : (α → R) →ₗ[R] β → R) (i : Function.Surjective ⇑f) :
Fintype.card β ≤ Fintype.card α
source
theorem card_le_of_surjective' (R : Type u) [Semiring R] [RankCondition R] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Function.Surjective ⇑f) :
Fintype.card β ≤ Fintype.card α
source
theorem Module.Finite.exists_nat_not_surjective (R : Type u) [Semiring R] [RankCondition R] (M : Type u_1) [AddCommMonoid M] [Module R M] [Module.Finite R M] :
∃ (n : ℕ), ∀ (f : M →ₗ[R] Fin n → R), ¬Function.Surjective ⇑f
source
@[instance 100]
instance rankCondition_of_strongRankCondition (R : Type u) [Semiring R] [StrongRankCondition R] :
RankCondition R

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.

source
class InvariantBasisNumber (R : Type u) [Semiring R] :
Prop

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.

- eq_of_fin_equiv {n m : ℕ} : ∀ (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m

  Any linear equiv between `Rⁿ` and `Rᵐ` guarantees `m = n`.

Instances

source
@[instance 100]
instance invariantBasisNumber_of_rankCondition (R : Type u) [Semiring R] [RankCondition R] :
InvariantBasisNumber R
source
theorem eq_of_fin_equiv (R : Type u) [Semiring R] [InvariantBasisNumber R] {n m : ℕ} :
∀ (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m
source
theorem card_eq_of_linearEquiv (R : Type u) [Semiring R] [InvariantBasisNumber R] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : (α → R) ≃ₗ[R] β → R) :
Fintype.card α = Fintype.card β
source
theorem nontrivial_of_invariantBasisNumber (R : Type u) [Semiring R] [InvariantBasisNumber R] :
Nontrivial R
source
@[instance 100]
instance IsNoetherianRing.strongRankCondition (R : Type u) [Ring R] [Nontrivial R] [IsNoetherianRing R] :
StrongRankCondition R

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

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:

1. 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`.
2. We construct an isomorphism of `R/I`-modules `R^n/I^n ≃ R^m/I^m` using the isomorphism `R^n ≃ R^m`.

source
@[instance 100]
instance invariantBasisNumber_of_nontrivial_of_commRing {R : Type u} [CommRing R] [Nontrivial R] :
InvariantBasisNumber R

Nontrivial commutative rings have the invariant basis number property.

There are two stronger results in mathlib: `commRing_strongRankCondition`, which says that any nontrivial commutative ring satisfies the strong rank condition, and `rankCondition_of_nontrivial_of_commSemiring`, which says that any nontrivial commutative semiring satisfies the rank condition.

We prove this instance separately to avoid dependency on `Mathlib/LinearAlgebra/Charpoly/Basic.lean` or `Mathlib/LinearAlgebra/Matrix/ToLin.lean`.