undefined | Better HN

0 pointshackandthink2y ago0 comments

Though I did not find Topos Theory.

0 comments

There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2]

[1] https://github.com/leanprover-community/mathlib4/tree/master...

[2] https://leanprover-community.github.io/blog/posts/lte-final/

hackandthinkOP2y ago

Thanks,

and there is Subobject, which looks like the subobject classifier.

https://github.com/leanprover-community/mathlib4/blob/master...

generalnonsense2y ago

To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.

riccardobrasca2y ago

We don't have any topos theory, that's right. But all the prerequisites are there. If you're interested in working on it I strongly suggest to ask on Zulip.

kevinbuzzard2y ago

Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the community have had great success with that kind of project; one million lines of mathlib was translated from Lean 3 to Lean 4 using a combination of automation and human work)

generalnonsense2y ago

As others said above, `mathlib4` has quite a lot of Sheaf theory, and in particular the category of sheaves of Sets (i.e. Types) over an arbitrary site. In this sense, it is possible to talk about Grothendieck toposes. We don't have the characterization in terms of Giraud's axioms, though.

j / k navigate · click thread line to collapse

0 comments

hiker2y ago

There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2]

[1] https://github.com/leanprover-community/mathlib4/tree/master...

[2] https://leanprover-community.github.io/blog/posts/lte-final/

hackandthinkOP2y ago

Thanks,

and there is Subobject, which looks like the subobject classifier.

https://github.com/leanprover-community/mathlib4/blob/master...

generalnonsense2y ago

To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.

riccardobrasca2y ago

We don't have any topos theory, that's right. But all the prerequisites are there. If you're interested in working on it I strongly suggest to ask on Zulip.

kevinbuzzard2y ago

generalnonsense2y ago

j / k navigate · click thread line to collapse