A spanning set of size rk(M) forms a basis

Stream: Is there code for X?

[Artie Khovanov]

"Let M be a free module. Then any spanning set of size rk(M) forms a basis."

This is stronger than the Rank Condition, and holds over all commutative rings - it's property (III) in https://www.sciencedirect.com/science/article/pii/0040938366900061

I'm looking for a statement of the form docs#finsetBasisOfTopLeSpanOfCardEqFinrank (this one is for division rings).

[edited repeatedly for accuracy]

[Eric Wieser]

(docs#finsetBasisOfTopLeSpanOfCardEqFinrank, docs#OrzechProperty)

[Artie Khovanov]

edited

[Junyan Xu]

There's also Module.finBasisOfFinrankEq with a Free assumption (which I agree is unnecessary by Orzech)

[Artie Khovanov]

Well it's not unncessary - you need M to be free in the first place!

[Artie Khovanov]

Oh hang on - the Orzech property doesn't say what I thought it says. It's not what I need.

[Artie Khovanov]

I've edited my post.

[Junyan Xu]

I meant it's unnecessary if we add the spanning condition.
docs#basisOfTopLeSpanOfCardEqFinrank is more pertinent, and we should be able to replace the DivisionRing assumption by OrzechProperty.

[Artie Khovanov]

Not Orzech Property! But by CommRing or alternatively by whatever condition (III) in the paper I sent is called - I'm not sure it's defined in Mathlib?
It's equivalent to "for all square matrices A,B over R such that AB=I, also BA=I".

[Eric Wieser]

Probably the interesting lemma is that the indexed set of vectors is linearly independent, rather than getting distracted by converting them into a basis

[Artie Khovanov]

Yes indeed
Downstream lemmas can be generalised

[Junyan Xu]

It's equivalent to "for all square matrices A,B over R such that AB=I, also BA=I".

Oh this is called "stably finite" in GTM 189. It's stronger than docs#RankCondition but neither weaker nor stronger than docs#StrongRankCondition. OrzechProperty implies StrongRankCondition and therefore stably finiteness.
image.png
#19581 shows CommSemirings are stably finite. We should probably introduce a typeclass for it, and I deduced StrongRankCondition in #20584.

[Artie Khovanov]

Maybe I'm misunderstanding, but I think the paper I linked says that stably finite (III) is strictly stronger than Strong Rank Condition (II):
image.png

[Junyan Xu]

(II) is the rank condition, not the strong one.
(and of course (I) is docs#InvariantBasisNumber)
image.png

[Riccardo Brasca]

Out of curiosity, what is an example of a ring that has the invariant basis number property but it doesn't satisfy the rank condition?

[Artie Khovanov]

There are examples in the paper I linked - sorry the maths is beyond me

[Junyan Xu]

Some relevant parts from Lam (GTM 189) and the paper:
image.png
image.png
image.png
image.png
and a nice synopsis
image.png

[Junyan Xu]

#32262 introduces Dedekind-finite and stably finite rings.

[Junyan Xu]

Experimented a bit with performance optimization and I'm happy with the current state of the PR.

[Junyan Xu]

... but as it turns out, the correct condition for docs#finsetBasisOfTopLeSpanOfCardEqFinrank really is Orzech property, not stable finitenss or something else, see #32339.

[Artie Khovanov]

I'm confused. I thought Orzech is stronger than stable finiteness. The thing I linked says precisely that stable finiteness is equivalent to condition (III) "any generating set of n elements in R^n is free." Whereas Orzech contains the behaviour of non-free modules, too.

[Junyan Xu]

Oh I forgot about freeness. finsetBasisOfTopLeSpanOfCardEqFinrank doesn't contain the freeness condition (though it's automatic under the original DivisionRing assumption now generalized away).
If you assume freeness then yes IsStablyFiniteRing is enough. I might add this to #32262 some time later.

[Junyan Xu]

Though this version (with freeness assumption) can't quite be stated using finrank: since stably finiteness doesn't imply the strong rank condition, R^n may have infinity rank (=> zero finrank). This isn't a problem with Orzech property, which implies the strong rank condition.

[Artie Khovanov]

Well yeah you also have to assume finite rank

[Artie Khovanov]

Oh maybe I'm missing something
In any case this is enough for what I need so thanks!

[Junyan Xu]

R^n is usually said to be free of finite rank n for any semiring R, but in mathlib Module.rank is the supremum of cardinalities of linearly independent sets. If R doesn't satisfy strong rank condition, then some R^{n+1} embeds into R^n, and one can show (#32194) that R^n must then contain an infinite linearly independent set, so its rank according to mathlib is infinite. (It's relatively easy to see the rank is infinite since ... embeds in R^{n+3} embeds in R^{n+2} embeds in R^{n+1} embeds in R^n.)

[Artie Khovanov]

Oh I see, it's a subtlety in how "rank" is defined.

[Antoine Chambert-Loir]

“R^n is usually said to be free of finite rank n for any semiring R” — I'm not sure how “usual” this is, because when R^n is isomorphic to, say, R^2n, one wouldn't say simultaneously that a module is free of rank n and 2n.

[Junyan Xu]

Search results suggests that people routinely talk about ranks as cardinalities of free generating sets that are not a priori unique.

[Antoine Chambert-Loir]

Using StackExchange for this test is a bit paradoxical, since most of its users are half-instructed people. And even mathematicians are used to frame their thoughts upside-down. But that doesn't mean that "rank" is ill-defined.

[Antoine Chambert-Loir]

Colleagues who have thought about this “know” that the dimension of a (projective) module over a commutative ring should be a (locally constant) function on the spectrum of that ring, as is the dimension of a topological space (of a manifold). But this correct definition is hard to implement in practice (if the dimension of a manifold varies, how do you frame the duality of differential forms/currents, etc.) so that most people half-renounce that subtlety.

[Junyan Xu]

Mathlib does have Module.isLocallyConstant_rankAtStalk_freeLocus

The SE questions mentions Dummit--Foote so I looked into the textbook. It is apparent that they are really using the word "rank" for free objects without assuming it has to be unique. Moreover it does define $R^n$ to be "the free module of rank n" over any ring R.
image.png
image.png
image.png
image.png
image.png
image.png

[Antoine Chambert-Loir]

I was presomptuous of my colleagues. I wonder how can we expect our students to understand something.

[Antoine Chambert-Loir]

In any case, thank you for this reference. This is really instructive.