Stream: maths

Topic: condensed mathematics

Kevin Buzzard (Apr 29 2019 at 20:15):

I mentioned a link to a talk of Scholze on condensed sets recently. He's giving a course on it now:

http://www.math.uni-bonn.de/ag/alggeom/veranstaltungen/veranstaltungen_ss19

Here's a direct link to the pdf notes. @Scott Morrison @Reid Barton if you want to find a use for your categories other than "doing schemes properly" -- can you do this? This all looks very very reasonable to do in Lean, and it is a Fields Medallist explaining some completely up to the minute ideas. @Patrick Massot can you make anything of this? Scholze is wresting with some very general ideas about how mathematicians put topology in their work, but of course he is coming from a very algebraic perspective. @Kenny Lau after exams do you want to take a look at this? This might be a big thing, and in stark contrast to the perfectoid space theory, the entireity of what is known to humanity about condensed mathematics is in those 33 pages. Seems like a great time to start formalising it!

Kevin Buzzard (Apr 29 2019 at 20:17):

Theorem 1.10. The category of condensed abelian groups is an abelian category which satis-
fies Grothendieck’s axioms (AB3), (AB4), (AB5), (AB6), (AB3*) and (AB4*), to wit: all limits
(AB3*) and colimits (AB3) exist, arbitrary products (AB4*), arbitrary direct sums (AB4) and fil-
tered colimits (AB5) are exact,...


The proof looks simple. @Reid Barton how far are we from formalising this stuff in Lean?

Kevin Buzzard (Apr 29 2019 at 20:18):

Proof is in lecture 2.

Kevin Buzzard (Apr 29 2019 at 20:19):

Scholze seems to be worrying about the kind of things you once told me you were worrying about (cutting off the universe at kappa and then worrying about what he's lost)

Jesse Michael Han (Apr 29 2019 at 20:31):

Tom and I were actually discussing this as a possible project last week. I guess it depends on the API for sheaves on sites. Do we have a definition of what it means for a Grothendieck topology to be generated by covering families, and can we work with sheaves on sites other than the opens of a topological space? Do we have the category of pro-objects of finsets, or at least Stone spaces? If that's all there, then the various categories of condensed (insert models of algebraic theory) should be straightforward to define.

Kevin Buzzard (Apr 29 2019 at 20:36):

I know that @Johan Commelin was thinking about Grothendieck topologies at some point but he ran into problems. Johan -- why did you stop doing sheaves on sites? Would working in one fixed universe help matters? Note that Scholze spends half his life justifying how he can do everything in Type 0.

Kenny Lau (Apr 29 2019 at 21:17):

what is condensed mathematics?

Patrick Massot (Apr 29 2019 at 21:23):

You need to read the paper, or watch the talk

Kevin Buzzard (Apr 29 2019 at 21:28):

A condensed X is a functor from the cat of profinite sets to the cat of X's. This is all coming out of Scholze's pro-etale stuff but it's independent of that.

Jesse Michael Han (Apr 29 2019 at 21:28):

in a slogan, "mathematics internal to the topos of sheaves on the pro-etale site"

Kevin Buzzard (Apr 29 2019 at 21:28):

One of the insights is that we always used to think about the etale site, but never the pro-etale site; this was only discovered a few years ago.

Johan Commelin (Apr 30 2019 at 04:24):

I stopped doing sheaves because I wasn't getting anywhere, and I wanted to move on with the perfectoid project. I would love to return to sites and topoi. Especially if there are more people who want to contribute!

Johan Commelin (Apr 30 2019 at 04:26):

Note that the first 5 pages out of 33 don't contain any maths. Otoh... lecturing has just started in Germany... so you can expect that from this week onwards this document will grow with 25 pages a week, until mid-July. (In particular, I don't think the statement "all that is known about condensed mathematics is written in these 33 pages" is correct. There are likely stacks of notes by Dustin and Peter lying around in there offices. And those will be appended to these lecture notes at high speed.)

Johan Commelin (Apr 30 2019 at 06:40):

I fear that formalising §2 will be quite hard. We'll need a very decent API for sites if we want to prove that a certain topos is equivalent to sheaves on various different sites.

Johan Commelin (Apr 30 2019 at 06:53):

Warning 2.8 suggests that we might first want to formalise infty-cats

Kevin Buzzard (Apr 30 2019 at 07:22):

I believe that both @Mario Carneiro and I have similar feelings about category theory -- at a basic level it offers little more than a collection of organising principles, and so far in mathlib we have managed to formalise many of those basic organising principles just fine without having to bundle everything -- see Galois connections etc. However, beyond a certain point the language does become a lot more useful and powerful, when the stuff you're organising starts getting out of hand. We are on the verge of this in mathlib -- we don't have sheaf cohomology yet but I could imagine defining it as a derived functor, for example. But because it's not been essential for anything else just yet, it is still there being rather uncared for with only Scott and Reid ever contributing to it. I have proposed rewriting parts of the schemes project using this language, and I would still very much like to do this. But this much meatier project of condensed mathematics might be a way of understanding much better which parts of the library need developing. How much of the basic category theory material needed before we can even contemplate a basic API for sites is already in mathlib and how much is just languishing elsewhere, about ten PR's away? That's a key question right now.

oh boy

Mario Carneiro (Apr 30 2019 at 07:35):

If you think handling non-defeq type equalities and equivs are bad now, just wait until you see what infinity cats are like

Kevin Buzzard (Apr 30 2019 at 07:36):

More and more people are using infinity categories. Lurie is using them to do number theory.

Mario Carneiro (Apr 30 2019 at 07:36):

that seems infinitely more complicated than necessary

Kevin Buzzard (Apr 30 2019 at 07:37):

https://press.princeton.edu/titles/8957.html

Kevin Buzzard (Apr 30 2019 at 07:37):

This stuff is no longer in the fringes. That's not just some logician doing navel-gazing, that's someone interested in actual questions in geometry

Mario Carneiro (Apr 30 2019 at 07:37):

Infinity categories are deeply connected to HoTT. The language of HoTT is basically infinity groupoids

Kevin Buzzard (Apr 30 2019 at 07:38):

But we can emulate HoTT in Lean, right?

Kevin Buzzard (Apr 30 2019 at 07:38):

Where is this HoTT library that I never look at...

Mario Carneiro (Apr 30 2019 at 07:38):

but the level of dependent types you have to deal with is almost unpalatable

Kevin Buzzard (Apr 30 2019 at 07:38):

https://github.com/gebner/hott3

Kevin Buzzard (Apr 30 2019 at 07:39):

don't use rewrite, use rwr instead

oh hells bells

Mario Carneiro (Apr 30 2019 at 07:39):

It's possible, but it tends to take over your research program until everything is homotopy classes of spheres

Kevin Buzzard (Apr 30 2019 at 07:40):

That is exactly what I want to not happen.

Kenny Lau (Apr 30 2019 at 07:41):

when you said "the entirety of what is known to humanity about condensed mathematics is in those 33 pages" I thought you meant "the entirety of what is known to humanity about mathematics is condensed in those 33 pages"

Kevin Buzzard (Apr 30 2019 at 07:41):

Voevodsky's 2017 talk in Cambridge: "I got interested in this stuff, I kind of wanted to formalise some of my work on Bloch-Kato, and then all of a sudden I decided to reject the axiom of choice and now I am doing other things. And Bloch-Kato will now never be done because I lost interest."

Kevin Buzzard (Apr 30 2019 at 07:41):

when you said "the entirety of what is known to humanity about condensed mathematics is in those 33 pages" I thought you meant "the entirety of what is known to humanity about mathematics is condensed in those 33 pages"

I am not sure the theory has had that much impact yet ;-)

Kenny Lau (Apr 30 2019 at 07:41):

and then to my disappointment I couldn't find the Green's function for the Laplacian there

Kevin Buzzard (Apr 30 2019 at 07:42):

and then to my disappointment I couldn't find the Green's function for the Laplacian there

@Kenny Lau you might find it in Faltings' work on the Mordell conjecture...

Mario Carneiro (Apr 30 2019 at 07:44):

I would be curious to see what a "plain formalization" of infinity categories looks like. HoTT is more of a "synthetic" formulation, a.k.a a shallow embedding, where you can't see outside the theory and so principles like univalence can be stated unqualified as axioms

Kevin Buzzard (Apr 30 2019 at 07:45):

Right. The difference between the two ideas is slowly dawning on me.

Mario Carneiro (Apr 30 2019 at 07:45):

I don't know if anyone has tried the external perspective, where they are just some structure with stuff

Kevin Buzzard (Apr 30 2019 at 07:46):

So HoTT in Lean 3 is just like doing HoTT in Coq? There are various tactics which you're not allowed to use any more because they lead to contradictions?

yes

Kevin Buzzard (Apr 30 2019 at 07:46):

They add an axiom which formally speaking is inconsistent?

Kevin Buzzard (Apr 30 2019 at 07:46):

And then get round it by making us promise not to use subsingleton elimination?

Mario Carneiro (Apr 30 2019 at 07:47):

In lean 3, unlike lean 2, you can't "turn off Prop", which is inconsistent with HoTT, so instead you have to carefully examine every def to make sure it doesn't use anything bad

oh boy

Mario Carneiro (Apr 30 2019 at 07:47):

There is a @[hott] attribute to automate this

Mario Carneiro (Apr 30 2019 at 07:48):

of course, Prop is "no axioms"...

Kevin Buzzard (Apr 30 2019 at 07:48):

axiom univalence (A B : Type u) : is_equiv (@equiv_of_eq A B)


There it is.

It's too strong

Johan Commelin (Apr 30 2019 at 07:49):

@Mario Carneiro Have you read the intro of HTT by Lurie? It is very readable and it show how the "external" theory of infty-cats might be done.

Kevin Buzzard (Apr 30 2019 at 07:49):

We just want univalence to apply to mathematical objects, and only at certain times.

is it free?

It is

Kevin Buzzard (Apr 30 2019 at 07:49):

https://arxiv.org/abs/math/0608040

Johan Commelin (Apr 30 2019 at 07:50):

Checkout Lurie's website! It contains several thousands of carefully written hardcore maths

Johan Commelin (Apr 30 2019 at 07:50):

https://kerodon.net/ — this is where Lurie is now putting all his stuff. But it isn't as complete as his other writings yet.

Mario Carneiro (Apr 30 2019 at 07:50):

I am highly doubtful that any HoTT embedding stuff will help you in your quest @Kevin Buzzard better than transfer, even as it currently exists

Johan Commelin (Apr 30 2019 at 07:51):

Mario, infty cats existed and where used before HoTT was cooked up.

of course

Johan Commelin (Apr 30 2019 at 07:51):

They are really essential to certain parts of maths. Not because of transport-like things. Because of actual maths-with-content

Johan Commelin (Apr 30 2019 at 07:51):

See Warning 2.8 in the notes by Scholze at the top of this thread.

Mario Carneiro (Apr 30 2019 at 07:52):

I know, I'm just saying that category theory is hard and infty-cats are harder

Johan Commelin (Apr 30 2019 at 07:52):

Hmm... you seemed to be saying more than that (-;

Mario Carneiro (Apr 30 2019 at 07:53):

I've expected this request to appear for some time now; we already have CAT as a higher category

Mario Carneiro (Apr 30 2019 at 07:54):

and given the way equalities "aren't good enough" for DTT it's really natively an infty cat even if you don't want it to be

Mario Carneiro (Apr 30 2019 at 07:55):

and that's why HoTT is implemented as a dependent type theory rather than something else

Mario Carneiro (Apr 30 2019 at 07:56):

but I don't think this makes anything easier - it's more like "DTT is hard, infty-cats are hard - match made in heaven"

Mario Carneiro (Apr 30 2019 at 07:57):

That said I'm obviously biased. There are lots of type theorists that will tell you how great HoTT is. My worry is that they are all type theorists

Johan Commelin (Apr 30 2019 at 07:58):

For this discussion, I (for once, w00t) don't care about HoTT.

Johan Commelin (Apr 30 2019 at 07:58):

I just want actual infty-cats

Johan Commelin (Apr 30 2019 at 07:58):

No matter which foundations we have.

Kevin Buzzard (Apr 30 2019 at 07:59):

Lurie manages to prove a nonabelian version of proper base change. Great.

Kevin Buzzard (Apr 30 2019 at 07:59):

Did I ever need that? Classical proper base change sure, but why this?

Johan Commelin (Apr 30 2019 at 07:59):

Lurie manages to prove a nonabelian version of proper base change. Great.

@Mario Carneiro That's the kind of stuff we're talking about. This is completely orthogonal to HoTT (as far as I know).

Johan Commelin (Apr 30 2019 at 08:00):

Well, Lurie also managed to prove some stuff in geometric Langlands

Johan Commelin (Apr 30 2019 at 08:00):

And Bhatt and Scholze didn't jump on the infty-cat-ship for no reason

Kevin Buzzard (Apr 30 2019 at 08:32):

Well, Lurie also managed to prove some stuff in geometric Langlands

Did he prove anything concrete which wasn't known already, or did he somehow just categorify known results? Do you understand anything about his work on the Tamagawa number problem Johan? Does one need category theory to prove it?

Johan Commelin (Apr 30 2019 at 08:33):

I am not even close to really understanding his work. But he seems to have proven new stuff, yes.

Mario Carneiro (Apr 30 2019 at 08:36):

I wish we had a better proof-theoretic analysis of these kinds of proofs, so we can say to what extent the use of categories or higher categories is necessary or compresses the direct proof

Kevin Buzzard (Apr 30 2019 at 08:37):

He proved the Tamagawa number conjecture for function fields, right? If he did it using infinity categories in an "essential" way (i.e. stripping them out would cause genuine pain) then that would be interesting. I simply have no idea how he did it. I went to a lecture by him about it all and it was 55 minutes history of the problem and then 5 minutes "oh by the way I finished the job"

Johan Commelin (Apr 30 2019 at 08:37):

Yup, I've seen a similar talk by him...

Kevin Buzzard (Apr 30 2019 at 08:38):

I wish we had a better proof-theoretic analysis of these kinds of proofs, so we can say to what extent the use of categories or higher categories is necessary or compresses the direct proof

"necessary" - I bet nothing is necessary. "Compresses the proof" -- yeah, this is the sort of question which might be interesting.

Mario Carneiro (Apr 30 2019 at 08:38):

Well, they say similar things about FLT, but AFAIK it's all still folklore

Mario Carneiro (Apr 30 2019 at 08:39):

that you don't need categories or universes to prove it

Mario Carneiro (Apr 30 2019 at 08:39):

and it's provable in PA

Kevin Buzzard (Apr 30 2019 at 08:39):

Oh you definitely don't need categories or universes

Kevin Buzzard (Apr 30 2019 at 08:39):

you can easily modify the proof to avoid them

Kevin Buzzard (Apr 30 2019 at 08:39):

but modifying the proof so that it worked without AC would be extremely difficult

Kevin Buzzard (Apr 30 2019 at 08:40):

There's just some nonsense logic theorem saying something, isn't there? Completely nonconstructive

Kevin Buzzard (Apr 30 2019 at 08:40):

I don't even know what it says. Certainly "provable in ZFC" -> "true in PA" but do we know "provable in PA"?

Mario Carneiro (Apr 30 2019 at 08:40):

all the nonsense logic theorems I've heard in this area are actually constructive, although possibly with an obscene upper bound

Kevin Buzzard (Apr 30 2019 at 08:40):

That Goodstein sequence thing is true but not provable in PA

Kevin Buzzard (Apr 30 2019 at 08:41):

But is that somehow of some higher complexity than FLT?

Mario Carneiro (Apr 30 2019 at 08:41):

FLT is Pi1, that's probably part of it

Kevin Buzzard (Apr 30 2019 at 08:41):

https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem

Mario Carneiro (Apr 30 2019 at 08:42):

Paris-Harrington is Pi2

Thanks

Kevin Buzzard (Apr 30 2019 at 08:42):

So do you think it's a theorem that FLT has a proof in PA?

Kevin Buzzard (Apr 30 2019 at 08:42):

I don't know enough logic

Mario Carneiro (Apr 30 2019 at 08:43):

I have no idea... I know someone claims this

Kevin Buzzard (Apr 30 2019 at 08:43):

Most mathematicians have no interest in this sort of thing

Mario Carneiro (Apr 30 2019 at 08:43):

I'm not familiar with the details of the argument

Kevin Buzzard (Apr 30 2019 at 08:43):

[obviously we're assuming FLT has a proof in ZFC, which I am happy to believe]

Mario Carneiro (Apr 30 2019 at 08:43):

Con(PA) is also Pi1, so it can't be as simple as that

Kevin Buzzard (Apr 30 2019 at 08:44):

aah, and it has a proof in ZFC too

Mario Carneiro (Apr 30 2019 at 08:45):

But I'm more interested in whether there is a practical proof in PA

Mario Carneiro (Apr 30 2019 at 08:46):

like maybe all the linguistic fluff about infinite sets can be removed

Mario Carneiro (Apr 30 2019 at 08:49):

There are definitely examples of the opposite phenomenon though - whenever you increase the consistency strength you get more than just new proofs, you also get shorter proofs for provable things

Kevin Buzzard (Apr 30 2019 at 08:49):

It's impossible to rule out some trivial proof of FLT in PA although it would be the biggest shock to happen in pure mathematics for centuries were an elementary proof to be found. Number theorists believe they understand the nature of Diophantine equations in general, especially smooth affine curves like $x^n+y^n=1$ over the rationals. Developing tools to bound the solutions to such equations has been a focal point of interest for centuries now, or even millenia if you count Diophantus himself. So many brilliant people have thought about this general problem, that the idea that there might be some cheap new method is almost inconcievable.

Mario Carneiro (Apr 30 2019 at 08:50):

My hope is not so much to invent a new method as find a way to extract the content from the existing proof

Kevin Buzzard (Apr 30 2019 at 08:50):

We have elaborate methods and conjectures, which ultimately yielded a proof of FLT, but 25 years later we are not really any closer to seeing on a more elementary level why it is true. It's a consequence of the Langlands philosophy, by deep work of Ribet and an observation of Frey-Hellgouarch.

Kevin Buzzard (Apr 30 2019 at 08:51):

The content, when unravelled, would stretch for miles.

In Lean, say.

Kevin Buzzard (Apr 30 2019 at 08:51):

with all the classical.choice stuff in it

yes, absolutely

Mario Carneiro (Apr 30 2019 at 08:51):

any kind of formalization would be a huge help

Kevin Buzzard (Apr 30 2019 at 08:51):

and real and complex numbers

Mario Carneiro (Apr 30 2019 at 08:52):

just having it all in one place with all prerequisites is immensely useful

Kevin Buzzard (Apr 30 2019 at 08:52):

What about giving a partial proof term of the form "and so if we believe this explicit statement relating modular forms to elliptic curves, then we're done"

Kevin Buzzard (Apr 30 2019 at 08:52):

A proof that Shimura-Taniyama-Weil implies FLT.

Kevin Buzzard (Apr 30 2019 at 08:53):

As input there's some statement about modular forms, which are functions on the upper half of the complex plane.

Mario Carneiro (Apr 30 2019 at 08:53):

The problem with this kind of result is that it's not "closed" in the original language - you are giving a statement that is in the new language, so any conservativity results don't apply

Kevin Buzzard (Apr 30 2019 at 08:53):

That's just hundreds of pages of scheme nonsense :-)

I see.

Mario Carneiro (Apr 30 2019 at 08:54):

If there is a PA way to state an equivalent of that conjecture, that would work

Hmm

Kevin Buzzard (Apr 30 2019 at 08:54):

I don't know if that is possible or not.

Kevin Buzzard (Apr 30 2019 at 08:55):

I guess I believe the proof of it so it is possible in a crappy logic sense

Kevin Buzzard (Apr 30 2019 at 08:55):

but I have no idea how bad PA really is.

Mario Carneiro (Apr 30 2019 at 08:55):

It's not obvious that RH has a PA equivalent either

Mario Carneiro (Apr 30 2019 at 08:59):

The theorem states that any elliptic curve over $\Bbb Q$ can be obtained via a rational map with integer coefficients from the classical modular curve $X_{0}(N)$ for some integer N; this is a curve with integer coefficients with an explicit definition. This mapping is called a modular parametrization of level N. [From https://en.wikipedia.org/wiki/Modularity_theorem ]

I think that's a statement in PA

Mario Carneiro (Apr 30 2019 at 09:00):

insofar as it's a claim about equality of polynomials over Q

Mario Carneiro (Apr 30 2019 at 09:04):

oh wait, "rational map" does not mean what I thought it meant

Mario Carneiro (Apr 30 2019 at 09:05):

is this just a rational function?

Johan Commelin (Apr 30 2019 at 09:06):

No... not exactly

Johan Commelin (Apr 30 2019 at 09:06):

A rational function is a rational map to P^1 (= projective line)

Johan Commelin (Apr 30 2019 at 09:06):

A rational map is a morphism defined on a dense open subset.

Johan Commelin (Apr 30 2019 at 09:07):

We are hoping that the new partial keyword will make it very easy to use rational maps in Lean 4 :rolling_on_the_floor_laughing:

Mario Carneiro (Apr 30 2019 at 09:07):

we're talking about equivalence of elliptic curves, though, so it's CP^1, right?

Mario Carneiro (Apr 30 2019 at 09:08):

I want to know if there is an easy way to express "obtained by a rational map" in the quoted theorem

Johan Commelin (Apr 30 2019 at 09:08):

I think the theorem is saying "For every ell.curve $E$, there exists an integer $N$ and a rational map $X_0(N) \to E$.

Mario Carneiro (Apr 30 2019 at 09:09):

I believe that, but I don't know what parameterizes the possible rational maps

Mario Carneiro (Apr 30 2019 at 09:10):

That is, both sides are elliptic curves over Q, so surely there is an easy way to describe when a rational map exists?

Johan Commelin (Apr 30 2019 at 09:10):

The LHS is not an ell.curve, it usually has higher genus

Mario Carneiro (Apr 30 2019 at 09:11):

pretend I don't know what that means :) It's still a variety?

Mario Carneiro (Apr 30 2019 at 09:11):

i.e. solution set to some polynomial

Kevin Buzzard (Apr 30 2019 at 09:12):

For all N there's some magic set of equations depending on N with rational coefficients which define an algebraic variety, yes

Kevin Buzzard (Apr 30 2019 at 09:12):

Indeed the equations define a smooth projective curve

Kevin Buzzard (Apr 30 2019 at 09:13):

I think that one could even just rephrase this in terms of function fields.

Mario Carneiro (Apr 30 2019 at 09:13):

but how much "data" is needed to specify the rational map that connects it to the original curve?

Kevin Buzzard (Apr 30 2019 at 09:13):

An elliptic curve is determined by two integers A and B

Mario Carneiro (Apr 30 2019 at 09:14):

I don't want to have to specify a dense open set

Kevin Buzzard (Apr 30 2019 at 09:14):

and using these integers one can make an explicit field

Kevin Buzzard (Apr 30 2019 at 09:14):

it's OK, what I'm going to say is concrete and avoids those problems

Kevin Buzzard (Apr 30 2019 at 09:14):

The field is the field of fractions of $\mathbb{Q}[X,Y]/(Y^2-X^3-AX-B)$

Kevin Buzzard (Apr 30 2019 at 09:15):

Similarly given a positive integer $N$ there is another field of this form

Kevin Buzzard (Apr 30 2019 at 09:15):

the field of rational functions of $X_0(N)$

so far so good

Kevin Buzzard (Apr 30 2019 at 09:16):

and the conjecture is that for all $A$ and $B$ with $4A^3-27B^2\not=0$ there exists $N$ and a ring homomorphism from the $A, B$ field to the $N$ field.

aha

Mario Carneiro (Apr 30 2019 at 09:16):

that's PA alright

Kevin Buzzard (Apr 30 2019 at 09:16):

I am not sure how explicit I can make the $N$ field

no scratch that

Kevin Buzzard (Apr 30 2019 at 09:16):

I can make it completely explicit

Kevin Buzzard (Apr 30 2019 at 09:17):

I can use $X(N)$ and build the field using division polynomials on the universal elliptic curve

Kevin Buzzard (Apr 30 2019 at 09:17):

I can use $X(3N)$ and not have to worry about representability issues

Kevin Buzzard (Apr 30 2019 at 09:18):

@Johan Commelin how about this: I write down the universal elliptic curve over $X(3)$ explicitly ($X(3)$ has genus 0) and then I find the equation for the modular curves $X(3N)$ using division polynomials, which are completely algorithmic

Kevin Buzzard (Apr 30 2019 at 09:19):

The division polynomials factor because a point of order $N$ can have exact order $d$ for some $d\mid N$

Kevin Buzzard (Apr 30 2019 at 09:20):

but I am not sure I even care. I can take the total ring of fractions and then just demand that for all Weierstrass models there's some N such that the field of fractions of the Weierstrass model over Q embeds into this total ring of fractions.

Kevin Buzzard (Apr 30 2019 at 09:20):

That's a surprisingly low-level statement of Taniyama-Shimura or whatever it's called nowadays

Johan Commelin (Apr 30 2019 at 09:23):

Right... I guess you can prove it by induction on $A$ and $B$. (But that's probably the hard part of the proof.)

Kevin Buzzard (Apr 30 2019 at 09:31):

given that that's the only technique you have, I would definitely recommend using it at least once.

Floris van Doorn (Apr 30 2019 at 14:38):

Re: condensed mathematics. If people think this would be an interesting project to formalize, I'd be happy to help with the formalization.

Floris van Doorn (Apr 30 2019 at 14:45):

Re: higher categories. I believe there is a formalization in progress to do semantics of HoTT. Maybe they formalized higher or infinity categories there, although I cannot find the repository now.
On the other hand, often when doing categorical semantics of (homotopy) type theory, you don't directly work with infinity-categories, but instead you work with a model category (or similar), which is just a 1-category with some extra data. You can construct an infinity-category out of this data, but in practice it's easier to work with the 1-categorical formulation (for obvious reasons).

Patrick Massot (Apr 30 2019 at 14:50):

Floris, you must understand Kevin is overexcited by the completion of the perfectoid project, and dreaming out loud. There is no way we can formalize condensed mathematics when the category theory part of mathlib is not usable to define schemes.

Jesse Michael Han (Apr 30 2019 at 14:53):

@Floris van Doorn let's do it! (after we finish Flypitch, and iterated forcing, and inter-universal Teichmueller theory...)

Jesse Michael Han (May 01 2019 at 14:10):

related: https://arxiv.org/abs/1904.09966

they take hypersheaves (whatever that means) on compact hausdorff spaces instead of just Stone spaces (with the same type of Grothendieck topology, I believe)

interestingly, in 0.3 of the introduction, the authors point out that their theory actually requires an inaccessible cardinal while the theory of condensed objects can be developed in ZFC

also all the careful bookkeeping of universe-levels for sheaves and the word "tiny" (which I think is their terminology for _ : Type 0) is something that we're already used to dealing with in the category theory library

Johan Commelin (Nov 25 2019 at 11:40):

We will just note that “the” real numbers are not well-defined anymore:To define a category of modules over $\mathbb{R}$, one needs to specify in addition $0 < p < 1$; and in some sense an infinitesimal deformation of $p$ gives rise to $B^+_{\mathrm{dR}}$, so there is in some sense a 1-parameter family of versions of the real numbers.

Johan Commelin (Nov 25 2019 at 11:45):

I'm not sure what the type of p is in this remark :rolling_on_the_floor_laughing:

Kevin Buzzard (Nov 25 2019 at 11:47):

I've been thinking about this with @Calle Sönne . I think that this stuff represents a really good way to see the category theory stuff in action. For a start it forces you to think about sites. @Reid Barton suggested following this approach for sites; then we need profinite sets, extremely disconnected sets and some basic theorems relating them -- do we have Stone-Cech compactifications? They would be really fun to do. Proving that the categories of sheaves on the three sites are equivalent (props 2.3 and 2.7 of Scholze's notes ) would be a great exercise, the maths proofs are relatively simple. Did anyone do sites in Coq or any of the other systems yet? Then proving Theorem 2.2 of those notes would be some flagship result.

Kevin Buzzard (Nov 25 2019 at 11:47):

The $\mathbb{R}$ stuff is much further away.

Johan Commelin (Nov 25 2019 at 11:48):

Stone-Cech is in mathlib. Done by Reid.

Johan Commelin (Nov 25 2019 at 11:48):

Sites have been done in Coq.

Kevin Buzzard (Nov 25 2019 at 11:48):

Do they work? Have people used them to do anything?

Johan Commelin (Nov 25 2019 at 11:48):

As far as I know, they haven't been used.

Johan Commelin (Nov 25 2019 at 11:49):

I found that defining sites and sheaves was not the hard thing. The hard thing for me was the $f_*$-$f^*$ adjunction.

Johan Commelin (Nov 25 2019 at 11:50):

And such adjunctions will be rather crucial a little down the road.

Kevin Buzzard (Nov 25 2019 at 12:07):

Did you already do sites and sheaves?

Johan Commelin (Nov 25 2019 at 12:08):

Yes, last year. But I never got a satisfactory API

Johan Commelin (Nov 25 2019 at 12:08):

Just having sheaves is not good enough. You need to be able to pull and push them around

Johan Commelin (Nov 25 2019 at 12:09):

I also had trouble showing that representable functors on Top are sheaves wrt the usual topology

Johan Commelin (Nov 25 2019 at 12:10):

So I could neither handle abstract nonsense nor concrete examples

Kevin Buzzard (Nov 25 2019 at 12:10):

Can they do either of these in Coq?

Je ne sais pas

Kevin Buzzard (Nov 25 2019 at 12:11):

Do we have adjunctions in Lean?

Kevin Buzzard (Nov 25 2019 at 12:11):

Where is this work? It needs to be done.

Johan Commelin (Nov 25 2019 at 12:12):

http://www-sop.inria.fr/lemme/personnel/Laurent.Chicli/FrCoq.html

Kevin Buzzard (Nov 25 2019 at 12:15):

I mean where is the Lean work?

Kevin Buzzard (Nov 25 2019 at 12:16):

@Kenny Lau this is a better generality for gluing than sheaves on a topological space.

what is?

Kevin Buzzard (Nov 25 2019 at 12:17):

gluing sheaves on a site.

Kevin Buzzard (Nov 25 2019 at 12:18):

What I am unclear about is whether it's worth making an API for sheaves on a topological space and then starting on e.g. etale cohomology and realising that one has to do it all again for sheaves on a site.

Johan Commelin (Nov 25 2019 at 12:35):

My guess is that Mario would say it's worth it to do it twice

Why?

Johan Commelin (Nov 25 2019 at 12:36):

Because that's what he often seems to say

Johan Commelin (Nov 25 2019 at 12:36):

Premature optimization and all that....

Johan Commelin (Nov 25 2019 at 12:36):

Sometimes generalities are good, sometimes they're not

Johan Commelin (Nov 25 2019 at 12:38):

@Kevin Buzzard I've pushed some branches to github

Johan Commelin (Nov 25 2019 at 12:38):

sheaf-old, presheaf, sheaf, and sheaf-2

Kevin Buzzard (Nov 25 2019 at 12:38):

which one should I look at?

:D

Johan Commelin (Nov 25 2019 at 12:38):

It's been 1 year since I worked on this

Johan Commelin (Nov 25 2019 at 12:40):

There is also sheaves by @Scott Morrison. But it's not doing sites, just topological spaces

Johan Commelin (Nov 25 2019 at 12:45):

Yup... the analysis side of mathlib has made major strides in the last 6 months... the algebraic side didn't really move at all :expressionless:

Kevin Buzzard (Nov 25 2019 at 12:45):

the analysis side has got a lot of catching up to do though :D

Kevin Buzzard (Nov 25 2019 at 12:46):

If you imagine what we teach our 1st years, they certainly know that a power series is differentiable within its radius of convergence.

Johan Commelin (Nov 25 2019 at 12:47):

The 2nd year students know that a degree 5 equation can't be solved by radicals...

Johan Commelin (Nov 25 2019 at 12:47):

Anyway... let's stay on the topic of sites and sheaves (-;

Johan Commelin (Nov 25 2019 at 12:48):

I'm about to run a way to a seminar that has the same name as this thread

Mario Carneiro (Nov 25 2019 at 13:10):

I agree with Johan's projection of me

Mario Carneiro (Nov 25 2019 at 13:11):

The important thing is to get out of the slump, and just do something. It's not as bad as it sounds to do almost the same thing twice, and you often learn a lot in the process

Mario Carneiro (Nov 25 2019 at 13:12):

if in the end it turns out they are better served with a common definition, then you refactor later, simple as that

Johan Commelin (Nov 25 2019 at 14:51):

Getting out of the slump seems rather hard here... we've had countless discussions about sheaves here on Zulip. We have the approach taken in the schemes project, which worked I guess. We used that code for perfectoid spaces as well, where it started to show some cracks, because all of a sudden we needed sheaves of X's for lots of values of X. And Kevin just hacked the code together, but it was very much write-only code.

Johan Commelin (Nov 25 2019 at 14:52):

Designing something that scales well seems a rather non-trivial issue

Johan Commelin (Nov 25 2019 at 14:52):

Scott wrote https://github.com/leanprover-community/mathlib/issues/1462 which I think is a good strategy for dealing with "down-to-earth" sheaves

Johan Commelin (Nov 25 2019 at 14:53):

But I keep coming back to the push-pull adjunction. In all my experiments over a year ago, I couldn't pull that off.

Johan Commelin (Oct 26 2020 at 19:34):

For anyone interested in condensed maths:

Dear all,

This is to inform you that the Master Class on Condensed Mathematics, to be held in Copenhagen, November 9th-13th with lectures by Dustin Clausen and Peter Scholze, will be shifted to a fully online event. This is due to the rising number of Covid-19 cases which, together with the number of already registered participants, makes it difficult for us to organise this event in accordance to the safety and health regulations of the University of Copenhagen.

The lectures will be live streamed through Zoom and in addition will be made available on the Youtube channel of the Center of Geometry and Topology at Copenhagen, which is: