Length of a module?

Stream: Is there code for X?

[Jz Pan]

We have assertion that a module is of finite length docs#IsFiniteLength, but seems that we don't have have the definition of the length of a module yet.

[Jz Pan]

I think there was discussions of Jordan-H\"older series (for modules) before, but I can't find the links.

[Johan Commelin]

cc @Raphael Douglas Giles and @Andrew Yang

[Raphael Douglas Giles]

So there's been a little bit of work on this, and it should be in mathlib relatively soon. I worked on some API for lengths of modules in #22127 using an approach which requires some refactoring of Relseries stuff to make work as nicely as I thought it would. In that thread, @Andrew Yang gave some code detailing an alternate approach which makes better use of the existing API, and we decided it would be best to pursue this method for getting module lengths into mathlib. PRs  #21800 and #21803 are developing some of the material used here, and once these are merged in I think we should be pretty close to having lengths of modules and some nice api for them

[Jz Pan]

Thanks. I'm in a group which are starting a project to formalize some basic concepts of Iwasawa Theory. I'm studying what materials on commutative algebra we have in mathlib.

[Filippo A. E. Nuccio]

Jz Pan said:

Thanks. I'm in a group which are starting a project to formalize some basic concepts of Iwasawa Theory. I'm studying what materials on commutative algebra we have in mathlib.

Oh, I'd be very interested in following the advances of this group, where does it meet @Jz Pan ?

[Jz Pan]

Filippo A. E. Nuccio said:

Jz Pan said:

Thanks. I'm in a group which are starting a project to formalize some basic concepts of Iwasawa Theory. I'm studying what materials on commutative algebra we have in mathlib.

Oh, I'd be very interested in following the advances of this group, where does it meet Jz Pan ?

It's a tentative project in Academy of Mathematics and Systems Science, Chinese Academy of Sciences. Once it's started I'll try my best to setup a blueprint. Now I need to do a little research to find out all available prerequisites (even for WIP pull requests and for those in separate repositories), to reduce duplicated work.

[Filippo A. E. Nuccio]

Oh great, I'll be at Pekin Univ for ten days at the beginning of May, I'd be happy to discuss.

[Riccardo Brasca]

I will also be in Beijing, and very happy to discuss about this!

[Oliver Nash]

Jz Pan said:

We have assertion that a module is of finite length docs#IsFiniteLength, but seems that we don't have have the definition of the length of a module yet.

IMHO we shouldn't really have the IsFiniteLength definition since it means we have two ways to say the same thing. I do accept the justification that it gives a convenient induction principle for proving the basic results but I claim that all API should be written under the assumptions [IsNoetherian R M] [IsArtinian R M] rather than IsFiniteLength.

[Jz Pan]

Oliver Nash said:

Jz Pan said:

We have assertion that a module is of finite length docs#IsFiniteLength, but seems that we don't have have the definition of the length of a module yet.

IMHO we shouldn't really have the IsFiniteLength definition since it means we have two ways to say the same thing. I do accept the justification that it gives a convenient induction principle for proving the basic results but I claim that all API should be written under the assumptions [IsNoetherian R M] [IsArtinian R M] rather than IsFiniteLength.

Oh, I see. I'll note in the blueprint.

[Jz Pan]

By the way, do we have consensus that the function name of the length of a module? Module.length? Does the definition requires IsNoetherian + IsArtinian, or it's definition is if ... then ... else 0?

[Jz Pan]

I'll write down this in the experimental code, with all of its property sorry.

[Kevin Buzzard]

The definition of docs#finsum is if ... then ... else 0.