topos

Stream: new members

[Jon Bannon]

Hello everyone! I'm trying out the Zulip chat for the first time, and trying to build my first lean project. I wanted to do something involving toposes, and so have tried Mehta's topos build found here: https://github.com/b-mehta/topos

I'm getting a lot of "failed to synthesize type class" errors, though. Is this code obsolete (e.g. written for Lean 2?) or are toposes best sought elsewhere? Thanks, in advance!

I see here that evidently sites are already in mathlib...

[Mario Carneiro]

It's definitely not lean 2 code, but lean 3 moves pretty fast so bitrot would not surprise me

[Mario Carneiro]

cc: @Bhavik Mehta

[Bhavik Mehta]

I haven't kept up to date with maintaining this, sorry! It could still build on an earlier version of Lean, it last worked on 3.23.0. Sites are already in mathlib, and I'm pretty sure that's one of the things causing the build errors.

[Kevin Buzzard]

The word topos has two different definitions in mathematics -- which one are you interested in?

[David Michael Roberts]

To clarify: the two options are elementary toposes (finite limits, cartesian closed, subobject classifier) or Grothendieck/sheaf toposes (sheaves on a site), with the latter being a special case of the former. Bhavik's topos.lean takes the first definition.

[Jon Bannon]

Kevin Buzzard said:

The word topos has two different definitions in mathematics -- which one are you interested in?

Sorry everyone! Still slow on the uptake with the chat. I'm interested in Grothendieck toposes (so I may not need the 'topos' file that hasn't been updated.) Thank you all for the warm welcome.

I'm very new to Lean (I've completed natural number game and most of the real analysis "game" and have watched quite a few videos over the past month) and am going to try to formalize a certain topos to continue getting experience with the system. I hope to attend LFTCM at ICERM in July...but hopefully by then will know a bit more. Right now, my code is awful...

[Kevin Buzzard]

Yeah by far the best way to learn how to use Lean is just to dive in and try and make an object which you understand very well mathematically

[Kevin Buzzard]

For example, can you make the function which takes as input a topological space $X$ and spits out the type of all sheaves of types on $X$?

[Kevin Buzzard]

AKA the class of all sheaves of sets on $X$

[Jon Bannon]

Kevin Buzzard said:

Yeah by far the best way to learn how to use Lean is just to dive in and try and make an object which you understand very well mathematically

Thanks! I'm happy to know that I'm not being too reckless by trying to dive in like this! I will try your suggested exercise. Presently I'm doing something that is perhaps even more lowbrow: I'm trying to construct a category consisting of a single object and whose morphisms are given by the multiplicative semigroup of natural numbers. I'm hoping to gain some proficiency with Lean by stepping this up gradually in order to formalize the Connes-Consani Arithmetic Site. I am wondering if geometric morphisms appear anywhere here, yet? I'm particularly looking forward to trying to formalize the points of the associated topos.

(Getting experience using "punit" :laughing: )

Thank you again for the exercise...

[Kevin Buzzard]

We'll have adeles soon enough -- I have a post-doc @María Inés de Frutos Fernández working on them. @Yakov Pechersky is working on tropical geometry. I don't know if we have the completed zeta function but I don't see any obstruction to having it -- I believe we can now do the integrals to define the Gamma function. @Heather Macbeth how far away are we from a holomorphic Gamma function and zeta function on Re(s)>1? We can get categories from partially ordered sets and we have functors. A lot of the stuff is there or pending.

[Jon Bannon]

Kevin Buzzard said:

We'll have adeles soon enough -- I have a post-doc María Inés de Frutos Fernández working on them. Yakov Pechersky is working on tropical geometry. I don't know if we have the completed zeta function but I don't see any obstruction to having it -- I believe we can now do the integrals to define the Gamma function. Heather Macbeth how far away are we from a holomorphic Gamma function and zeta function on Re(s)>1? We can get categories from partially ordered sets and we have functors. A lot of the stuff is there or pending.

Very exciting! So this might be even closer than I had hoped to realizing the identification of the points with the Adèle class space. Great!

[Heather Macbeth]

Kevin Buzzard said:

Heather Macbeth how far away are we from a holomorphic Gamma function and zeta function on Re(s)>1?

The main technical gap (apart from complex analysis) is showing that the compact open topology on a compact space is the same as the sup-norm topology, I think #10967 nearly does this.

[Kevin Buzzard]

We can already define zeta as a bare function on Re(s)>1, and presumably we can do this for Gamma too? Then the questions are proving continuity and holomorphicity.

[Heather Macbeth]

The point I mentioned is what's needed for continuity.

[Heather Macbeth]

And, once Yury's stuff is in, it will also be all that's needed for holomorphicity too.

[Kevin Buzzard]

Nice :-)

[Adam Topaz]

@Jon Bannon formalizing the definition of Connes-Consani's arithmetic site should be a very doable project. Mathlib has the category of sheaves on a site (taking values in any category), so you can get the associated topos. We don't yet have the characterization of Grothendieck topoi, or anything about geometric morphisms, unfortunately.

[Jon Bannon]

Adam Topaz said:

Jon Bannon formalizing the definition of Connes-Consani's arithmetic site should be a very doable project. Mathlib has the category of sheaves on a site (taking values in any category), so you can get the associated topos. We don't yet have the characterization of Grothendieck topoi, or anything about geometric morphisms, unfortunately.

Yes this is really not so bad, my above category problem was easily solved using 'single_obj'. I don't think I'm going to be able to go back to non-Lean mathematics after knowing what this thing can do...how much fun is this?

[Adam Topaz]

Careful... lean will very quickly change how you think about math.

[Jon Bannon]

Adam Topaz said:

Careful... lean will very quickly change how you think about math.

This really feels like some kind of paradigm shift about to happen...

[Arthur Paulino]

Adam Topaz said:

Careful... lean will very quickly change how you think about math.

Do you mean Lean in particular or formalized mathematics?

[Johan Commelin]

Lean is like cocaine: very addictive and it will "very quickly change how you think about math"

[Kevin Buzzard]

I felt just the same thing in 2018, I felt like I wanted to rewrite my maths research papers in this language instead of writing any more new ones

[Jon Bannon]

Kevin Buzzard said:

I felt just the same thing in 2018, I felt like I wanted to rewrite my maths research papers in this language instead of writing any more new ones

Exactly!!! I'm in operator algebras...there is a huge amount to do here in order to just get started formalizing my old papers...

[Kevin Buzzard]

There's a huge amount to do before we can even state the theorems of most of my papers but part of the project right now is to get things like modular forms and automorphic representations defined

[Jon Bannon]

Adam Topaz said:

Jon Bannon formalizing the definition of Connes-Consani's arithmetic site should be a very doable project. Mathlib has the category of sheaves on a site (taking values in any category), so you can get the associated topos. We don't yet have the characterization of Grothendieck topoi, or anything about geometric morphisms, unfortunately.

So @Adam Topaz, it seems that we can easily get the associated topos as you say by something like:

def J := grothendieck_topology.trivial (single_obj ℕ)

def  hatNx := Sheaf J Type*

(I'm new to this type theory approach...so my last line might be very wrong...Connes-Consani want to consider sheaves of sets, but I imagine here that this translates into general types? I'm inferring this from the definition of concrete category in Lean.) So this can definitely at least get started. It looks like we need to develop the ability to talk about structures internal to a topos, is this right? (We have something like the tropical semiring here, but I don't know how to make it internal to the topos.)

[Johan Commelin]

@Jon Bannon Yes, those defs look right to me.

[Johan Commelin]

Note that you can format code on Zulip by using #backticks (← that's a link)

[Johan Commelin]

We don't have much about stuff internal to a topos at the moment. But Adam has developed a bunch about abelian sheaves recently.

[Johan Commelin]

It's been a while since I read Connes-Consani, so I'm not up to speed about what would be needed for that.

[Adam Topaz]

I don't think it's too important but Connes-Consani use $\mathbb{N}^\times$ (as a multiplicative monoid) and you use $\mathbb{N}$ (again as a multiplicative monoid)..

[Jon Bannon]

This might be important, actually. I don't think we want a zero. Do you happen to know where I might find \N^x?

Also, maybe next it would be worth trying to go and repair some of https://github.com/b-mehta/topos/blob/master/src/internal_category.lean?

[Adam Topaz]

To define the structure sheaf, for now you could define it as a sheaf of rings -- we still don't have anything about internal ring objects in a topos

[Adam Topaz]

docs#pnat

[Adam Topaz]

I think (hope) docs#pnat should have a monoid structure..

[Jon Bannon]

Great! 'pnat' worked.

I'll try to define the structure sheaf as a sheaf of rings. Thanks!