4 ms·
There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2] [1] https://github.com/l
by 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 agoThanks, 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 agoTo clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.