## Stream: maths

### Topic: topos

#### Edward Ayers (Mar 09 2020 at 16:10):

Dear all, in the growing Cambridge Lean User Group; @Bhavik Mehta , @Wojciech Nawrocki , @Thomas Read and I have started building a topos theory library which we now think might be worth mentioning.

https://github.com/b-mehta/topos

So far the highlights are: Grothendieck topologies, subobject classifiers, binary products implies finite products, cartesian closed categories and lemmas about pullbacks and the over category. Some of it might already be floating around in mathlib branches or hidden repos, so we ought to coordinate with everyone else to make sure we don't reprove the wheel. Some people who might be interested: @Scott Morrison @Reid Barton @Johan Commelin .

#### Reid Barton (Mar 09 2020 at 16:11):

Oh wow, I was going to start working on a very similar list of things last week but then I got sick instead. Good timing I guess?

#### Johan Commelin (Mar 09 2020 at 16:14):

Should https://github.com/b-mehta/topos/blob/master/src/sieve.lean#L135 be called pullback?

#### Johan Commelin (Mar 09 2020 at 16:14):

Or maybe comap, if you want to be particularly mathlibby.

#### Edward Ayers (Mar 09 2020 at 16:15):

Yeah I wasn't sure what to call it.

#### Johan Commelin (Mar 09 2020 at 16:15):

I'm quite sure that https://github.com/b-mehta/topos/blob/master/src/to_mathlib.lean are in mathlib already

#### Edward Ayers (Mar 09 2020 at 16:17):

Yeah feel free to PR and fling issues at us

#### Bhavik Mehta (Mar 09 2020 at 16:18):

Johan Commelin said:

Should https://github.com/b-mehta/topos/blob/master/src/sieve.lean#L135 be called pullback?

Yeah this was my vote too!

#### Johan Commelin (Mar 09 2020 at 16:22):

Johan Commelin said:

I'm quite sure that https://github.com/b-mehta/topos/blob/master/src/to_mathlib.lean are in mathlib already

#### Bhavik Mehta (Mar 09 2020 at 16:27):

Ah damn, we do have some similar/duplicated work - https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/limits/shapes/images.lean vs https://github.com/b-mehta/topos/blob/master/src/over.lean#L419

#### Johan Commelin (Mar 09 2020 at 16:38):

Let's hope that refactoring will be smooth

#### Bhavik Mehta (Mar 09 2020 at 16:40):

Yeah it doesn't seem too bad actually - it seems like my version should just form a nice instance of the new class

#### Johan Commelin (Mar 09 2020 at 16:41):

How many SLOC do you have already in this repo?

#### Johan Commelin (Mar 09 2020 at 16:41):

Please consider PRing the parts that you think have become reasonably stable.

#### Bhavik Mehta (Mar 09 2020 at 16:43):

(Assuming S means stable), my guess is that about a third to half of it right now

#### Edward Ayers (Mar 09 2020 at 16:45):

Johan Commelin said:

How many SLOC do you have already in this repo?

~3000 lines

#### Johan Commelin (Mar 09 2020 at 16:45):

SLOC = source lines of code

#### Johan Commelin (Mar 09 2020 at 16:46):

3000 lines * (1/3) = 1000. That's already 5 PR's that you have there.

More like 30

#### Reid Barton (Mar 09 2020 at 16:47):

Oh, 1000 / 5, okay.

#### Edward Ayers (Mar 09 2020 at 17:06):

Renamed sieve.yank to sieve.pullback.

#### Kevin Buzzard (Mar 09 2020 at 17:26):

I'm sure the advice from the perfectoid crew would be: strongly consider starting to make PR's to mathlib right now. Stuff changes. As mathlib changes your code will begin to break, and then it's your problem to fix it. If it's in mathlib then it gets fixed by the person who broke it instead (and it's often much easier for them to fix it because they almost always know exactly how they broke it, and indeed they just fixed the ten other parts of mathlib which broke for the same reason).

#### Scott Morrison (Mar 09 2020 at 19:09):

@Bhavik Mehta, this is all great, and I would encourage lots of PRs to mathlib!

#### Scott Morrison (Mar 09 2020 at 19:10):

Let me know if you want to discuss coordination, or any advice on what size chunks to split things into.

#### Scott Morrison (Mar 09 2020 at 19:12):

I'm curious about your definition of image, however. Is this not the "regular coimage", rather than the image? (They often coincide, so this is more of a naming problem than a content problem.)

#### Scott Morrison (Mar 09 2020 at 19:17):

The naming scheme, at least on the wikipedia page, is that "regular image" is the dual of what you've written, i.e. the equalizer of the pair of maps from Y into the pushout of X mapping via f into two copies of Y.

#### Scott Morrison (Mar 09 2020 at 19:18):

There's then a theorem someone ought to prove about when image and regular_image coincide.

#### Scott Morrison (Mar 09 2020 at 19:18):

And separately a theorem about when image and coimage coincide.

#### Scott Morrison (Mar 09 2020 at 19:19):

And then further the easier formulas you can use in abelian categories, etc.

#### Bhavik Mehta (Mar 09 2020 at 19:30):

Scott Morrison said:

I'm curious about your definition of image, however. Is this not the "regular coimage", rather than the image? (They often coincide, so this is more of a naming problem than a content problem.)

The "image" as I defined it satisfies the "general definition" of image given on wikipedia - proved on lines 535 and below. My goal here was to get to the 'image' as would be useful in a topos (or in my case a locally cartesian closed category with (refl.) coequalizers), so I've used something more like the regular category definition

#### Scott Morrison (Mar 09 2020 at 19:32):

I wonder if we should just simplify matters; throw out mine and just use yours.

#### Bhavik Mehta (Mar 09 2020 at 19:34):

As far as I can tell they should be able to coexist - I've shown that a LCCC with coequalizers has_images. I think the only real change that needs to be made to your code is to change the instance on L195 to a def

#### Bhavik Mehta (Mar 09 2020 at 19:35):

I should also add to Ed's message that contributions from anyone are more than welcome!

#### Scott Morrison (Mar 14 2020 at 15:57):

@Bhavik Mehta, have you done anything more with your definition of image? I noticed it's disappeared from the spot in your repository it used to be, and I can't find it now.

#### Bhavik Mehta (Mar 14 2020 at 15:57):

I moved it to locally_cartesian_closed.lean

#### Bhavik Mehta (Mar 14 2020 at 15:58):

I haven't yet done much more with it

#### Scott Morrison (Mar 14 2020 at 15:58):

Looking back at the history, I'm not sure you actually proved everything yet that the coequalizer of pullbuck definition actually satisfies the general universal property.

#### Scott Morrison (Mar 14 2020 at 15:58):

Am I missing something?

#### Bhavik Mehta (Mar 14 2020 at 15:59):

I think you are - I'll find the line number

#### Bhavik Mehta (Mar 14 2020 at 16:00):

https://github.com/b-mehta/topos/blob/master/src/locally_cartesian_closed.lean#L287

#### Bhavik Mehta (Mar 14 2020 at 16:00):

Specifically I constructed the regular coimage, and proved that in a locally cartesian closed category with coequalizers it coincides with the image

#### Bhavik Mehta (Mar 14 2020 at 16:03):

mono_part_is_mono establishes that my image is a mono_factorisation, image_is_smallest_subobject is the definition of is_image.lift and smallest_subobject_factors shows is_image.lift_fac'

#### Scott Morrison (Mar 14 2020 at 16:03):

Great. It would be nice to separate things out a bit, and identify explicitly at what point you're using the LCC condition.

#### Scott Morrison (Mar 14 2020 at 16:04):

Can you point me to where that is?

#### Bhavik Mehta (Mar 14 2020 at 16:04):

in mono_part_is_mono

#### Bhavik Mehta (Mar 14 2020 at 16:05):

In pullback_preserves_epi' and prod_map_epi near the end of that proof

Got it, thanks.

#### Bhavik Mehta (Mar 14 2020 at 16:06):

I should say that I wrote all this with the ultimate end-goal of getting to epi-mono factorisation in a topos, so I didn't care too much about what conditions were used where since we'd eventually have them all anyway

#### Bhavik Mehta (Mar 14 2020 at 16:07):

I think a better way of doing this would be to define a regular category and show that an LCC with refl. coeqs is regular

#### Bhavik Mehta (Mar 14 2020 at 16:08):

(and regular categories also generalise abelian categories which is I think what your end goal is?)

#### Bas Spitters (Mar 18 2020 at 11:44):

It may be interesting to translate some of the work on boolean valued models by @Floris van Doorn to topos theory, and perhaps generalize it to Heyting valued models.

#### Bas Spitters (Mar 18 2020 at 11:45):

E.g following the treatment in Maclane and Moerdijk

#### Bhavik Mehta (Mar 18 2020 at 13:32):

Yeah, I would like to get most of chapters 4-6 of MM

#### Bhavik Mehta (Mar 26 2020 at 20:53):

For those interested, we've effectively got the first milestone in this project! Pare's theorem: that a category with finite limits and power objects has finite colimits. Along the way, we've also now got the reflexive (or crude) monadicity theorem and creation of limits (it's sorry-free but still a bit messy, so it's in this branch)

#### Scott Morrison (Mar 27 2020 at 05:22):

PR, PR, PR, before it's too late. :-)

#### Scott Morrison (Mar 27 2020 at 05:24):

There's an art to keeping a bolus of development work going, making sure to balance the rates at which material enters and leaves (digested into mathlib).

#### Bhavik Mehta (Apr 30 2020 at 15:19):

Next milestone! We now have the Fundamental Theorem of Topos Theory, that every topos is locally cartesian closed and that every logical functor with a left adjoint has a right adjoint, as well as the adjoint lifting theorem. This covers almost all of A2.2 of the Elephant (plus stuff from A2.1 and A2.3), about 80% of chapter 4 of MM, and about 95% of the examinable topos theory part of the Part III category theory course (I think this means about 85% of the course is in lean now). Next up: sheaves and sheafification.

#### Kevin Buzzard (Apr 30 2020 at 16:12):

Did you tell PTJ?

#### Johan Commelin (Apr 30 2020 at 16:45):

Scott Morrison said:

PR, PR, PR, before it's too late. :-)

:up:

:up:

#### Bhavik Mehta (Aug 11 2020 at 13:53):

Sheaves and sheafification are done! For sheaves on a local operator, the special case of sheaves on a site and the very special case of sheaves on a space, take a look here: https://github.com/b-mehta/topos/blob/master/src/applications/sheaves_on_a_site.lean, in which I show the sheafification functor for set-valued presheaves, show it's left adjoint to forgetful and that it preserves finite products and equalizers. I don't yet claim I have a convenient API for them yet, but I used only abstract category theory and topos theory to get this geometric result (that is, no ++ construction), and I've tried to express the result without using any topos theory at all. One cute curiosity here is that while I did use choice to make the special case of sheaves on a site, it suffices to only use unique choice - meaning that sheafification can be constructed using only unique choice. Before people yell at me to PR to mathlib, I'm already starting to create PRs (and of course there have been quite a few already)

#### Bhavik Mehta (Aug 11 2020 at 13:58):

I should report also that virtually everything was just translating the maths proof to Lean, there were very few cases where I got stuck because Lean or mathlib was complaining - it was because I didn't understand the maths well enough. In particular the uses of choice happened exactly where they do in textbooks.

#### Patrick Massot (Aug 11 2020 at 14:04):

Does it mean you can handle actual sheaves, or is it still abstract? For instance, can you define the presheaf of constant functions on a topological space and prove its sheafification is the sheaf of locally constant functions?

#### Bhavik Mehta (Aug 11 2020 at 14:06):

I'm in the process of trying to make it a bit more concrete, but the former is automatic because I have the same definition of presheaf as in mathlib, and I think the latter is possible up to isomorphism of sheaves

#### Patrick Massot (Aug 11 2020 at 14:08):

I understand nothing from the previous message.

#### Bhavik Mehta (Aug 11 2020 at 14:20):

I'll try to be clearer: It's mostly abstract but it's possible to define a concrete sheaf, and I'm working on making this easier (especially in the case of spaces). It's easy to define the presheaf of constant functions on a space: I used the definition of presheaf that's already in mathlib. It's also possible to show that the presheaf of locally constant functions on a space is a sheaf (but again, not yet as convenient as I'd like), and to show that this sheaf is the sheafification of the presheaf of constant functions, I'm not yet sure but I'll think about it

#### Kevin Buzzard (Aug 11 2020 at 17:07):

Do you have anything like "if you are in the sheaf, then you are locally in the presheaf"?

#### Bhavik Mehta (Aug 11 2020 at 17:09):

I'm not sure I understand this question...

#### Kevin Buzzard (Aug 11 2020 at 17:10):

There's a map from P(U) -> S(U) where S is the sheafification of P. For topological spaces, if f is in S(U) then you can cover U with U_i and prove that f_i is in the image of P(U_i).

#### Kevin Buzzard (Aug 11 2020 at 17:10):

I have no idea to what extent this generalises but it is an easy way to see that the sheafification of constant functions is locally constant functions.

#### Adam Topaz (Aug 11 2020 at 17:16):

Kevin Buzzard said:

Do you have anything like "if you are in the sheaf, then you are locally in the presheaf"?

Isn't this the universal property of the sheafification?

#### Reid Barton (Aug 11 2020 at 17:19):

It's more like the fact that the map to the sheafification is a local isomorphism

#### Reid Barton (Aug 11 2020 at 17:20):

I guess if you think the universal property is "the universal thing with a local isomorphism from the presheaf" then yes. :upside_down:

#### Adam Topaz (Aug 11 2020 at 17:20):

Okay, yeah. So for spaces it boils down to the fact that the stalks are the same.

#### Adam Topaz (Aug 11 2020 at 17:21):

And I guess the same would be true in general if you have enough points.

#### Reid Barton (Aug 11 2020 at 17:21):

You can state it without stalks, too. Exactly.

#### Adam Topaz (Aug 11 2020 at 17:23):

What I originally meant by "universal property" was the fact that sheafification is a left adjoint, i.e. the freest sheaf with a map from the presheaf.

#### Reid Barton (Aug 11 2020 at 17:24):

Then I don't see how to conclude this fact directly (though of course it must be a consequence somehow)

#### Adam Topaz (Aug 11 2020 at 17:25):

You're right. But the sheafification is constructed as some fancy limit, right? So something can be said in general.

#### Reid Barton (Aug 11 2020 at 17:25):

The statement I had in mind is, I think, what you get by interpreting "is an isomorphism" in the sheaf semantics, but if you unwind it, it becomes:
(surjectivity) for every U and section s of the sheafification over U, there exists a cover V -> U and a section of the original presheaf which maps to the restriction/pullback of s to V
(injectivity) ...

#### Scott Morrison (Aug 12 2020 at 00:12):

@Bhavik Mehta, what do you think we should do with #3605 / #3608 (I know it's not compiling right now, but it's an easy fix)?

#3608 is the PR with Johan where we check that the presheaf of continuous functions on a space forms a sheaf. From what I understand, this work needs to be done at some point, and it's just a question of which definitions we connect it to.

Does it make sense to just have lots of (proved equivalent) versions of the sheaf condition? i.e. merge #3605, finish #3608, done in terms of that statement of the sheaf condition, and then as your PRs come along prove the equivalence between the sheaf-condition-on-a-site and the condition on a space given in #3605?

#### Scott Morrison (Aug 12 2020 at 00:13):

Alternatively, we could just ditch #3605 and redo #3608.

#### Bhavik Mehta (Aug 12 2020 at 00:15):

Scott Morrison said:

Does it make sense to just have lots of (proved equivalent) versions of the sheaf condition? i.e. merge #3605, finish #3608, done in terms of that statement of the sheaf condition, and then as your PRs come along prove the equivalence between the sheaf-condition-on-a-site and the condition on a space given in #3605?

I think this makes the most sense - since the sheaf condition is subsingleton anyway my feeling is that as long as we have equivalent versions which are useful for both practically doing geometry and proving abstract results, it should all work fine

Last updated: May 18 2021 at 06:15 UTC