Zulip Chat Archive

Stream: maths

Topic: condensed mathematics


view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 29 2019 at 20:18):

Proof is in lecture 2.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 29 2019 at 21:17):

what is condensed mathematics?

view this post on Zulip Patrick Massot (Apr 29 2019 at 21:23):

You need to read the paper, or watch the talk

view this post on Zulip 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.

view this post on Zulip Jesse Michael Han (Apr 29 2019 at 21:28):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 30 2019 at 06:53):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:34):

oh boy

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:36):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:36):

that seems infinitely more complicated than necessary

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:37):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:37):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:38):

But we can emulate HoTT in Lean, right?

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:38):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:38):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:38):

https://github.com/gebner/hott3

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:39):

don't use rewrite, use rwr instead

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:39):

oh hells bells

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:40):

That is exactly what I want to not happen.

view this post on Zulip 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"

view this post on Zulip 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."

view this post on Zulip 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 ;-)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:41):

@Floris van Doorn is definitely the best expert to ask about this

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:45):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:46):

yes

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:46):

They add an axiom which formally speaking is inconsistent?

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:46):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:47):

oh boy

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:47):

There is a @[hott] attribute to automate this

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:48):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:48):

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

There it is.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:49):

It's too strong

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:49):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:49):

is it free?

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:49):

It is

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:49):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:50):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:51):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:51):

of course

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:51):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:52):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:52):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 07:55):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:58):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:58):

I just want actual infty-cats

view this post on Zulip Johan Commelin (Apr 30 2019 at 07:58):

No matter which foundations we have.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:59):

I don't know enough about this stuff to know why I as a working mathematician should care about this stuff.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:59):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 07:59):

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

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Apr 30 2019 at 08:00):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 08:00):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Apr 30 2019 at 08:37):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:38):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:38):

What is said about FLT?

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:39):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:39):

and it's provable in PA

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:39):

Oh you definitely don't need categories or universes

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:39):

you can easily modify the proof to avoid them

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:39):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:40):

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

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:40):

That Goodstein sequence thing is true but not provable in PA

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:41):

But is that somehow of some higher complexity than FLT?

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:41):

FLT is Pi1, that's probably part of it

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:41):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:42):

Paris-Harrington is Pi2

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:42):

Thanks

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:42):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:42):

I don't know enough logic

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:43):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:43):

Most mathematicians have no interest in this sort of thing

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:43):

I'm not familiar with the details of the argument

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:43):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:43):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:44):

aah, and it has a proof in ZFC too

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:45):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:46):

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

view this post on Zulip 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

view this post on Zulip 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 xn+yn=1x^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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:51):

The content, when unravelled, would stretch for miles.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:51):

Would giving the proof term help you to extract the content??

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:51):

In Lean, say.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:51):

with all the classical.choice stuff in it

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:51):

yes, absolutely

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:51):

and the p-adic numbers etc

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:51):

any kind of formalization would be a huge help

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:51):

and real and complex numbers

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:52):

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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:52):

A proof that Shimura-Taniyama-Weil implies FLT.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:53):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:54):

I see.

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:54):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:54):

Hmm

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:54):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 08:55):

but I have no idea how bad PA really is.

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:55):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 08:59):

The theorem states that any elliptic curve over Q\Bbb Q can be obtained via a rational map with integer coefficients from the classical modular curve X0(N)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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:00):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:04):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:05):

is this just a rational function?

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:06):

No... not exactly

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:06):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:06):

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

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:07):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:08):

I don't get your question

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:08):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:09):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:10):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:11):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:11):

i.e. solution set to some polynomial

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:12):

Indeed the equations define a smooth projective curve

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:13):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:13):

An elliptic curve is determined by two integers A and B

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:14):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:14):

and using these integers one can make an explicit field

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:14):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:14):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:15):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:15):

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

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:15):

so far so good

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:16):

and the conjecture is that for all AA and BB with 4A327B2̸=04A^3-27B^2\not=0 there exists NN and a ring homomorphism from the A,BA, B field to the NN field.

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:16):

aha

view this post on Zulip Mario Carneiro (Apr 30 2019 at 09:16):

that's PA alright

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:16):

I am not sure how explicit I can make the NN field

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:16):

no scratch that

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:16):

I can make it completely explicit

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:17):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:17):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:18):

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

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:19):

The division polynomials factor because a point of order NN can have exact order dd for some dNd\mid N

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 30 2019 at 09:20):

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

view this post on Zulip Johan Commelin (Apr 30 2019 at 09:23):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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

view this post on Zulip 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 R\mathbb{R}, one needs to specify in addition 0<p<10 < p < 1; and in some sense an infinitesimal deformation of pp gives rise to BdR+B^+_{\mathrm{dR}}, so there is in some sense a 1-parameter family of versions of the real numbers.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 11:47):

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

view this post on Zulip Johan Commelin (Nov 25 2019 at 11:48):

Stone-Cech is in mathlib. Done by Reid.

view this post on Zulip Johan Commelin (Nov 25 2019 at 11:48):

Sites have been done in Coq.

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 11:48):

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

view this post on Zulip Johan Commelin (Nov 25 2019 at 11:48):

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

view this post on Zulip 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 ff_*-ff^* adjunction.

view this post on Zulip Johan Commelin (Nov 25 2019 at 11:50):

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

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:07):

Did you already do sites and sheaves?

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:08):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:09):

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

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:10):

So I could neither handle abstract nonsense nor concrete examples

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:10):

Can they do either of these in Coq?

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:10):

Je ne sais pas

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:11):

Do we have adjunctions in Lean?

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:11):

Where is this work? It needs to be done.

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:12):

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

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:15):

I mean where is the Lean work?

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:16):

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

view this post on Zulip Kenny Lau (Nov 25 2019 at 12:16):

what is?

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:17):

gluing sheaves on a site.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:35):

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

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:35):

Why?

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:36):

Because that's what he often seems to say

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:36):

Premature optimization and all that....

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:36):

Sometimes generalities are good, sometimes they're not

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:38):

@Kevin Buzzard I've pushed some branches to github

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:38):

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

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:38):

which one should I look at?

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:38):

Don't ask me about how they compare...

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:38):

:D

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:38):

It's been 1 year since I worked on this

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:40):

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

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:42):

I see now we talked about this on the stacks project thread.

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Nov 25 2019 at 12:45):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:47):

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

view this post on Zulip Johan Commelin (Nov 25 2019 at 12:47):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 25 2019 at 13:10):

I agree with Johan's projection of me

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 25 2019 at 14:52):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:
https://www.youtube.com/channel/UCuDrbQmLiT0jkSlMKPN-fsQ

If you are interested in joining the meetings, please register at our webpage (the deadline is extended until November 8th):
https://www.math.ku.dk/english/calendar/events/condensed-mathematics/

The schedule is available on the webpage (all times are in the local Copenhagen time), but other information, like the Zoom links and passwords, will be made available for registered participants only.

We look forward to seeing many of you (though not in person) at the Master Class,

Best wishes,
Lars Hesselholt, Ryomei Iwasa, Markus Land, Piotr Pstragowski


Last updated: May 09 2021 at 10:11 UTC