Codimension of the annihilator

Stream: Is there code for X?

[Yaël Dillies]

I am explicitly not going to give Lean code here, because I want to know how you would write it in Lean. I am looking for the following mathematical statement: If $V$ is a (finite dimensional if you want) $\R$-vector space and $\Delta \subseteq V$ is a finite set, then $\{f : V \to \R \mid \forall d \in \Delta, f(d) = 0\}$ has codimension at most $|\Delta|$ as a subspace of $V \to \R$ (the space of linear maps, not just bare functions).

[Yaël Dillies]

Do we have this, in any form?

[Kyle Miller]

If W is the subspace spanned by $\Delta$ (Submodule.span \R \Delta), then your set is W.dualAnnihilator, and the codimension of it can be calculated using docs#Subspace.quotAnnihilatorEquiv to see that Dual \R V / W.dualAnnihilator is Dual \R W, which has dimension at most $|\Delta|$.

[Yaël Dillies]

Nice! Do we have any spelling for codimension but finrank k Space - finrank k Subspace?

[Kyle Miller]

It looks like Module.rank k (Space / Subspace) is common for codimension. Given that there's no corank or codim, I'd probably put theorems into that form. This has the benefit that it supports infinite dimensional subspaces of finite codimension.

[Yaël Dillies]

Okay, that's a nice suggestion! I will adapt to it

[Yaël Dillies]

Do we then have antitonicity of codimension with this spelling?

[Kyle Miller]

I'm sure there's something for antitonicity of quotients, but for codimension itself the only things I can find are docs#Submodule.finrank_quotient_add_finrank and docs#rank_quotient_add_rank

[Johan Commelin]

Kyle Miller said:

It looks like Module.rank k (Space / Subspace) is common for codimension. Given that there's no corank or codim, I'd probably put theorems into that form. This has the benefit that it supports infinite dimensional subspaces of finite codimension.

Nevertheless, we should probably turn this into a defn, and write a little API for it. Don't you think?

[Antoine Chambert-Loir]

Should it be a particular case of a more general theory for modules of finite length?

[Johan Commelin]

You mean that we should generalize k? I agree.

[Antoine Chambert-Loir]

On the other hand, “le mieux est l'ennemi du bien” as we say in French, so maybe it's better to have today some API which is not fully general, but can be generalized by somebody who needs it — and builds on it — than never having the ultimate one.

[Bhavik Mehta]

Antoine Chambert-Loir said:

On the other hand, “le mieux est l'ennemi du bien” as we say in French, so maybe it's better to have today some API which is not fully general, but can be generalized by somebody who needs it — and builds on it — than never having the ultimate one.

(as an aside: I've also heard this phrase in English so I was curious about its origin, supposedly it's originally an Italian proverb!)

[Riccardo Brasca]

Which one?

[Yaël Dillies]

Antoine Chambert-Loir said:

Should it be a particular case of a more general theory for modules of finite length?

I don't know what a module of finite length is. Can you expand on what the generalisation would look like?

[Kevin Buzzard]

(finite length means there's a finite chain of submodules such that each one when quotiented out by the next one is a simple module, i.e. only has bot and top as submodules. For example you would filter a f.d.v.s over $k$ by subspaces with dimensions growing by 1 each time, as the simple $k$-modules are the 1d ones if $k$ is a field. The finite length $\mathbb{Z}$-modules (i.e. abelian groups) are precisely the finite ones.)

[Antoine Chambert-Loir]

Indeed. (That's gives a slightly different point of view on dimension on vector spaces — rather than looking at bases, look at flags, increasing systems of subspaces $V_0\subset V_1\subset\dots\subset V_m$, such that all inclusions are strict and can't be refined.)

[Kyle Miller]

Antoine Chambert-Loir said:

Should it be a particular case of a more general theory for modules of finite length?

That would only be for finite corank, correct? The Module.rank k (Mod / SubMod) definition works for infinite corank as well.

It seems to me that the theory of Module.rank k (Mod / SubMod) should be related to the theory of modules of finite length in situations where it can be done, but in general these seem to be different.

[Antoine Chambert-Loir]

if dimension is length or height, codimension is colength or coheight, with a similar API which, btw, should already be implemented in a way or another.

[Kyle Miller]

Would this be restricting dimensions to finite dimensions though? Or would the definition of a flag be generalized to be a chain of submodules?

[Antoine Chambert-Loir]

A flag is a chain of submodules, the length of a module is the supremum of the lengths of all chains ($V_0\subset \dots \subset V_m$ has length $m$), the height and the coheight of a submodule are the supremum of the lengths of all chains ending or starting (I'm not clear about which is which) at this submodule.

[Antoine Chambert-Loir]

One has height + coheight = length, with usual conventions for infinite addition.

[Kyle Miller]

Just to be clear, the definition of "chain of submodules" I'm using is "a totally ordered subset of submodules". The definition of flag I'm familiar with are the ones indexed by some set {0,1,...,m}. With flags, the only possible lengths are 0,1,2,...,\infty, but with chains you can have any cardinality.

[Yaël Dillies]

Just noting that @Joachim Breitner is currently doing very good work on redefining the notion of (co)height of an element in an order

[Yaël Dillies]

... and might be interested in hearing that there is a case for cardinal-valued height

[Bhavik Mehta]

Riccardo Brasca said:

Which one?

"Il meglio è l'inimico del bene", see eg https://en.wikipedia.org/wiki/Perfect_is_the_enemy_of_good

[Daniel Weber]

Yaël Dillies said:

... and might be interested in hearing that there is a case for cardinal-valued height

Aren't heights usually ordinals?

[Violeta Hernández]

oooh, ordinal valued heights?

[Violeta Hernández]

(we've got docs#WellFounded.rank for this, btw)

[Antoine Chambert-Loir]

In the case of Artinian modules, the situation is actually well studied, eg

https://link.springer.com/article/10.1007/s13366-014-0229-z

[Antoine Chambert-Loir]

There is also a paper (I can't find it anymore) that works out the two possibilities, working with increasing or with decreasing chains, and the two theories are indeed different.