[Merged by Bors] - feat(CategoryTheory/Sites): internal hom of (pre)sheaves #8622
Conversation
joelriou
added
the
awaiting-review
| this `internalHom F G` is the presheaf of types which sends an object `X : C` | ||
| to the type of morphisms between the "restrictions" of `F` and `G` to the category `Over X`. -/ | ||
| @[simps! obj] | ||
| def internalHom : Cᵒᵖ ⥤ Type _ where |
There was a problem hiding this comment.
internalHom sounds a bit strange as it's not valued in the original category A. yoneda feels more appropriate, especially if you show it's functorial in F.
There was a problem hiding this comment.
It should not be too hard to deduce an internal hom in Sheaf J A when A has a limit-preserving, isomorphism-reflecting functor to types though. I'm not sure it's interesting in other cases.
Internal also refers to the fact that it's internal to sheaf categories.
There was a problem hiding this comment.
A itself need to have internal homs, right? Like the category of abelian groups or modules over a CommRing.
There was a problem hiding this comment.
I am not convinced of yoneda as a name, but would presheafHom (and sheafHom for the sheaf version) be ok? (I do not intend to develop the A-valued version soon.)
There was a problem hiding this comment.
I'm fine with either version (internalHom makes sense at least when A is Type _), I agree that yoneda is not a good name.
There was a problem hiding this comment.
I have fixed the name as presheafHom.
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Thanks for the reviews! bors merge |
In this PR, we define a presheaf `presheafHom F G` when `F` and `G` are presheaves `Cᵒᵖ ⥤ A` and show that it is a sheaf when `G` is a sheaf (for a certain Grothendieck topology on `C`). Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
In this PR, we define a presheaf `presheafHom F G` when `F` and `G` are presheaves `Cᵒᵖ ⥤ A` and show that it is a sheaf when `G` is a sheaf (for a certain Grothendieck topology on `C`). Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
In this PR, we define a presheaf
presheafHom F GwhenFandGare presheavesCᵒᵖ ⥤ Aand show that it is a sheaf whenGis a sheaf (for a certain Grothendieck topology onC).