Topos theory so far

Stream: maths

[Ken Lee]

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

[Kevin Buzzard]

which kind of topos?

[Ken Lee]

Grothendieck topos

[Kevin Buzzard]

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]

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

[Bhavik Mehta]

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