Documentation

Mathlib.LinearAlgebra.InvariantBasisNumber

Invariant basis number property #

Main definitions #

Let R be a (not necessary commutative) ring.

It is also useful to consider the following stronger conditions:

Instances #

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):

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 #

Tags #

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

theorem strongRankCondition_iff (R : Type u) [Semiring R] :
StrongRankCondition R ∀ {n m : } (f : (Fin nR) →ₗ[R] Fin mR), Function.Injective fn m

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

Instances
    theorem StrongRankCondition.le_of_fin_injective {R : Type u} :
    ∀ {inst : Semiring R} [self : StrongRankCondition R] {n m : } (f : (Fin nR) →ₗ[R] Fin mR), Function.Injective fn m

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

    theorem le_of_fin_injective (R : Type u) [Semiring R] [StrongRankCondition R] {n : } {m : } (f : (Fin nR) →ₗ[R] Fin mR) :
    Function.Injective fn m
    theorem strongRankCondition_iff_succ (R : Type u) [Semiring R] :
    StrongRankCondition R ∀ (n : ) (f : (Fin (n + 1)R) →ₗ[R] Fin nR), ¬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.

    @[instance 100]

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

    Equations
    • =
    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) :
    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) :
    class RankCondition (R : Type u) [Semiring R] :

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

    Instances
      theorem RankCondition.le_of_fin_surjective {R : Type u} :
      ∀ {inst : Semiring R} [self : RankCondition R] {n m : } (f : (Fin nR) →ₗ[R] Fin mR), Function.Surjective fm n

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

      theorem le_of_fin_surjective (R : Type u) [Semiring R] [RankCondition R] {n : } {m : } (f : (Fin nR) →ₗ[R] Fin mR) :
      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) :
      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) :
      @[instance 100]

      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.

      • eq_of_fin_equiv : ∀ {n m : }, ((Fin nR) ≃ₗ[R] Fin mR)n = m

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

      Instances
        theorem InvariantBasisNumber.eq_of_fin_equiv {R : Type u} :
        ∀ {inst : Semiring R} [self : InvariantBasisNumber R] {n m : }, ((Fin nR) ≃ₗ[R] Fin mR)n = m

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

        @[instance 100]
        Equations
        • =
        theorem eq_of_fin_equiv (R : Type u) [Semiring R] [InvariantBasisNumber R] {n : } {m : } :
        ((Fin nR) ≃ₗ[R] Fin mR)n = m
        theorem card_eq_of_linearEquiv (R : Type u) [Semiring R] [InvariantBasisNumber R] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : (αR) ≃ₗ[R] βR) :
        @[instance 100]

        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:

        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.
        @[instance 100]

        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
        • =