topos

Stream: maths

[Edward Ayers]

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]

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]

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

[Johan Commelin]

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

[Edward Ayers]

Yeah I wasn't sure what to call it.

[Johan Commelin]

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

[Edward Ayers]

Yeah feel free to PR and fling issues at us

[Johan Commelin]

Ha, I'm really excited about this!

[Bhavik Mehta]

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]

Johan Commelin said:

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

Voila: https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category/default.lean#L128

[Bhavik Mehta]

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]

Let's hope that refactoring will be smooth

[Bhavik Mehta]

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]

How many SLOC do you have already in this repo?

[Johan Commelin]

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

[Bhavik Mehta]

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

[Edward Ayers]

Johan Commelin said:

How many SLOC do you have already in this repo?

~3000 lines

[Johan Commelin]

SLOC = source lines of code

[Johan Commelin]

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

[Reid Barton]

More like 30

[Reid Barton]

Oh, 1000 / 5, okay.

[Edward Ayers]

Renamed sieve.yank to sieve.pullback.

[Kevin Buzzard]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

And separately a theorem about when image and coimage coincide.

[Scott Morrison]

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

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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]

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

[Scott Morrison]

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

I moved it to locally_cartesian_closed.lean

[Bhavik Mehta]

I haven't yet done much more with it

[Scott Morrison]

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]

Am I missing something?

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

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]

Can you point me to where that is?

[Bhavik Mehta]

in mono_part_is_mono

[Bhavik Mehta]

In pullback_preserves_epi' and prod_map_epi near the end of that proof

[Scott Morrison]

Got it, thanks.

[Bhavik Mehta]

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]

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]

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

[Bas Spitters]

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]

E.g following the treatment in Maclane and Moerdijk

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

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

[Scott Morrison]

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]

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]

Did you tell PTJ?

[Johan Commelin]

Scott Morrison said:

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

:up:

[Patrick Massot]

:up:

[Bhavik Mehta]

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]

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]

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]

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]

I understand nothing from the previous message.

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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]

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]

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]

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

[Reid Barton]

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]

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

[Adam Topaz]

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

[Reid Barton]

You can state it without stalks, too. Exactly.

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Reid Barton]

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]

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

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

[Bhavik Mehta]

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