Zulip Chat Archive

Stream: maths

Topic: Topos theory so far


Ken Lee (Mar 19 2021 at 16:27):

Hi, just curious what's the current status of topos theory in Lean?

Kevin Buzzard (Mar 19 2021 at 16:27):

which kind of topos?

Ken Lee (Mar 19 2021 at 16:27):

Grothendieck topos

Kevin Buzzard (Mar 19 2021 at 16:28):

We have the concept of a sheaf on a site, and that's pretty much it. But Bhavik has a load of work on elementary topoi.

Ken Lee (Mar 19 2021 at 16:29):

oh cool! That's presumably on the logic side of things? How about on the geometric side? (E.g. connected morphisms)

Bhavik Mehta (Mar 19 2021 at 17:23):

Ken Lee said:

oh cool! That's presumably on the logic side of things? How about on the geometric side? (E.g. connected morphisms)

Not much on the geometric side - we don't even have geometric morphisms yet! I think they're very much within reach though, and I think it wouldn't be too hard to define a grothendieck topos as a category equivalent to a category of sheaves on a small site, and do geometric morphisms on them


Last updated: Dec 20 2023 at 11:08 UTC