feat: cofinality within order

[vihdzp]

We introduce Order.cofWithin x = Order.cof (Iio x) for the cofinality of an element within a preorder. This generalizes Ordinal.cof, with the caveat that cof o : Cardinal.{u} for o : Ordinal.{u}, whereas cofWithin o : Cardinal.{u + 1}.

---

[github-actions]

PR summary f543a8738e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsSuccLimit.cofWithin_ne_one
+ IsSuccLimit.one_lt_cofWithin
+ IsSuccPrelimit.cofWithin_ne_one
+ _root_.Order.cofWithin_ordinal
+ aleph0_le_cofWithin_iff
+ cofWithin
+ cofWithin_bot
+ cofWithin_eq_one_iff
+ cofWithin_eq_zero_iff
+ cofWithin_le
+ cofWithin_le_one_iff
+ cofWithin_lt_aleph0_iff
+ cofWithin_ne_one_iff
+ cofWithin_succ
+ cofWithin_succ_of_not_isMax
+ cof_Iio
+ cof_typein
+ mk_preimage_val_le_left
+ mk_preimage_val_le_right
+ one_lt_cofWithin_iff
- _root_.Order.cof_Iio

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[YaelDillies]

What's your use case?

[vihdzp]

I want to prove the following theorem: for any well-order α of uncountable cofinality, for any c < cof α, the set of elements with cofWithin equal to c is stationary.

More generally, this cofWithin function is used within various proofs about club/stationary sets. I believe Solovay splitting is another example, on which I'm currently working on.

[YaelDillies]

Does this appear in the literature? If so, can you add a reference?

[vihdzp]

It appears implicitly in the set theory literature. Set theorists generally identify a cardinal with an ordinal with a well-order, and under this identification Order.cofWithin is just the Ordinal.cof function (i.e. I need this new predicate to spell what they would just write as $\textrm{cf}$).

[YaelDillies]

Do you mean that you want to talk about cofWithin (c : Cardinal)? Can you add some lemmas to this PR as examples?

[vihdzp]

I'll give a more detailed example of what I want to do. In page 94 of Jech's Set Theory he defines, for a regular uncountable cardinal $\kappa$ and for $\lambda < \kappa$, the set

$$E_\lambda^\kappa = \{\alpha < \kappa : \mathop{\textrm{cf}}(\alpha) = \lambda\}$$

and claims that it is stationary in $\kappa$. The literal Lean translation of this would make use of κ.ord.ToType or perhaps Iio κ.ord. But it serves to instead abstract this result to any well-order with order type κ.ord (in fact, a version of this result is true for any well-order of uncountable cofinality). After we do this, what we previously wrote as $\textrm{cf}(\alpha)$ is now more properly the cofinality of Iio α.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[b-mehta]

I'm not convinced of the motivation here - we already have two ways of writing this, and your new version is less convenient since it has a universe bump! It seems to me that instead of writing cofWithin x, we may as well write cof (Iio x) if you want to allow the universe bump (as you seem to do here).

Also, your use-case is a generalisation of a notion used only occasionally in Jech.

I also notice that your PR deprecates a theorem which was added in a PR just 2 and a half months ago, so I worry that some of the notions in this part of the library are going through churn at such a rate that suggests that some of these notions and design decisions should instead be allowed to stabilise in a downstream repo before being upstreamed.

I will add that if you make a separate PR for the changes in Mathlib/SetTheory/Cardinal/Basic.lean, then I'd be very happy to merge that.

[vihdzp]

The idea is that we'd be using cofWithin in orders other than the ordinals, in which we don't get a universe bump. I could just write cof (Iio x) everywhere, but that feels a bit clunky to me. I could also write cof (typein (· < ·) x), but now we have two different spellings, neither canonical. Hence the new definition.

I do ultimately need some API on this notion in order to prove the result from Jech, regardless of how we write it down. The main theorem I need is that if α has no maximum and f : α → β is strictly monotone, then cofWithin (⨆ i : α, f i) = cof α. This result exists on ordinals as Ordinal.cof_iSup, but it's not exclusive to them.

[b-mehta]

I still don't think this PR is worth it - cof (Iio _) is shorter. I agree you need API on this notion, but that can just be new lemmas, we gain very little from making this special case of cof.

[ocfnash]

I haven't read the discussion but I've removed the maintainer-merge label since Bhavik is not convinced about this PR. If this changes, then of course the label can be reapplied.