Definitions for chain height/partitions

Stream: mathlib4

[Vlad Tsyrklevich]

Just for fun I wanted to knock out one of the 1000 theorems so I formalized Dilworth's (and Mirsky's) theorems on decomposition of finite posets into chains/antichains. About a third of the formalization is just helper lemmas that I've PR'd. Another third is definitions + basic API for heights/widths of chains/antichains (e.g. maximum chain/antichain sizes) and (minimal) chain/antichain partitions.

I know that some generalizations of Dilworth's theorem like Greene-Kleitman don't directly use these definitions, e.g. G-K is stated in terms of sizes of unions of a specific number of chains/antichains, so I wasn't sure if these definitions were worth contributing to mathlib. (I assume the proofs themselves are in the wrong generality for Mathlib given the existence of e.g. Greene-Kleitman.) I wanted to see if anyone knew of other cases where these definitions might be useful, otherwise i'll just keep them in my repository.

[Vlad Tsyrklevich]

Amusingly I found this thread #Carleson > Task 52 @ 💬 and there are already at least 2 competing notions of maximum chain heights in Mathlib, though they both depend on [LT] rather than taking arbitrary relations which is concise but I dislike that it's hard to then usem with anything that's spelled otherwise.

[Vlad Tsyrklevich]

I was looking because I also realized that docs#SimpleGraph.indepNum and docs#SimpleGraph.cliqueNum are also just minimum chain heights/antichain widths in Mathlib. Partially duplicate definitions abound.

[Vlad Tsyrklevich]

@Andrew Yang Do you know if Mathlib.Order.Height is in use anywhere outside of Mathlib? In mathlib it's not included anywhere, and perhaps that's a good opportunity to generalize it to arbitrary relations

[Antoine Chambert-Loir]

Unless I'm mistaken, commutative algebra uses this notion of height for the poset of prime ideals (to define height, dimension, etc.).

[Christian Merten]

Yes docs#Order.height is used a lot in commutative algebra. A generalization would not be hard (by replacing LTSeries by a general RelSeries), but it would be better to have this as a new definition SetRel.height and make Order.height an abbreviation for SetRel.height for the most common case of preorders.

[Vlad Tsyrklevich]

Is there a reason why the RelSeries spelling is prefered over docs#List.IsChain? I saw that recently it was changed to take a relation spelled as SetRel for some reason I have not looked into yet, but otherwise it is morally identical to List.IsChain right?

[Christian Merten]

See docs#RelSeries.Equiv. I have advocated for redefining docs#RelSeries for a while. But not in the direction you propose, but rather in the direction of docs#Quiver.Path. I would introduce a SetRel.Path as an inductive type with head and last element as a parameter. A RelSeries would be a structure bundling a head, a last element and a SetRel.Path head last.
If instead of r : SetRel X X we take a general r : X -> X -> Sort*, this could be used to define docs#Quiver.Path.

Most of the RelSeries API would be developed for SetRel.Path instead, only providing simple wrapping operations in the last step when RelSeries are needed.

[Christian Merten]

The reason for this is that working with an inductive type is much smoother than with a subtype of an inductive type.

[Christian Merten]

@Edward van de Meent has made some significant progress on this in a branch, but I don't know what the status of this is.

[Vlad Tsyrklevich]

Interesting, this would be the equivalent of docs#SimpleGraph.Walk for a general relation

[Christian Merten]

Yes, there is a lot of deduplication potential here.

[Vlad Tsyrklevich]

Anyways, I would like to take a stab at upstreaming the chain height/antichain width definitions in terms of general relations and then re-defining Order.height in terms of it. I am prototyping that now locally now. (Set.chainHeight is unused and close enough in meaning that I think it could be deprecated/absorbed into the other definition)

[Vlad Tsyrklevich]

I'm putting this down for now. Though I have an API I'm happy with for working with chain heights, trying to prove equivalence with Order.height is very unergonomic. RelSeries not accepting empty lists and the use of Fin makes proving tedious, and this seems like the type of large scale change that may flounder in the review queue for lack of interest.

[Bhavik Mehta]

Can you sketch what you'd like changed? I might be able to help with getting this in

[Vlad Tsyrklevich]

The overall idea is that it would be nice to have a general definition of chain heights/antichain widths since this idea comes up in multiple places. docs#Order.height is one instance of a chain height definition that should not be generalized but could possibly be subsumed by a more general definiton. docs#Set.chainHeight is an implementation of chain heights but it appears unused and in my opinion:

• should be stated for arbitrary relations instead of LT. For example, clique/independence numbers in graph theory are chain heights/antichain widths for G.Adj and this should be supported without having to resort to have : LT V := { lt := ... everywhere
• should use docs#IsChain instead of docs#List.IsChain, e.g. all elements are comparable instead of just consecutive elements. I think this is the more common mathematical definition--the two cases are equivalent for transitive relations, but they have a different meaning in the case given above.
• from some of my experimentation locally, I think the definition of chain heights should also probably be for Types and not for Sets, e.g. chainHeight type rel instead of set.chainHeight rel. Some of the proofs go through more cleanly and it's a bit more flexible.

The disadvantages I can think of with my approach are:

• Carrying around a (· < ·) term, though this is likely to be hidden by defs wrapping the API
• Dealing with set subtypes in some places, but in my experience it's not so bad to write chainHeight ↑s rel instead of s.chainHeight rel.

I think 1) Set.chainHeight should be replaced by a more general definition with comparable API [and also add an antichainWidth analog], and 2) Order.height could then be re-defined using that definition (in a non-breaking equivalent way.) I think the first step is something I could polish and achieve fairly easily, I've already developed most of it and just need to expand and polish. The second will require more time to develop some API to make the transition smooth.

I think just doing step #1 is a good step since it replaces an unused definition with a more general version, and I am also interested in going through with step #2 if there's interest in having me do this--I just think it's too big an undertaking to do speculatively.

[Edward van de Meent]

Vlad Tsyrklevich said:

I think this is the more common mathematical definition--the two cases are equivalent for transitive relations, but they have a different meaning in the case given above.

i don't feel this is true? i'm pretty sure the equivalent notion of "chain" for a graph would be a path, not a clique?

[Bhavik Mehta]

I agree docs#chainHeight should be stated for arbitrary relations, but I don't think it's useful to redefine docs#SimpleGraph.cliqueNum in terms of it, since the current definition is more workable in practice. I'm in favour of a lemma linking them though.
I agree using docs#IsChain is more reasonable than docs#List.IsChain (although note that docs#List.Pairwise gives a non-transitive version).
It's not clear to me that the types version is better than the sets version here, it might be reasonable to have both? Note that docs#IsChain is for sets, and many order-theoretic things are in general.

[Bhavik Mehta]

Edward van de Meent said:

Vlad Tsyrklevich said:

I think this is the more common mathematical definition--the two cases are equivalent for transitive relations, but they have a different meaning in the case given above.

i don't feel this is true? i'm pretty sure the equivalent notion of "chain" for a graph would be a path, not a clique?

If chain uses consecutive elements, then it's a path, but if it's arbitrary (as Vlad wants to change it to) then it's a clique.

[Bhavik Mehta]

I'd like to hear @Andrew Yang's opinion here, since he wrote docs#Set.chainHeight, did you have a particular use-case in mind? If so, we should make sure to support it.

[Edward van de Meent]

indeed if it's arbitrary. however, saying that "chains correspond to cliques, therefore chains should use arbitrary elements" is a non-argument to me because chains don't correspond to cliques

[Christian Merten]

We don't use docs#Set.chainHeight anywhere I think. Andrew introduced it back in 2022 to do heights of ideals in commutative algebra, but since then we got docs#Order.height and when all of Andrew's height theory was ported to Lean4, it got all converted to docs#Order.height.

[Andrew Yang]

I think we should either remove docs#Set.chainHeight or redefine it via docs#Order.height (my opinion without reading what happened above).

[Bhavik Mehta]

Edward van de Meent said:

indeed if it's arbitrary. however, saying that "chains correspond to cliques, therefore chains should use arbitrary elements" is a non-argument to me because chains don't correspond to cliques

Note that docs#IsChain is arbitrary, and so it does correspond to clique.

[Edward van de Meent]

this (to me) is just a consequence of there not being another way to define "IsChain" on sets, and not because this is the ideal version of what it means to be a chain.

[Bhavik Mehta]

I'm not really sure what you mean, the definition of chain is between arbitrary elements: https://en.wikipedia.org/wiki/Total_order#Chains

[Edward van de Meent]

it's the definition that makes sense for transitive relations.

[Vlad Tsyrklevich]

Bhavik Mehta said:

It's not clear to me that the types version is better than the sets version here, it might be reasonable to have both? Note that docs#IsChain is for sets, and many order-theoretic things are in general.

I should play with it more--I think the difficulty I found is that by stating the definition purely in terms of sets working with RelHom/RelEmbedding/RelIsos becomes more difficult. Proofs that were trivial in the typed version become a bit of a quagmire since you can't escape to Types to e.g. deal with some coercions. Most of theory goes through just fine and mostly the exact same proofs, I was just wary of the few that became more difficult

[Christian Merten]

To repeat what I already said above:

• We should define a general inductive type Path that is identical to docs#Quiver.Path, but instead of taking a typeclass argument Quiver V, it should take a general relation r : V -> V -> Sort*.
• Then we redefine docs#RelSeries to be

structure RelSeries (r : X -> X -> Sort*) where
  head : X
  last : X
  path : Path r head last

• We define Rel.height in the same way as docs#Order.height, but taking an explicit r : X -> X -> Sort* argument.

[Vlad Tsyrklevich]

Edward van de Meent said:

it's the definition that makes sense for transitive relations.

I think that's a valid point, chains are usually discussed for transitive relations. It's unfortunate that IsChain/List.IsChain differ in meaning here, but I was working under the idea that chains specify total orders, so the natural definition for non-transitive relations is that everything is comparable.

[Christian Merten]

Finally, we can

• deprecate docs#Set.chainHeight
• define docs#Quiver.Path and docs#SimpleGraph.Walk as specializations of Path
• naturally define relative heights (i.e. between two terms x y : X) to be the suprema of lengths of Paths between x and y

[Bhavik Mehta]

Christian Merten said:

Finally, we can

• deprecate docs#Set.chainHeight

The issue I have with this is that the height of a chain is a useful notion in order theory, and either RelSeries formulation of it is super awkward for order theory.

[Edward van de Meent]

i almost completely agree with Christian's opinion, with the technical exception that i think it should be for r : V -> V -> Type* because of unification issues between Sort (max m (n + 1)) and Type w, and when you need it for Prop you use PLift

[Edward van de Meent]

in particular, having Path r head last : Type u always unify allows us to make use of a bunch of useful notation.

[Edward van de Meent]

(like appending and such)

[Christian Merten]

Bhavik Mehta said:

The issue I have with this is that the height of a chain is a useful notion in order theory, and either RelSeries formulation of it is super awkward for order theory.

I don't understand this, we don't use docs#Set.chainHeight currently. Do you mean that we should still have a notion of "maximal height in a set" notion? This could just be defined in terms of Rel.height of the set coerced to a type.

[Vlad Tsyrklevich]

Wouldn't this limit it to Finsets? Or rather, wouldn't it limit it to finite chains.

[Christian Merten]

Edward van de Meent said:

i almost completely agree with Christian's opinion, with the technical exception that i think it should be for r : V -> V -> Type* because of unification issues between Sort (max m (n + 1)) and Type w, and when you need it for Prop you use PLift

Using PLift would be quite annoying I think? (Note, still the most used case will be the one of orders).

[Edward van de Meent]

true, but i imagine that we can have a facade to hide the API behind, making it much more usable i think

[Bhavik Mehta]

Christian Merten said:

I don't understand this, we don't use docs#Set.chainHeight currently.

Sure, but we do want a notion of chain height of a poset, the notion shows up fairly often but just isn't in mathlib in a nice form yet. And Vlad's proof of Dilworth is a good opportunity to get it in.

Christian Merten said:

This could just be defined in terms of Rel.height of the set coerced to a type.

Right, but the inductive definition is really annoying to use in order theory, and limits us to finiteness as well as transitivity

[Christian Merten]

@Edward van de Meent Can you point to a unification problem that is not related to notation?

[Edward van de Meent]

not at the moment... but i don't think this is an irrelevant consideration. this has also been a consideration for the category theory library, i believe?

[Edward van de Meent]

i.e. Quiver.Hom : C -> C -> Type w rather than C -> C -> Sort w

[Christian Merten]

Bhavik Mehta said:

Right, but the inductive definition is really annoying to use in order theory, and limits us to finiteness as well as transitivity

Sorry, why does it limit us to finiteness? Are you saying docs#Set.chainHeight is not equal to docs#Order.krullDim of the coerced set?

[Andrew Yang]

I guess you cannot say that the height is some arbitrary ordinal (which you cannot with Order.krullDim either)

[Bhavik Mehta]

Cardinal, but yeah

[Bhavik Mehta]

Christian Merten said:

Edward van de Meent said:

i almost completely agree with Christian's opinion, with the technical exception that i think it should be for r : V -> V -> Type* because of unification issues between Sort (max m (n + 1)) and Type w, and when you need it for Prop you use PLift

Using PLift would be quite annoying I think? (Note, still the most used case will be the one of orders).

Yeah, and the simple graph case would also need PLift

[Bhavik Mehta]

I think there's a middle ground here, which is adopting Vlad and Christian's plans, except not removing Set.chainHeight. Then we can show that both heights are the same, and it's valuable to have both since the inductive vs Set formulations seem genuinely both useful

[Andrew Yang]

The current Set.chainHeight is also an inductive definition as it is the supremum of all monotone lists.

[Bhavik Mehta]

Sorry I should have been clearer: Vlad's plan includes changing that to use docs#IsChain, so it wouldn't be inductive any more

[Christian Merten]

I was missing this piece of information, now I understand and agree that we should have both notions.

[Vlad Tsyrklevich]

Also I just realized that though the current definition of Set.chainHeight has been stated in terms of LT as an arbitrary relation it is not well-defined for arbitrary relations. For example with the relation that is always true, the chain height of a singleton is infinite because there is an infinitely long list forming a chain, but this doesn't match my intuition about what a chain is.

import Mathlib.Order.Height
import Mathlib.Tactic.ENatToNat

theorem not_well_defined {α : Type*} [N : Nonempty α] : True := by
  let : LT α := { lt := fun _ _ ↦ True}
  have ⟨x⟩ := N
  have : ({x} : Set α).chainHeight = ⊤ := by
    simp [Set.chainHeight]
    refine ENat.eq_top_iff_forall_gt.mpr fun n ↦ ?_
    refine lt_biSup_iff.mpr ?_
    use List.replicate (n + 1) x
    constructor
    · simp [Set.subchain]
      induction n
      · simp
      · rename_i n ih
        exact List.isChain_replicate_of_rel (n + 1 + 1) trivial
    · enat_to_nat
      grind
  sorry

To be fair the doc comment does say the definition is for chain heights in a preorder, but it's been stated using LT since at least the port from mathlib3.