Invariant basis number: finite version implies infinite?

Stream: maths

[Scott Morrison]

In https://leanprover-community.github.io/mathlib_docs/linear_algebra/invariant_basis_number.html, @Markus Himmel has written

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.

Does anyone know a (maths) reference for this? I would like to use it, but I don't know the argument. (@Kevin Buzzard?)

[Markus Himmel]

See for example Thm 42.6 in http://math.buffalo.edu/~badzioch/MTH619/Lecture_Notes_files/MTH619_week13.pdf

[Markus Himmel]

I wonder whether the proof of docs#basis.le_span can be generalised to any coefficient ring with IBN. I suspect that it already contains all of the hard work to get the above statement.

[Scott Morrison]

Indeed, the first case of basis.le_span (J is infinite) works over any nontrivial ring.

[Kevin Buzzard]

Thm 42.6 is false for the zero ring :p

[Scott Morrison]

I haven't seen how to make the second case of basis.le_span work assuming [invariant_basis_number] (rather than [division_ring]).

[Scott Morrison]

Is it even true? I don't know this stuff.

import linear_algebra.invariant_basis_number
import linear_algebra.basis
import set_theory.cardinal_ordinal

open submodule set

example {K V ι : Type}
  [ring K] [nontrivial K] [invariant_basis_number K]
  [add_comm_group V] [module K V]
  {J : set V} (hJ : span K J = ⊤) (oJ : cardinal.mk ↥J < cardinal.omega)
  (v : basis ι K V) :
  cardinal.mk ↥(range ⇑v) ≤ cardinal.mk ↥J :=
begin
  admit,
end

[Kevin Buzzard]

invariant_basis_number implies nontrivial. This example is true for any nontrivial commutative ring K. You have a surjection K^J -> K^v and now reducing modulo a maximal ideal of K you get a map field^J ->> field^v so v<=J. I don't know about the non-commutative case. Is it true for rings which have no non-trivial two-sided ideals? Do those rings have a name? Is that the same as a division ring? I'm clueless about the non-commutative case.

[Kevin Buzzard]

The much harder result is that if R is a nontrivial commutative ring and R^a injects into R^b then a<=b. See for example this MO question where Pete Clark writes something about the noncommutative case.

[Scott Morrison]

Okay: so we have the "strong rank condition" (injections of free modules give inequalities of ranks) which implies the "rank condition" (surjections of free modules give inequalities of ranks) which implies the "invariant basis number condition" (equivalences of free modules give equalities of ranks).

As you've observed, the example above follows immediately from the "rank condition".

As Peter explained on MO, in fact every left-Noetherian ring and every commutative ring satisfies the strong rank condition.

So one way to deal with this would be to state the "rank condition", and prove basis.le_span with that as a typeclass argument.

[Kevin Buzzard]

Oh nice!

[Scott Morrison]

Kevin Buzzard said:

Is it true for rings which have no non-trivial two-sided ideals? Do those rings have a name? Is that the same as a division ring? I'm clueless about the non-commutative case.

These are "simple rings", but in general they are far from division rings.

[Scott Morrison]

I guess a missing piece in this is that I don't know why the strong rank condition implies the rank condition.

[Scott Morrison]

But I guess I do know how to prove that left-Noetherian rings satisfy the rank condition: the proof I just PR'd early today that they have invariant basis number actually proves that anyway.

[Kevin Buzzard]

Oh, two x two complex matrices have no nontrivial two-sided ideals I guess.

[Scott Morrison]

Yes: artinian simple rings are matrices over some division ring, so this is pretty representative.

[David Wärn]

Apparently this is all dealt with in the first 11 pages of Lam's "Lectures on Modules and Rings"

[David Wärn]

So IBN does not imply rank conditoin

[David Wärn]

The implication "strong rank condition => rank condition" is easy. Suppose $f : R^m \to R^n$ is surjective. Then because $R^n$ is free $f$ splits via $g : R^n \to R^m$. Now $g$ is split monic, hence monic, so $n \le m$ by strong rank condition, as needed.

[Scott Morrison]

I'd just read that same statement in Lam and was coming here to report it. :-)

[Scott Morrison]

Okay. I may attempt this all in the next few days. I'll add [rank_condition R] as a class, prove it for left-Noetherian and commutative rings, and then try to refactor lots of linear_algebra/dimension.lean to just use rank_condition instead of field.

[Scott Morrison]

It seems this will be better than trying to do things in terms of invariant_basis_number, because some nice facts still won't be available.