# 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: May 06 2021 at 19:30 UTC