condensed mathematics

Stream: maths

[Kevin Buzzard]

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]

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]

Proof is in lecture 2.

[Kevin Buzzard]

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]

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]

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]

what is condensed mathematics?

[Patrick Massot]

You need to read the paper, or watch the talk

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

oh boy

[Mario Carneiro]

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]

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

[Mario Carneiro]

that seems infinitely more complicated than necessary

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

But we can emulate HoTT in Lean, right?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

https://github.com/gebner/hott3

[Kevin Buzzard]

don't use rewrite, use rwr instead

[Kevin Buzzard]

oh hells bells

[Mario Carneiro]

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

[Kevin Buzzard]

That is exactly what I want to not happen.

[Kenny Lau]

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]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

yes

[Kevin Buzzard]

They add an axiom which formally speaking is inconsistent?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

oh boy

[Mario Carneiro]

There is a @[hott] attribute to automate this

[Mario Carneiro]

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

[Kevin Buzzard]

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

There it is.

[Kevin Buzzard]

It's too strong

[Johan Commelin]

@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]

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

[Mario Carneiro]

is it free?

[Johan Commelin]

It is

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

of course

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

I just want actual infty-cats

[Johan Commelin]

No matter which foundations we have.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

What is said about FLT?

[Mario Carneiro]

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

[Mario Carneiro]

and it's provable in PA

[Kevin Buzzard]

Oh you definitely don't need categories or universes

[Kevin Buzzard]

you can easily modify the proof to avoid them

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

That Goodstein sequence thing is true but not provable in PA

[Kevin Buzzard]

But is that somehow of some higher complexity than FLT?

[Mario Carneiro]

FLT is Pi1, that's probably part of it

[Kevin Buzzard]

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

[Mario Carneiro]

Paris-Harrington is Pi2

[Kevin Buzzard]

Thanks

[Kevin Buzzard]

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

[Kevin Buzzard]

I don't know enough logic

[Mario Carneiro]

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

[Kevin Buzzard]

Most mathematicians have no interest in this sort of thing

[Mario Carneiro]

I'm not familiar with the details of the argument

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

aah, and it has a proof in ZFC too

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

The content, when unravelled, would stretch for miles.

[Kevin Buzzard]

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

[Kevin Buzzard]

In Lean, say.

[Kevin Buzzard]

with all the classical.choice stuff in it

[Mario Carneiro]

yes, absolutely

[Kevin Buzzard]

and the p-adic numbers etc

[Mario Carneiro]

any kind of formalization would be a huge help

[Kevin Buzzard]

and real and complex numbers

[Mario Carneiro]

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

[Kevin Buzzard]

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]

A proof that Shimura-Taniyama-Weil implies FLT.

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

I see.

[Mario Carneiro]

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

[Kevin Buzzard]

Hmm

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but I have no idea how bad PA really is.

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

is this just a rational function?

[Johan Commelin]

No... not exactly

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

I don't get your question

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

i.e. solution set to some polynomial

[Kevin Buzzard]

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

[Kevin Buzzard]

Indeed the equations define a smooth projective curve

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

An elliptic curve is determined by two integers A and B

[Mario Carneiro]

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

[Kevin Buzzard]

and using these integers one can make an explicit field

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

so far so good

[Kevin Buzzard]

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.

[Mario Carneiro]

aha

[Mario Carneiro]

that's PA alright

[Kevin Buzzard]

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

[Kevin Buzzard]

no scratch that

[Kevin Buzzard]

I can make it completely explicit

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

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

[Floris van Doorn]

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]

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]

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]

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

[Jesse Michael Han]

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]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

Stone-Cech is in mathlib. Done by Reid.

[Johan Commelin]

Sites have been done in Coq.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

Did you already do sites and sheaves?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So I could neither handle abstract nonsense nor concrete examples

[Kevin Buzzard]

Can they do either of these in Coq?

[Johan Commelin]

Je ne sais pas

[Kevin Buzzard]

Do we have adjunctions in Lean?

[Kevin Buzzard]

Where is this work? It needs to be done.

[Johan Commelin]

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

[Kevin Buzzard]

I mean where is the Lean work?

[Kevin Buzzard]

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

[Kenny Lau]

what is?

[Kevin Buzzard]

gluing sheaves on a site.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Why?

[Johan Commelin]

Because that's what he often seems to say

[Johan Commelin]

Premature optimization and all that....

[Johan Commelin]

Sometimes generalities are good, sometimes they're not

[Johan Commelin]

@Kevin Buzzard I've pushed some branches to github

[Johan Commelin]

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

[Kevin Buzzard]

which one should I look at?

[Johan Commelin]

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

[Kevin Buzzard]

:D

[Johan Commelin]

It's been 1 year since I worked on this

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

I agree with Johan's projection of me

[Mario Carneiro]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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]

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