Singular homology and universes

Stream: mathlib4

[Sébastien Gouëzel]

Do I understand correctly that the current definition of singular homology in mathlib only makes sense for spaces in Type? Is there a roadmap to extend it to general universes, or is this completely barred by the way category theory works in mathlib?

[Andrew Yang]

According to #maths > Ext and Tor @ 💬, we might be able to extend that some time in the future.

[Sébastien Gouëzel]

And I had already asked the very same question in this thread! :-)

[Kevin Buzzard]

That's because it's a good question!

[Joël Riou]

The issue is with the realization functor from simplicial sets to topological spaces and its right adjoint, which are currently defined only for SSet.{0]. I have some code doing this extension; I will try to PR it soon.

[Kevin Buzzard]

I will make a provocative remark: I would say that we've all been brainwashed by universes and that people like Sébastien would never actually need to compute the homology of any space not in Type even if he were to formalize all his favourite theorems. The same might even be true of me -- although I have this uncomfortable feeling that it might be convenient to have the etale cohomology of a smooth projective variety over $\overline{\mathbb{Q}}$ to at least temporarily live in Type 1 and then Joël will apply his magic to descend it back into Type. I think that a lot depends on the exact moment at which one decides to invoke the set-theory witchcraft which does this.

The place where universes are convenient is in category theory, because otherwise we would have to develop different API for small and large categories. In fact I think that this is where our approach really yields benefits -- in ZFC (which of course historically came decades before category theory) you have to jump through certain hoops to make an adequate theory of categories in the generality in which algebraic geometers use it; in Lean this seems to me to be much cleaner.

[James E Hanson]

Kevin Buzzard said:

in ZFC (which of course historically came decades before category theory) you have to jump through certain hoops to make an adequate theory of categories in the generality in which algebraic geometers use it; in Lean this seems to me to be much cleaner.

Are you claiming that it's cleaner even relative to something like Tarski-Grothendieck set theory or just relative to ZFC with no additional assumption of the presence of universes?

[Kevin Buzzard]

It's cleaner relative to ZFC, I should think that Tarski-Grothendieck makes it as easy as it is in lean. In brief, every "classical" mathematical object like a group, ring, manifold etc in lean comes with an extra natural number parameter which is the universe level that it lives in. In contrast, a category comes with two natural numbers, the universe level of the type of all objects and the universe level of each of the morphism types Hom(X,Y). The definition of a small category that these two numbers are equal, the definition of a large category is that the object number is one bigger than the morphism number. The two theories are treated uniformly in mathlib and my guess is that this would be difficult to do in bare ZFC formally. Whenever one does something which would be described as "taking the limit over a class" in ZFC this just corresponds to adding 1 to the object number. I would strongly expect that Tarski-Grothendieck offered exactly the same simplifications (in fact Lean's type theory is equiconsistent with ZFC + some statement of the form "for all naturals n, there exists a chain of n universes").

[James E Hanson]

I see, thank you.

Incidentally, I think you have the equiconsistency statement slightly wrong, but to be fair it's a relatively subtle point. Lean's type theory is equiconsistent with $\mathsf{ZFC} + \{\text{"there are}~n~\text{inaccessible cardinals"} : n \in \mathbb{N}\}$. This is strictly weaker than $\mathsf{ZFC} + \text{"for every natural}~n\text{, there are}~n~\text{inaccessible cardinals"}$.

[Kevin Buzzard]

Yes I knew there was a subtlety here which I didn't understand properly hence the hedging with "some statement of the form". Thanks!

[Filippo A. E. Nuccio]

James E Hanson said:

I see, thank you.

Incidentally, I think you have the equiconsistency statement slightly wrong, but to be fair it's a relatively subtle point. Lean's type theory is equiconsistent with $\mathsf{ZFC} + \{\text{"there are}~n~\text{inaccessible cardinals"} : n \in \mathbb{N}\}$. This is strictly weaker than $\mathsf{ZFC} + \text{"for every natural}~n\text{, there are}~n~\text{inaccessible cardinals"}$.

I confess my ignorance in Set Theory, can you briefly point at the difference between the two statements?

[Mario Carneiro]

The latter statement is equivalent to "there are $\omega$ inaccessible cardinals", and in particular means that you can construct a set containing $\omega$ inaccessible cardinals. The former statement lets you construct sets containing any finite number $n$ of inaccessibles but the proofs grow with $n$ and there is no proof of all of them living together

[James E Hanson]

Filippo A. E. Nuccio said:

I confess my ignorance in Set Theory, can you briefly point at the difference between the two statements?

Yeah part of the subtlety here is that any standard model of the first theory is also a model of the second theory, so it's hard to imagine them being different.

It might be easier to think about it like this: Consistency of Lean is equivalent to the statement

For each $n$, $\mathsf{ZFC} + \text{``there are at least}~n~\text{inaccessible cardinals''}$ is consistent.

This is strictly weaker than the statement

$\mathsf{ZFC} + \text{``there are infinitely many inaccessible cardinals"}$ is consistent.

I think this makes it a little more intuitive why they could be different.

[Kevin Buzzard]

@Filippo A. E. Nuccio all this sounds like the same reason induction is an axiom. If you know p(0) and that p(d) implies p(d+1) then for any given n you can prove p(n) but as n gets bigger your proofs get longer, and a proof has to be finite, so it's not clear at this point that you have a finite proof of "for all n, p(n)". The axiom of induction tells you that you do have such a proof. Looks like we're not so lucky here though!

[Aaron Liu]

According to Gödel's second incompleteness theorem, assuming your system is consistent, it is not possible to prove the statement "for every natural $n$, there is no proof of $\text{False}$ of length at most $n$". However, then for every natural $n$ it is possible to prove the statement "there is no proof of $\text{False}$ of length at most $n$" just by enumerating every proof. The difference is that you can't condense the infinitely many proofs into just one because proofs have to be finite.

[Filippo A. E. Nuccio]

Oh, I see, thank you all. I thought I grasped the difference between the existence of $\omega$ inaccessible cardinals and the existence of $n$ of them for every $n$, but @Mario Carneiro 's explanation is very enlightening. In particular, I could not parse the braces appropriately to figure out what was what, and @Kevin Buzzard helped with this. :pray: