introduce the category of graded lattices

[fchapoton]

as this will be a useful thing to have

sequel of #39554 and #40705

📝 Checklist

• The title is concise and informative.
• The description explains in detail what this PR is about.
• I have linked a relevant issue or discussion.

[github-actions]

Documentation preview for this PR (built with commit f1db531; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

[fchapoton]

@tscrim, would you please have a look if you can ?

[tscrim]

I'm a little worried about this because it introduces a subtle conflict with the graded functorial constructions. It becomes easy to accidentally declare it as an axiom for non-posets. In somr ways, "Ranked" is a better choice, but that is, of course, a slightly different (more general) concept. I feel like we should try to find a slightly different name to avoid the conflict. Maybe "GradedByChains"? That's a bit long though...

@nthiery Do you have any thoughts about this?

[fchapoton]

I do not think that Nicolas is listening. Somewhere in our doc, it is written that one should be able to use the same axiom name in unrelated domains without too much issues. But the "Graded" functorial construction is not an axiom, probably ?

[nthiery]

Thank you for the continued progress on posets and lattices!

I do not think that Nicolas is listening.

Yeah, more or less. I actually do get notifications on explicit mentions :-) But not necessarily active though if I don't have up to date information ...

In the case at hand, as far as I can remember, it should be completely safe to have a functorial construction and an axiom with the same name, as long one never construct a category deriving both from Modules().Graded() and LatticePosets().Graded().

So the questions are:

1. can we preclude that, in the foreseeable future, someone will want to create a parent that would be both a lattice and a vector space (e.g. over a finite field), and where Graded could be ambiguous?
2. could it be confusing for the users to have an axiom and a functorial construction with same name but distinct semantic.

If in doubt, the axiom for posets could be called with a disambiguated name e.g. LatticePosets().GradedAsLattice(), while still having it printed as, e.g. graded lattice by tweaking CategoryWithAxiom._repr_object_names_static. Which would be a minor annoyance given that .GradedAsLattice` can still easily be discovered by automatic completion.

Btw: should the graded axiom be defined more generally for posets?

Altogether, I don't have opinions in one or the other direction.

Cheers,

[fchapoton]

Concerning question 1, I would not expect this to happen.

Cocnerning question 2. Only advanced users can see that possible confusion, maybe they will know enough ?

I am currently not introducing axioms for posets, only axioms for lattices. My aim is to move some methods to the appropriate category and also to introduce at least one new method in the correct place.

So I would prefer to keep "Graded" as an axiom for lattices.

[mantepse]

I understand that you only want to introduce axioms for lattices now, but are you excluding the possibility of having axioms for posets at some point in the future?

On the other hand, if we have a graded poset which is also a module, I can imagine that the most natural grading of the module is the same as the grading of the poset. However, I don't know.

How much does it hurt to call the axiom "GradedAsOrder"?

[fchapoton]

I do not exclude to introduce axioms for posets later. Maybe "Bounded" (having 0 and 1) would be the first one coming to my mind.

[tscrim]

@nthiery Thank you for responding.

Sorry for taking some time for my response.

1. I believe I have a somewhat reasonable example: graded crystals. For a highest weight crystal, it is naturally a graded poset, but there are (natural) gradings from the corresponding modules that would not necessarily agree with the poset grading. I don’t have a reason currently to build this, but it is certainly possible for this to be declared. It is already done implicitly by statistics in certain cases, so it’s still mildly contrived…
2. I think this would be confusing for someone trying to implement their own categories. While this is a more advanced user, I don’t think they need to be that advanced in order to want to access these features. I think it is a little too easy for someone to mistakenly use the axiom when they actually wanted a functorial construction.

It might also have similar such conflicts as “graded” is something that can get used more often in other contexts… So I am more firmly thinking we need to have a different name for this axiom.

The correct place to introduce this axiom would be in posets. IMO it would be better to add it to the correct place and just be done with it.

[fchapoton]

Would ChainGraded be a correct name ?

I tried and failed to introduce a ChainGraded axiom for finite posets, sigh.

[tscrim]

I'm very sorry for not being able to get to this faster.

I think chain graded is a very good name for this axiom.

What you've done mostly looks good for the implementation except for what I noted. What's not working correctly?

[tscrim]

This isn't the correct way to introduce this relation. You either want to use extra_super_categories to add the distributive lattices as a supercategory or the same mechanism used for Wedderburn's theorem.

[fchapoton]

Thanks, Travis. Now I would prefer to do #41216 first, if this makes sense.