New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(category_theory/sites): sheaves on types #5259
Conversation
kckennylau
commented
Dec 6, 2020
src/category_theory/sites/types.lean
Outdated
|
||
In this file we define a grothendieck topology on the category of types, | ||
and construct the canonical function that sends a type to a sheaf over | ||
the category of types. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you actually construct this function? I think a better description would be to say something like the yoneda presheaf for any type is a sheaf (or to actually make a function which takes types to sheaves).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@kckennylau ⬆️ what do you think?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Now I have actually constructed the functor and the induced equivalence of categories.
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
src/category_theory/sites/types.lean
Outdated
@@ -54,6 +54,11 @@ theorem is_sheaf_yoneda' {α : Type u} : is_sheaf types_grothendieck_topology (y | |||
by { convert this, exact rfl }, | |||
λ f hf, funext $ λ y, by convert congr_fun (hf _ (hs y)) punit.star⟩ | |||
|
|||
/-- The yoneda functor that sends a type to a sheaf over the category of types -/ | |||
def yoneda' : Type u ⥤ Sheaf types_grothendieck_topology := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you add @[simps] to this, and show that composing this with the forgetful functor Sheaf => Presheaf is yoneda?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Pull request successfully merged into master. Build succeeded: |