Singular cardinals

Stream: mathlib4

[Nir Paz]

I've been thinking about defining Cardinal.IsSingular for infinite non regular cardinals. On the one hand it might force require transitioning between IsRegular and IsSingular now and then which is a little extra step, but on the other hand ℵ₀ ≤ κ ∧ ¬(IsRegular κ) is a common assumption that's nasty to state.

@Violeta Hernández

[Violeta Hernández]

I don't know, I don't see how using "not is regular" is particularly nasty

[Violeta Hernández]

Also, we rarely ever have predicates for both a property and its negation. The one exception I can think of is odd and even numbers.

[Daniel Weber]

Another example is IsTranscendental and IsAlgebraic

[Violeta Hernández]

Actually, IsRegular and IsSingular wouldn't be strict antonyms. From what I understand, the convention is that finite cardinals are neither.

[Violeta Hernández]

I fear we might run into yet another IsSuccLimit / IsSuccPrelimit situation, though, where sometimes we care about the extra ℵ₀ ≤ c assumption, and sometimes we don't.

[Violeta Hernández]

@Nir Paz What kind of results do you want to state on regular/singular cardinals? Do they require this infinitude assumption?

[Nir Paz]

Violeta Hernández said:

Nir Paz What kind of results do you want to state on regular/singular cardinals? Do they require this infinitude assumption?

Mostly results about the behaviour of the continuum/power function at singular cardinals. Because of Easton's theorem there are only interesting results for singulars, and I will always assume they are infinite. Stuff like GCH can't break for the first time on a singular with uncountable cofinality, bounds on powers of singulars based on powers below them, etc.

[Violeta Hernández]

Well, I've got no idea how many of these results will generalize to finite cardinals, but in any case they're probably not very interesting for finite cardinals anyways.

[Nir Paz]

Violeta Hernández said:

Well, I've got no idea how many of these results will generalize to finite cardinals, but in any case they're probably not very interesting for finite cardinals anyways.

I usually forget they exist.

[Violeta Hernández]

Skimming through the PCF article on Wikipedia it is pretty clear that only singular cardinal exponentiation is interesting. So I now support making IsSingular into a definition.

[Violeta Hernández]

We could define it as

def IsSingular (c : Cardinal) : Prop :=
  ℵ₀ ≤ c ∧ ¬ c.IsRegular

Then every cardinal is exactly one of three: finite, singular, or regular.

[Nir Paz]

Violeta Hernández said:

Skimming through the PCF article on Wikipedia it is pretty clear that only singular cardinal exponentiation is interesting. So I now support making IsSingular into a definition.

Then I'll put a pin on a couple of PRs that could be better stated with IsSingular and make a PR for that first.

[Nir Paz]

Do you think this might be a good excuse to add a new file, something like Cardinal/Singular.lean? Nothing that already exists can really be better stated with it, so it could be nice to add it as an end extension of the existing set theory library.

[Nir Paz]

Even if the whole files won't be specifically about singulars, it's better than MoreArithmetic.lean, which is really what we need.

[Violeta Hernández]

I think we could split the cofinality file, so that stuff about regular cardinals (and maybe strong limit / inaccessible cardinals too?) is in this new file as well.

[Violeta Hernández]

Actually, docs#Cardinal.IsStrongLimit could probably go on the Basic file, there's no reason to wait until cofinality to define it.

[Violeta Hernández]

Inaccessible cardinals can definitely go at the end of the singular/regular file. We barely prove anything about them anyways, besides the fact that they exist :stuck_out_tongue:

[Nir Paz]

#17005

This has the definition and some lemmas in a new file. You can split the cofinality file in that branch if you want, or I'll do it when I can (but I'm going to be a bit busy next week).

[Violeta Hernández]

I think it might be best to do the split and adding new content in different PRs.