Cofinal sets

Stream: maths

[Violeta Hernández]

I wanted to introduce a predicate for cofinal sets, so I opened #18214 with some basic API. I was then informed that docs#Order.Cofinal already exists, though this is for the type of cofinal sets, rather than being just a predicate.

Does it make sense to have both? Or should one be used in favor of the other?

[Violeta Hernández]

@Yaël Dillies @Nir Paz

[Violeta Hernández]

To give a few examples of the API I want for cofinal sets:

• the empty set is cofinal iff the type is empty - gives a very short proof of cof o = 0 ↔ o = 0
• a set in an OrderTop is cofinal iff it contains ⊤ - should allow a similarly short proof of cof o = 1 ↔ o ∈ range succ`
• if f and g form a galois connection and s is cofinal, so is g '' s - this gives a very quick proof that relation isomorphisms preserve cofinality

[Violeta Hernández]

I feel like all of these would be somewhat awkward to state with the type approach.

[Antoine Chambert-Loir]

There's an ambiguity in cofinality that it can be defined as a cardinal (for sets in a preordered type) or as an ordinal (for sets in a well-ordered type). For well-ordered types, both approaches concur in the end, but the definition as an ordinal says something slightly stronger.

[Nir Paz]

Is it common in mathlib to have both a structure and a predicate? Seems bad for scaling. If we choose one, I'm definitely in favor of a predicate since otherwise like you say it's clumsy to state a theorem that a set is cofinal, which is pretty common

[Violeta Hernández]

Antoine Chambert-Loir said:

There's an ambiguity in cofinality that it can be defined as a cardinal (for sets in a preordered type) or as an ordinal (for sets in a well-ordered type). For well-ordered types, both approaches concur in the end, but the definition as an ordinal says something slightly stronger.

I think it's fine to just have the cardinality definition, as the cofinality definition is easy to state as a theorem afterwards

[Violeta Hernández]

In the current API that would be docs#Ordinal.ord_cof_eq

[Violeta Hernández]

Nir Paz said:

Is it common in mathlib to have both a structure and a predicate? Seems bad for scaling. If we choose one, I'm definitely in favor of a predicate since otherwise like you say it's clumsy to state a theorem that a set is cofinal, which is pretty common

I recall I've seen a few other structures like these around the order library, but I can't find any for the moment.

[Violeta Hernández]

I think it's fine to have both the predicate and the type, since there is at least one property of the type we care about: it's nonempty

[Violeta Hernández]

I'd rather have it just be a subtype so we could use e.g. docs#Subtype.forall, but maybe there's a good reason for not doing that

[Violeta Hernández]

Talking about the type, would it make sense to rename it to Cofinals?

And also, should the predicate Cofinal be in the Order namespace?

[Violeta Hernández]

Another question: is it a big deal to lose the def-eq (type r).cof = Order.cof r?

[Violeta Hernández]

With my planned redefinition of Order.cof in terms of a preorder, I can still guarantee (type α (· < ·)).cof = Order.cof α, but since LinearOrder is data-carrying I sadly can't make that a def-eq

[Violeta Hernández]

I've thought about this a bit. I think we can have both the predicate IsCofinal and the type Cofinal, in analogy to e.g. docs#IsUpperSet vs docs#UpperSet

[Yaël Dillies]

Yes, but what's the use case of the structure?

[Violeta Hernández]

I'm not sure I can answer that, but looking at the API for the existing docs#Order.Cofinal e.g. docs#Order.idealOfCofinals, a lot of these theorems seem more natural to state using the type

[Violeta Hernández]

It's also used a bit in model theory it seems, e.g. docs#Order.PartialIso.definedAtLeft

[Violeta Hernández]

Maybe it's best to ask the author @Gabin Kolly

[Violeta Hernández]

Also, just found this two-month old convo where you also argue for Cofinal to be a predicate: https://github.com/leanprover-community/mathlib4/pull/11177/files#r1715176361

[Violeta Hernández]

Honestly, I don't see an issue with having both the predicate and the type. In any case, we can probably benefit from having the type by defining the cofinality of a type α as ⨅ s : Cofinal α, #s.carrier and making use of the Nonempty instance on Cofinal α.

[Violeta Hernández]

A more pressing issue: is it ok for docs#Order.Cofinal to be in the Order namespace? It makes sense, but other order-related types/predicates like the aforementioned docs#UpperSet are in the root namespace instead.

[Violeta Hernández]

Is there anyone else currently working on model theory I could ask for comment?

[David Wärn]

IIRC docs#Order.Cofinal was defined a long time ago for the Rasiowa--Sikorsi lemma docs#Order.idealOfCofinals and the related docs#Order.iso_of_countable_dense. This has since been generalised to docs#FirstOrder.Language.equiv_between_cg. These seem to be the only uses of Order.Cofinal? For these purposes it was convenient to use the structure, but I guess one would also like to have the property

[Antoine Chambert-Loir]

About the namespaces, I note that docs#Order.Cofinal requires docs#Preorder while docs#UpperSet is content with docs#LE. The namespaces can help disambiguate, which seems unnecessary here, and to allow for dot notation, which is neither the case here, because orders are usually given at the level of typeclasses. For algebraic structures, the namespace seems to refer either to the morphisms (docs#Function, docs#AlgHom…) or predicates. All in all, this suggests for suppressing the namespace here.

[Gabin Kolly]

So as the author of FirstOrder.Language.equiv_between_cg, I don't think using a property instead of a structure would change a lot, and the proof can be easily adapted to use the predicate.

[Violeta Hernández]

I can leave this refactor as a TODO within my own PR

[Violeta Hernández]

Would we also need to refactor docs#Order.Ideal in this way?

[Gabin Kolly]

In the proof, I use docs#Order.sequenceOfCofinals which is in docs#Order.Ideal, so it would need to be refactored as well.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I'm confused on what to do with docs#Order.Cofinal.

[Violeta Hernández]

I think it makes sense to keep docs#Order.Ideal and docs#Order.PFilter as structures rather than predicates, if only to match docs#Filter. But under that logic, refactoring docs#Cofinal would make the Order.Ideal file inconsistent.

[Violeta Hernández]

For the moment I've opened #19681, which redefines Cofinal in terms of IsCofinal.

[Violeta Hernández]

Not quite the original thread topic, but you might be interested in knowing I'm doing a very large refactor on the cofinality API: #19698

[Violeta Hernández]

This is meant to solve two major problems with the current API:

• Defining docs#Order.cof in terms of an unbundled relation rather than a linear order is pretty inconvenient, most notably not allowing us to easily link together cofinality to cofinal sets.
• A lot of theorems are written in terms of lsub, blsub, etc. which are in process of being deprecated.
• (and also, a lot of the current proofs are a mess)

[Violeta Hernández]

@Nir Paz

[Nir Paz]

Defining cofinality for relation really does seem like redundant generality, preorders are what I would think is the most general use case, so no objections!

Could you clearify how this will help the lsub-and-friends problem? Do you just mean this gives you an opportunity to refactor them out of a lot of places?

[Violeta Hernández]

Oh yeah, I'm really just taking the opportunity to refactor everything at once.

[Violeta Hernández]

Otherwise I end up duplicating work, e.g. if I redefine Order.cof I have to reprove all of the lsub theorems and such, and then I have to get rid of them!

[Violeta Hernández]

(deleted)

[Violeta Hernández]

The refactor is almost done! I'm just missing some minor theorems on nfpFamily, plus some not so minor results about the infinite pigeonhole principle

[Violeta Hernández]

What exactly is the infinite pigeonhole principle in this context?

[Violeta Hernández]

The version I learned simply states "given finitely many holes and infinitely many pigeons, some hole contains infinitely many pigeons"

[Violeta Hernández]

I'm having a hard time parsing the version on Mathlib: docs#Ordinal.infinite_pigeonhole

[Violeta Hernández]

Given infinitely many pigeons b, and less holes than the cofinality of b, some hole has b pigeons?

[Violeta Hernández]

That makes sense actually

[Violeta Hernández]

In other words, if x is a cardinal with cofinality y, the sum / supremum of < y cardinals less than x is also less than x