Invariant basis number property
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
(fin n → R) ≃ₗ[R] (fin m → R) implies
n = m.
invariant_basis_number R is a type class stating that
R has the invariant basis number property.
We show that every nontrivial commutative ring has the invariant basis number property.
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 prividing a basis indexed by
a finite type. There should be lemmas applying the invariant basis number property to each
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.
free module, rank, invariant basis number, IBN
We want to show that nontrivial commutative rings have invariant basis number. The idea is to
take a maximal ideal
R and use an isomorphism
R^n ≃ R^m of
R modules to produce an
(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^n/I^n ≃ (R/I)^n. This isomorphism is called
ideal.pi_quot_equivand is located in the file
- We construct an isomorphism of
R^n/I^n ≃ R^m/I^musing the isomorphism
R^n ≃ R^m.