Mathlib.LinearAlgebra.InvariantBasisNumber

Module docstring

{"# 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/Invariantbasisnumber
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

","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. "}

StrongRankCondition structure

Full source

/-- We say that `R` satisfies the strong rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)` injective
    implies `n ≤ m`. -/
@[mk_iff]
class StrongRankCondition : Prop where
  /-- Any injective linear map from `Rⁿ` to `Rᵐ` guarantees `n ≤ m`. -/
  le_of_fin_injective : ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Injective f → n ≤ m

Strong Rank Condition for Rings

Informal description

A ring $ R $ satisfies the *strong rank condition* if for any natural numbers $ n $ and $ m $, the existence of an injective linear map $ ( \text{Fin } n \to R ) \to_{R} ( \text{Fin } m \to R ) $ implies $ n \leq m $. This condition ensures that the dimension of free modules over $ R $ is well-behaved under injective linear transformations.

le_of_fin_injective theorem

[StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) : Injective f → n ≤ m

Full source

theorem le_of_fin_injective [StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) :
    Injective f → n ≤ m :=
  StrongRankCondition.le_of_fin_injective f

Injective Linear Maps Preserve Rank under Strong Rank Condition

Informal description

Let $ R $ be a ring satisfying the strong rank condition. For any natural numbers $ n $ and $ m $, if there exists an injective linear map $ f \colon R^n \to R^m $ (where $ R^n $ denotes the free $ R $-module $ \text{Fin } n \to R $), then $ n \leq m $.

strongRankCondition_iff_succ theorem

: StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective f

Full source

/-- 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. -/
theorem strongRankCondition_iff_succ :
    StrongRankConditionStrongRankCondition R ↔
      ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective f := by
  refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩
  · letI : StrongRankCondition R := h
    exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)
  · by_contra H
    exact
      h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
        (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))

Strong Rank Condition Characterization via Injective Maps on Free Modules

Informal description

A ring $R$ satisfies the strong rank condition if and only if for every natural number $n$, there does not exist an injective linear map from the free $R$-module $R^{n+1}$ to the free $R$-module $R^n$.

strongRankCondition_of_orzechProperty instance

[Nontrivial R] [OrzechProperty R] : StrongRankCondition R

Full source

/-- Any nontrivial ring satisfying Orzech property also satisfies strong rank condition. -/
instance (priority := 100) strongRankCondition_of_orzechProperty
    [Nontrivial R] [OrzechProperty R] : StrongRankCondition R := by
  refine (strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_
  let f : (Fin (n + 1) → R) →ₗ[R] Fin n → R := {
    toFun := fun x ↦ x ∘ Fin.castSucc
    map_add' := fun _ _ ↦ rfl
    map_smul' := fun _ _ ↦ rfl
  }
  have h : (0 : Fin (n + 1) → R) = update (0 : Fin (n + 1) → R) (Fin.last n) 1 := by
    apply OrzechProperty.injective_of_surjective_of_injective i f hi
      (Fin.castSucc_injective _).surjective_comp_right
    ext m
    simp [f, update_apply]
  simpa using congr_fun h (Fin.last n)

Orzech Property Implies Strong Rank Condition for Nontrivial Rings

Informal description

Every nontrivial ring $R$ satisfying the Orzech property also satisfies the strong rank condition. That is, if for any finitely generated $R$-module $M$ and any surjective homomorphism $f \colon N \to M$ from a submodule $N$ of $M$ to $M$ is injective, then for any natural numbers $n$ and $m$, the existence of an injective linear map $R^n \to R^m$ implies $n \leq m$.

card_le_of_injective theorem

 [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α → R) →ₗ[R] β → R) (i : Injective f) :
  Fintype.card α ≤ Fintype.card β

Full source

theorem card_le_of_injective [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α → R) →ₗ[R] β → R) (i : Injective f) : Fintype.card α ≤ Fintype.card β := by
  let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
  let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
  exact
    le_of_fin_injective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
      (((LinearEquiv.symm Q).injective.comp i).comp (LinearEquiv.injective P))

Cardinality Bound for Injective Linear Maps under Strong Rank Condition

Informal description

Let $R$ be a ring satisfying the strong rank condition. For any finite types $\alpha$ and $\beta$, if there exists an injective linear map $f \colon (\alpha \to R) \to (\beta \to R)$ between the corresponding free $R$-modules, then the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$.

card_le_of_injective' theorem

 [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Injective f) :
  Fintype.card α ≤ Fintype.card β

Full source

theorem card_le_of_injective' [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Injective f) : Fintype.card α ≤ Fintype.card β := by
  let P := Finsupp.linearEquivFunOnFinite R R β
  let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
  exact
    card_le_of_injective R ((P.toLinearMap.comp f).comp Q.toLinearMap)
      ((P.injective.comp i).comp Q.injective)

Cardinality Bound for Injective Linear Maps on Finitely Supported Modules under Strong Rank Condition

Informal description

Let $R$ be a ring satisfying the strong rank condition. For any finite types $\alpha$ and $\beta$, if there exists an injective linear map $f \colon (\alpha \to_0 R) \to (\beta \to_0 R)$ between the corresponding finitely supported free $R$-modules, then the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$.

RankCondition structure

Full source

/-- We say that `R` satisfies the rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)` surjective
    implies `m ≤ n`. -/
class RankCondition : Prop where
  /-- Any surjective linear map from `Rⁿ` to `Rᵐ` guarantees `m ≤ n`. -/
  le_of_fin_surjective : ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Surjective f → m ≤ n

Rank condition for rings

Informal description

A ring $R$ satisfies the *rank condition* if for any natural numbers $n$ and $m$, the existence of a surjective linear map from the free module $R^n$ to $R^m$ implies that $m \leq n$.

le_of_fin_surjective theorem

[RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) : Surjective f → m ≤ n

Full source

theorem le_of_fin_surjective [RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) :
    Surjective f → m ≤ n :=
  RankCondition.le_of_fin_surjective f

Surjective linear maps between finite free modules imply inequality of dimensions under rank condition

Informal description

Let $R$ be a ring satisfying the rank condition. For any natural numbers $n$ and $m$, if there exists a surjective linear map $f: R^n \to R^m$ of $R$-modules, then $m \leq n$.

card_le_of_surjective theorem

 [RankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α → R) →ₗ[R] β → R) (i : Surjective f) :
  Fintype.card β ≤ Fintype.card α

Full source

theorem card_le_of_surjective [RankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α → R) →ₗ[R] β → R) (i : Surjective f) : Fintype.card β ≤ Fintype.card α := by
  let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
  let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
  exact
    le_of_fin_surjective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
      (((LinearEquiv.symm Q).surjective.comp i).comp (LinearEquiv.surjective P))

Surjective Linear Maps Between Finite Free Modules Imply Cardinality Inequality Under Rank Condition

Informal description

Let $R$ be a ring satisfying the rank condition. For any finite types $\alpha$ and $\beta$, if there exists a surjective linear map $f: (\alpha \to R) \to (\beta \to R)$ of $R$-modules, then the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$.

card_le_of_surjective' theorem

 [RankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Surjective f) :
  Fintype.card β ≤ Fintype.card α

Full source

theorem card_le_of_surjective' [RankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Surjective f) : Fintype.card β ≤ Fintype.card α := by
  let P := Finsupp.linearEquivFunOnFinite R R β
  let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
  exact
    card_le_of_surjective R ((P.toLinearMap.comp f).comp Q.toLinearMap)
      ((P.surjective.comp i).comp Q.surjective)

Surjective Linear Maps Between Finite Free Modules Imply Cardinality Inequality (Finitely Supported Case)

Informal description

Let $R$ be a ring satisfying the rank condition. For any finite types $\alpha$ and $\beta$, if there exists a surjective linear map $f: (\alpha \to_{\text{fin}} R) \to (\beta \to_{\text{fin}} R)$ of $R$-modules (where $\to_{\text{fin}}$ denotes finitely supported functions), then the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$.

rankCondition_of_strongRankCondition instance

[StrongRankCondition R] : RankCondition R

Full source

/-- 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.
-/
instance (priority := 100) rankCondition_of_strongRankCondition [StrongRankCondition R] :
    RankCondition R where
  le_of_fin_surjective f s :=
    le_of_fin_injective R _ (f.splittingOfFunOnFintypeSurjective_injective s)

Strong Rank Condition Implies Rank Condition

Informal description

Every ring $R$ satisfying the strong rank condition also satisfies the rank condition. That is, if for any natural numbers $n$ and $m$, the existence of an injective linear map $R^n \to R^m$ implies $n \leq m$, then the existence of a surjective linear map $R^n \to R^m$ implies $m \leq n$.

InvariantBasisNumber structure

Full source

/-- 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. -/
class InvariantBasisNumber : Prop where
  /-- Any linear equiv between `Rⁿ` and `Rᵐ` guarantees `m = n`. -/
  eq_of_fin_equiv : ∀ {n m : ℕ}, ((Fin n → R) ≃ₗ[R] Fin m → R) → n = m

Invariant Basis Number Property

Informal description

A ring $ R $ is said to have the *invariant basis number property* if for any natural numbers $ n $ and $ m $, the existence of a linear isomorphism between the free $ R $-modules $ R^n $ and $ R^m $ implies $ n = m $. This ensures that the rank of a finitely generated free $ R $-module is well-defined.

invariantBasisNumber_of_rankCondition instance

[RankCondition R] : InvariantBasisNumber R

Full source

instance (priority := 100) invariantBasisNumber_of_rankCondition [RankCondition R] :
    InvariantBasisNumber R where
  eq_of_fin_equiv e := le_antisymm (le_of_fin_surjective R e.symm.toLinearMap e.symm.surjective)
    (le_of_fin_surjective R e.toLinearMap e.surjective)

Rank Condition Implies Invariant Basis Number Property

Informal description

Every ring $R$ satisfying the rank condition also satisfies the invariant basis number property. That is, if for any natural numbers $n$ and $m$, the existence of a surjective linear map $R^n \to R^m$ implies $m \leq n$, then any linear isomorphism $R^n \simeq R^m$ implies $n = m$.

card_eq_of_linearEquiv theorem

{α β : Type*} [Fintype α] [Fintype β] (f : (α → R) ≃ₗ[R] β → R) : Fintype.card α = Fintype.card β

Full source

theorem card_eq_of_linearEquiv {α β : Type*} [Fintype α] [Fintype β] (f : (α → R) ≃ₗ[R] β → R) :
    Fintype.card α = Fintype.card β :=
  eq_of_fin_equiv R
    ((LinearEquiv.funCongrLeft R R (Fintype.equivFin α)).trans f ≪≫ₗ
      (LinearEquiv.funCongrLeft R R (Fintype.equivFin β)).symm)

Equality of Cardinalities under Linear Equivalence of Free Modules

Informal description

Let $R$ be a ring and let $\alpha$ and $\beta$ be finite types. Given a linear equivalence $f \colon (\alpha \to R) \simeq (\beta \to R)$ between the free $R$-modules on $\alpha$ and $\beta$, the cardinalities of $\alpha$ and $\beta$ are equal, i.e., $|\alpha| = |\beta|$.

nontrivial_of_invariantBasisNumber theorem

: Nontrivial R

Full source

theorem nontrivial_of_invariantBasisNumber : Nontrivial R := by
  by_contra h
  refine zero_ne_one (eq_of_fin_equiv R ?_)
  haveI := not_nontrivial_iff_subsingleton.1 h
  haveI : Subsingleton (Fin 1 → R) :=
    Subsingleton.intro fun a b => funext fun x => Subsingleton.elim _ _
  exact
    { toFun := 0
      invFun := 0
      map_add' := by simp
      map_smul' := by simp
      left_inv := fun _ => by simp [eq_iff_true_of_subsingleton]
      right_inv := fun _ => by simp [eq_iff_true_of_subsingleton] }

Nontriviality of Rings with Invariant Basis Number Property

Informal description

If a ring $R$ has the invariant basis number property, then $R$ is nontrivial (i.e., $0 \neq 1$ in $R$).

IsNoetherianRing.strongRankCondition instance

: StrongRankCondition R

Full source

/-- Any nontrivial noetherian ring satisfies the strong rank condition,
    since it satisfies Orzech property. -/
instance (priority := 100) IsNoetherianRing.strongRankCondition : StrongRankCondition R :=
  inferInstance

Noetherian Rings Satisfy the Strong Rank Condition

Informal description

Every nontrivial left-noetherian ring satisfies the strong rank condition. That is, for any natural numbers $n$ and $m$, if there exists an injective linear map from the free module $R^n$ to the free module $R^m$, then $n \leq m$.

invariantBasisNumber_of_nontrivial_of_commRing instance

{R : Type u} [CommRing R] [Nontrivial R] : InvariantBasisNumber R

Full source

/-- 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` or `Mathlib.LinearAlgebra.Matrix.ToLin`. -/
instance (priority := 100) invariantBasisNumber_of_nontrivial_of_commRing {R : Type u} [CommRing R]
    [Nontrivial R] : InvariantBasisNumber R :=
  ⟨fun e =>
    let ⟨I, _hI⟩ := Ideal.exists_maximal R
    eq_of_fin_equiv (R ⧸ I)
      ((Ideal.piQuotEquiv _ _).symm ≪≫ₗ inducedEquiv _ e ≪≫ₗ Ideal.piQuotEquiv _ _)⟩

Nontrivial Commutative Rings Have Invariant Basis Number

Informal description

Every nontrivial commutative ring $R$ has the invariant basis number property. That is, for any natural numbers $n$ and $m$, if there exists a linear isomorphism between the free $R$-modules $R^n$ and $R^m$, then $n = m$.