mathlib3 documentation

linear_algebra.invariant_basis_number

Invariant basis number property #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We say that a ring R satisfies the invariant basis number property if there is a well-defined notion of the rank of a finitely generated free (left) R-module. Since a finitely generated free module with a basis consisting of n elements is linearly equivalent to fin n → R, it is sufficient that (fin n → R) ≃ₗ[R] (fin m → R) implies n = m.

It is also useful to consider two stronger conditions, namely the rank condition, that a surjective linear map (fin n → R) →ₗ[R] (fin m → R) implies m ≤ n and the strong rank condition, that an injective linear map (fin n → R) →ₗ[R] (fin m → R) implies n ≤ m.

The strong rank condition implies the rank condition, and the rank condition implies the invariant basis number property.

Main definitions #

strong_rank_condition R is a type class stating that R satisfies the strong rank condition. rank_condition R is a type class stating that R satisfies the rank condition. invariant_basis_number R is a type class stating that R has the invariant basis number property.

Main results #

We show that every nontrivial left-noetherian ring satisfies the strong rank condition, (and so in particular every division ring or field), and then use this to show every nontrivial commutative ring has the invariant basis number property.

More generally, every commutative ring satisfies the strong rank condition. This is proved in linear_algebra/free_module/strong_rank_condition. We keep invariant_basis_number_of_nontrivial_of_comm_ring here since it imports fewer files.

Future work #

So far, there is no API at all for the invariant_basis_number 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, invariant basis number, IBN

@[class]

structure strong_rank_condition (R : Type u) [semiring R] :

Prop

le_of_fin_injective : ∀ {n m : ℕ} (f : (fin n → R) →ₗ[R] fin m → R), function.injective ⇑f → n ≤ m

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

Instances of this typeclass

theorem strong_rank_condition_iff (R : Type u) [semiring R] :

strong_rank_condition R ↔ ∀ {n m : ℕ} (f : (fin n → R) →ₗ[R] fin m → R), function.injective ⇑f → n ≤ m

theorem le_of_fin_injective (R : Type u) [semiring R] [strong_rank_condition R] {n m : ℕ} (f : (fin n → R) →ₗ[R] fin m → R) :

function.injective ⇑f → n ≤ m

theorem strong_rank_condition_iff_succ (R : Type u) [semiring R] :

strong_rank_condition 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.

theorem card_le_of_injective (R : Type u) [semiring R] [strong_rank_condition R] {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : (α → R) →ₗ[R] β → R) (i : function.injective ⇑f) :

fintype.card α ≤ fintype.card β

theorem card_le_of_injective' (R : Type u) [semiring R] [strong_rank_condition R] {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R) (i : function.injective ⇑f) :

fintype.card α ≤ fintype.card β

@[class]

structure rank_condition (R : Type u) [semiring R] :

Prop

le_of_fin_surjective : ∀ {n m : ℕ} (f : (fin n → R) →ₗ[R] fin m → R), function.surjective ⇑f → m ≤ n

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

Instances of this typeclass

rank_condition_of_strong_rank_condition

theorem le_of_fin_surjective (R : Type u) [semiring R] [rank_condition R] {n m : ℕ} (f : (fin n → R) →ₗ[R] fin m → R) :

function.surjective ⇑f → m ≤ n

theorem card_le_of_surjective (R : Type u) [semiring R] [rank_condition R] {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : (α → R) →ₗ[R] β → R) (i : function.surjective ⇑f) :

fintype.card β ≤ fintype.card α

theorem card_le_of_surjective' (R : Type u) [semiring R] [rank_condition R] {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R) (i : function.surjective ⇑f) :

fintype.card β ≤ fintype.card α

@[protected, instance]

def rank_condition_of_strong_rank_condition (R : Type u) [semiring R] [strong_rank_condition R] :

rank_condition 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.

@[class]

structure invariant_basis_number (R : Type u) [semiring R] :

Prop

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

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.

Instances of this typeclass

@[protected, instance]

def invariant_basis_number_of_rank_condition (R : Type u) [semiring R] [rank_condition R] :

invariant_basis_number R

theorem eq_of_fin_equiv (R : Type u) [semiring R] [invariant_basis_number R] {n m : ℕ} :

((fin n → R) ≃ₗ[R] fin m → R) → n = m

theorem card_eq_of_lequiv (R : Type u) [semiring R] [invariant_basis_number R] {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : (α → R) ≃ₗ[R] β → R) :

fintype.card α = fintype.card β

theorem nontrivial_of_invariant_basis_number (R : Type u) [semiring R] [invariant_basis_number R] :

@[protected, instance]

def noetherian_ring_strong_rank_condition (R : Type u) [ring R] [nontrivial R] [is_noetherian_ring R] :

strong_rank_condition R

Any nontrivial noetherian ring satisfies the strong rank condition.

An injective map ((fin n ⊕ fin (1 + m)) → R) →ₗ[R] (fin n → R) for some left-noetherian R would force fin (1 + m) → R ≃ₗ punit (via is_noetherian.equiv_punit_of_prod_injective), which is not the case!

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.pi_quot_equiv and is located in the file ring_theory/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.

@[protected, instance]

def invariant_basis_number_of_nontrivial_of_comm_ring {R : Type u} [comm_ring R] [nontrivial R] :

invariant_basis_number R

Nontrivial commutative rings have the invariant basis number property.

In fact, any nontrivial commutative ring satisfies the strong rank condition, see comm_ring_strong_rank_condition. We prove this instance separately to avoid dependency on linear_algebra.charpoly.basic.