RelIso.cof_eq

Stream: mathlib4

[Violeta Hernández]

We have two different definitions of cofinality, one for reflexive orders docs#Order.cof, and one for irreflexive orders docs#StrictOrder.cof. I'm not really sure that these names were the best choice, since it's unclear how to disambiguate between them in other theorem names.

[Violeta Hernández]

Particularly, I wanted to introduce a version of docs#RelIso.cof_eq for StrictOrder.cof, but I don't know how to call it.

[Violeta Hernández]

In fact, I suspect this might be somewhat of an X/Y, since I'm not even confident docs#StrictOrder.cof is correct as a definition in general. Going by the Wikipedia article, the cofinality of the partial order Unit ⊕ Unit (with respect to the ≤ order) should be 2, while this definition (with respect to the < order) would give 1. Order.cof (· ≤ ·) and StrictOrder.cof (· < ·) only coincide for linear orders.

[Violeta Hernández]

any thoughts?

[Violeta Hernández]

@Yaël Dillies @Nir Paz

[Yaël Dillies]

Do we even need the two definitions?

[Violeta Hernández]

I don't think we really use either of them at the moment, other than to define docs#Ordinal.cof which is what our current API actually talks about

[Violeta Hernández]

And it'd be trivial to redefine that to use Order.cof rather than StrictOrder.cof by inlining the definition

[Yaël Dillies]

Can we get rid of both and only use Ordinal.cof?

[Nir Paz]

Yaël Dillies said:

Can we get rid of both and only use Ordinal.cof?

There are areas in set theory that heavily use cofinalities of partial orders (the reflexive order one above).

[Violeta Hernández]

Yep, PCF theory is one of them, isn't it?

[Violeta Hernández]

I think getting rid of StrictOrder.cof should be fine

[Violeta Hernández]

But it'd be nice to generalize the Ordinal.cof API to general (partial/linear/well) orders whenever possible

[Nir Paz]

I was actually looking at StrictOrder.cof a few days ago and left a bit confused by the definition haha. I've never heard something like it being used

[Nir Paz]

Violeta Hernández said:

Yep, PCF theory is one of them, isn't it?

Yea. It also uses other notions of cofinality (like true cofinality), but it's nice one of them already exists.

[Yaël Dillies]

Nir Paz said:

I was actually looking at StrictOrder.cof a few days ago and left a bit confused by the definition haha. I've never heard something like it being used

Sounds like a no-brainer then :smiley: :point_right: :wastebasket:

[Violeta Hernández]

#18043

[Violeta Hernández]

Added a small dependent PR to avoid golfing the same theorems twice

[Violeta Hernández]

There's actually quite a few changes I want to implement within the cofinality file, so I'll use this thread to list them:

• Deprecate StrictOrder.cof (as discussed)
• Redefine Order.cof for a preorder, rather than an unbundled relation.
• Define a Set.Cofinal predicate (this is equivalent to not BddAbove for linear orders, but not for partial orders)
• Generalize various results from Order.cof to general well/linear/partial orders
• Get rid of Bounded and Unbounded