regular cardinals

Stream: maths

[Reid Barton]

@Mario Carneiro I want to show that if $\kappa$ is a regular cardinal, then the sum of fewer than $\kappa$ cardinals smaller than $\kappa$ is less than $\kappa$. Is there an easy way to do this from what's already there about regular cardinals?

[Mario Carneiro]

@Reid Barton added

[Kevin Buzzard]

@Mario Carneiro I want to show that if $\kappa$ is a regular cardinal, then the sum of fewer than $\kappa$ cardinals smaller than $\kappa$ is less than $\kappa$. Is there an easy way to do this from what's already there about regular cardinals?

yeah, you can ask Mario to do it

[Kenny Lau]

Do strong inaccessible cardinals exist in Lean?

[Mario Carneiro]

The answer was basically "yes, once you prove a few more basic facts"

[Kevin Buzzard]

That's not even right because that's not what you did -- you can mention it when Mario is within earshot is what I meant to say

[Kevin Buzzard]

How close is Type 1 from being one of these large cardinals?

[Kevin Buzzard]

If alpha is a type, is homs from alpha to bool still the same type? No, we went up a level in the universe hierarchy, right?

[Kenny Lau]

It's still the same type. Grothendieck universe is closed under power set

[Mario Carneiro]

@Kenny Lau yes, is_inacessible means strongly inaccessible

[Mario Carneiro]

@Kevin Buzzard Yes, univ_inaccessible asserts that a universe cardinal is inaccessible

[Kenny Lau]

/- Lean's foundations prove the existence of ω many inaccessible
   cardinals -/
theorem univ_inaccessible : is_inaccessible (univ.{u v}) :=
is_inaccessible.mk
  (by simpa using lift_lt_univ' omega)
  (by simp)
  (λ c h, begin
    rcases lt_univ'.1 h with ⟨c, rfl⟩,
    rw ← lift_two_power.{u (max (u+1) v)},
    apply lift_lt_univ'
  end)

[Kenny Lau]

cool!

[Kevin Buzzard]

I never remember the difference between all these large cardinal axioms and I've never thought about how they interact with type theory either. I'm not sure that "normal mathematicians" care about them (in set theory or in type theory).

[Kevin Buzzard]

(by which I mean geometers topologists analysts number theorists algebraists etc)

[Reid Barton]

Thanks Mario! I see you also added a bunch of other statements that I was looking for while trying to figure out how to prove this.
I'm really grateful that so much cardinal arithmetic is already in mathlib--if I hadn't seen that we already had regular cardinals I probably wouldn't have started down this road towards locally presentable categories.

[Reid Barton]

Kevin I've only ever needed regular and inaccessible cardinals. Regular cardinals are just what I wrote above, the union of a small family of small sets is again small, where "small" means cardinality $< \kappa$. It's useful for controlling a construction by transfinite induction up to $\kappa$. If we replace $< \kappa$ with $\le \kappa$ then this condition would automatically be satisfied, so every successor cardinal is regular. So regularity is not really a "largeness" condition but rather a way to rule out certain cardinals we don't like, the first example being $\aleph_\omega = \aleph_0 + \aleph_1 + \aleph_2 + \cdots$.

Inaccessible cardinals also have the same property with "product" in place of "union", and they are the cardinalities of Grothendieck universes, so you could say they bound the cardinality of any construction.

[Reid Barton]

By the way, is it intentional that cardinal.mk is not protected? I don't really mind at the moment, but it is a little odd to see just mk in my goals. If there's going to be a non-protected name for taking the cardinality of a type, maybe something like card would be better.
(I think this came up earlier, when people were looking for functions named mk which were not protected, for some reason.)

[Kevin Buzzard]

I think I once grepped through all of mathlib looking for unprotected mks and that was the only one, and at the time people said it was an error but I didn't know enough about how PR's etc worked to be able to fix it.

[Kevin Buzzard]

That's not true, it was another function not mk. I can't find the thread now though; might have been on gitter.

[Kevin Buzzard]

Why do you need it? I used to think this stuff was really cool when I was a graduate student but then I realised that it never seems to actually be any use in my area

[Kevin Buzzard]

[phone posting stuff three times]

[Reid Barton]

One place you need the notion of regular cardinal is in the small object argument, which is a generalization of the kind of argument where you approximate a space $X$ by building up a cell complex where at each stage, you attach a cell $\partial D^n \to D^n$ for every way to map $\partial D^n$ to your complex so far and every way to extend it to a map $D^n \to X$. More generally, we could do this for any set of "cell" maps in any (let's say cocomplete) category. We're going to repeat this $\kappa$ times and in the end, we're going to want to know that any map from the domain of one of our cell maps to the end result factors through the thing we produced at stage $\alpha$ for some $\alpha < \kappa$.

[Reid Barton]

To conclude this, we need two things.

• The domains of the cell maps are $\kappa$-presentable, so homs out of them commute with $\kappa$-filtered colimits. This is a kind of smallness condition. For example, if a set $S$ has cardinality less than $\kappa$, then a map from $S$ into a $\kappa$-filtered colimit factors through some object in the colimit.
• The ordered set of ordinals less than $\kappa$ is $\kappa$-filtered -- this is saying that $\kappa$ is a regular cardinal.

[Reid Barton]

Why do we need actual regular cardinals bigger than $\omega$? Probably hard to give an example off-hand.

[Kevin Buzzard]

I see. Thanks. So I guess even using transfinite induction is somehow beyond what I ever seen in practice in my area. Do you only need transfinite induction because you're trying to work with random categories?

[Reid Barton]

No, there are actual "applied" settings like constructing localizations with respect to homology theories, where it's not easy to bound the cardinals that show up, or at least the ones which appear are bigger than $\omega$.

[Kevin Buzzard]

Wow, that is what topology has become?

[Reid Barton]

Homotopy theorists study spaces one prime at a time, didn't you know? :)

[Kevin Buzzard]

So are there actual set-theoretic problems if you try to set this stuff up in ZFC? (in the sense that you can't actually do it?)

[Reid Barton]

No, because there's lots of regular cardinals.

[Kevin Buzzard]

Oh so you only need regular, not some crazy inaccessibles.

[Reid Barton]

Yes. You could probably get by without explicitly using the notion and just taking successor cardinals in various places, but it's nicer to keep track of what you actually need.

[Reid Barton]

That said, it is of course nice to set up the theory to work with "random" categories, or at least ones which are controlled in some sense by an arbitrary regular cardinal $\kappa$ (these are the locally presentable categories), and so you end up with this regular cardinal assumption baked in from the start. I'm expecting to find out exactly where it is and isn't used :)

[Reid Barton]

In fact it would do no real damage to the theory to just replace "regular cardinal" by "successor cardinal" everywhere, particularly in view of the fact that any limit cardinal that you can "write down" (like $\aleph_\omega$) cannot be regular. The point is just that "regular cardinal" (sum of fewer than $\kappa$ cardinals below $\kappa$ is smaller than $\kappa$) is the actual property you need to make the theory work.

[Mario Carneiro]

I'm worried that this is not the usual way we handle "size issues" in lean. Do you have an example where replacing kappa-somethings with somethings everywhere causes problems?

[Reid Barton]

So one of the themes in this area is that we have certain constructions in which we'd like to form large (co)limits and/or do transfinite induction over all ordinals. We cannot do these constructions in ZFC and so we prove somewhat complicated theorems to show that we can replace the needed (co)limits/transfinite inductions by small ones. But, even if we assume the existence of universes so that we could perform the construction in a higher universe, we would still want to know that the resulting object belongs to the original universe when it does.

[Mario Carneiro]

Right, in type theory the "size issue" manifests as making sure your construction is still in Type u given that your inputs are in Type u

[Mario Carneiro]

But we don't do transfinite induction very often in type theory; the substitute is the use of a complicated inductive type

[Mario Carneiro]

which is why I think having a regular cardinal may not be as useful as you think

[Reid Barton]

Maybe the simplest example would be something like this. If you have a poset with least upper bounds for any subset, then it has a maximum element which you can obtain by taking the least upper bound of everything. But in category theory, we cannot obtain a terminal object in Set by taking the colimit of the identity diagram Set -> Set. I mean it is the colimit, but we do not know a priori that it exists because we only know that we can form colimits of small diagrams and Set itself is a large category.

[Mario Carneiro]

Right, we can only take a colimit of a type in Type u

[Mario Carneiro]

but where do regular cardinals enter the picture?

[Reid Barton]

So, (obviously this is way overkill for this particular problem but) you can pick a regular cardinal $\kappa$, define what it means for a set to be "$\kappa$-compact" (in this case just that its cardinality is less than $\kappa$), show there is only a set of isomorphism classes of $\kappa$-compact sets (in this case, all the cardinalities less than $\kappa$), and pick one member from each class and form the full subcategory on those and form the colimit of that small diagram. Then you do more work to show that the colimit is a terminal object not just as seen by $\kappa$-compact sets, but as seen by every set.

[Reid Barton]

This also works in the category of models of any algebraic theory--here $\kappa$ has to be chosen larger than the arity of any operation in the theory

[Reid Barton]

I agree that the kinds of constructions that you can do in Set by this method overlap with what you can do directly with inductive types in type theory. In this language the fact that you can form the initial fixed point of a strictly positive functor comes down to the fact that it preserves $\kappa$-filtered colimits for some $\kappa$ (which has to be bigger than the cardinalities of any types which appear as "exponents" in the functor)

[Reid Barton]

Then you can form the fixed point by transfinite composition up to $\kappa$ and the fact that the functor commutes with the $\kappa$-filtered colimit you just wrote down is what tells you that you got a fixed point.

[Reid Barton]

I don't see how this helps me if I want to do some arbitrary transfinite composition construction in the category of simplicial rings or whatever, though.

[Reid Barton]

I actually am very curious when I do get to transfinite composition constructions what you have to say about representing them in Lean, because it seems like the kind of thing that Lean would be good at in some non-obvious (to me) way.

[Mario Carneiro]

So, (obviously this is way overkill for this particular problem but) you can pick a regular cardinal $\kappa$, define what it means for a set to be "$\kappa$-compact" (in this case just that its cardinality is less than $\kappa$), show there is only a set of isomorphism classes of $\kappa$-compact sets (in this case, all the cardinalities less than $\kappa$), and pick one member from each class and form the full subcategory on those and form the colimit of that small diagram. Then you do more work to show that the colimit is a terminal object not just as seen by $\kappa$-compact sets, but as seen by every set.

Okay, so here is how I think you would do this in types: We know that we can take a colimit over any set (aka thing in Type u), or possibly any set satisfying some condition that is easy to satisfy. This substitutes for all the work up to the last sentence. Then we obtain an approximate colimit of Set, and we now need to show that there is some choice of type that makes the approximation a true colimit. This will require some particular "size argument" specific to the problem, but often involves constructing an inductive type larger than everything in sight

[Reid Barton]

A less trivial (but basically still the same) theorem is the adjoint functor theorem for locally presentable categories: any functor between locally presentable categories which preserves colimits has a right adjoint

[Reid Barton]

Right so the size argument is specific to the problem, but it's not specific to the choice of locally presentable category (in this case I picked Set, but it could have been Ring or whatever).

[Mario Carneiro]

what is a locally presentable category?

[Reid Barton]

And to make that size argument in general, you need to talk about cardinals

[Mario Carneiro]

You can talk about types instead

[Mario Carneiro]

of course types are cardinals of themselves

[Mario Carneiro]

so you can use type variables as proxies for cardinal numbers

[Reid Barton]

There are a bunch of equivalent formulations, but we can say that it's the category of models of an essentially algebraic theory (which means the operations might have equality preconditions, like the composition in a category).

[Reid Barton]

There's no restriction on the number or arity of the operations, except that everything involved must be a set

[Mario Carneiro]

that seems messy to work with

[Reid Barton]

Another one is: a category which is cocomplete and for some $\kappa$, it has a set of $\kappa$-compact objects which generate the whole category under $\kappa$-filtered colimits

[Mario Carneiro]

I'm reading that on nlab now, and now I need to figure out what $\kappa$-compact and $\kappa$-filtered colimit mean

[Reid Barton]

I can give you three equivalent definitions in Lean :)

[Reid Barton]

For $\kappa$-filtered categories, that is

[Reid Barton]

I guess it's kind of hard to explain how $\kappa$-filtered colimits arise except that they give a good theory of $\kappa$-compact objects.
If you want, you can substitute $\kappa$-directed which is a bit simpler technically.

[Mario Carneiro]

Maybe you can tell me what goes wrong if $\kappa$ is not a regular cardinal?

[Reid Barton]

Well it's no longer true that a $\kappa$-small colimit of $\kappa$-compact objects is $\kappa$-compact (because in Set, this is basically the fact I asked you for).

[Mario Carneiro]

Is there an inductive closure condition that would ensure this works?

[Reid Barton]

You might want to take a quick look at https://ncatlab.org/nlab/show/arity+class

[Reid Barton]

Actually, maybe I misunderstood but that page may be somehow relevant.

[Reid Barton]

I think you want to build up the class of $\kappa$-compact objects in some inductive fashion?

[Reid Barton]

Or, there is another description again of locally presentable categories.

[Mario Carneiro]

You start from some initial objects, and want to close it to a suitably large cardinal

[Reid Barton]

Start with $\kappa$ and a small category which admits $\kappa$-small colimits.

[Reid Barton]

Then, you can "freely adjoin" all $\kappa$-filtered colimits and this gives you a general locally $\kappa$-presentable category.

[Mario Carneiro]

Although I don't think "regular cardinal" is an inductive condition

[Reid Barton]

Actually in some of these cases, you can say exactly what goes wrong if you don't assume $\kappa$ is regular.
Typically you get the same notion as if you had replaced $\kappa$ by its cofinality.

[Reid Barton]

So, a regular cardinal $\kappa$ is really "standing in" for the class of all cardinals of cofinality $\kappa$, from this point of view

[Reid Barton]

But it's better to work only with regular ones, because for example a locally $\kappa$-presentable category is also locally $\lambda$-presentable for $\kappa \le \lambda$, but if you were to ignore the condition that $\lambda$ be regular, then it might no longer be true (because the cofinality of $\lambda$ could be less than $\kappa$).

[Reid Barton]

In the end, the point is really that it's a large class of categories in which you can do a large class of constructions in a uniform way (once you know this parameter $\kappa$).

[Reid Barton]

And a lot of the constructions involve this somewhat involved reasoning about cardinalities, so it's worth it to not have to do them more than once

[Reid Barton]

For example, the construction of free objects

[Reid Barton]

I guess one other point is that to build a free object as an inductive type, you need Lean to be able to see syntactically that the functor involved is strictly positive.

[Reid Barton]

But to do the same construction even in Set using this regular cardinal kind of machinery, you only have to prove a theorem about how it commutes with sufficiently highly filtered colimits

[Mario Carneiro]

I think there is usually a way to make this work by writing the functor differently

[Mario Carneiro]

I have no sense of how easy "you only have to prove a theorem about how it commutes with sufficiently highly filtered colimits" is

[Reid Barton]

Sure, but proving a theorem is more flexible than having to produce something that satisfies a judgment. And you can abstract over an accessible functor, but you can't abstract over a strictly positive type constructor.

[Mario Carneiro]

But you can usually write something that is obviously positive but not obviously the same as your functor

[Mario Carneiro]

and then the theorem is shifted to proving this equality

[Reid Barton]

Well it depends on what the functor is of course :)
For FX = X^S, proving that F commutes with $\kappa$-filtered colimits -- or we can take $\kappa$-directed colimits for simplicity -- is checking that if $I$ is a $\kappa$-directed poset and for each $s \in S$, we have an element in some $A_{i(s)}$, then we can map them all into some common $A_{i'}$ -- and this is the definition of $\kappa$-directed for $\kappa > |S|$.

[Reid Barton]

What if my functor is something like FX = the set of unordered pairs of elements of X?

[Reid Barton]

Anyways I think the ability to abstract over "an accessible functor" is the more interesting thing

[Reid Barton]

Just to give you a taste, in the theory of model categories all this machinery is used heavily. One of the most important ways to construct model categories is https://ncatlab.org/nlab/show/combinatorial+model+category#SmithTheorem and if you just look at the hypotheses it should give you some sense of how this stuff gets used. It's actually quite difficult to construct any interesting examples of model categories, so this is a major result.

[Reid Barton]

(My secret plan is to formalize the proof of this theorem.)