4 ms·

Everything I can think of and more of what I'll ever need: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory https://github.c

Everything I can think of and more of what I'll ever need: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory https://github.com/leanprover-community/mathlib4/tree/master...

hackandthink 3y ago
Though I did not find Topos Theory.
- hiker 3y 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/Mathlib/CategoryTheory/Sites https://github.com/leanprover-community/mathlib4/tree/master... [2] https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/
  - hackandthink 3y ago
    Thanks, and there is Subobject, which looks like the subobject classifier. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Subobject/Basic.lean https://github.com/leanprover-community/mathlib4/blob/master...
    - generalnonsense 3y ago
      To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.
- riccardobrasca 3y 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.
  - kevinbuzzard 3y ago
    Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src 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)
- generalnonsense 3y 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.

hackandthink 3y ago

Though I did not find Topos Theory.

hiker 3y 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/Mathlib/CategoryTheory/Sites https://github.com/leanprover-community/mathlib4/tree/master... [2] https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/
- hackandthink 3y ago
  Thanks, and there is Subobject, which looks like the subobject classifier. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Subobject/Basic.lean https://github.com/leanprover-community/mathlib4/blob/master...
  - generalnonsense 3y ago
    To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.
riccardobrasca 3y 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.
- kevinbuzzard 3y ago
  Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src 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)
generalnonsense 3y 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.