Commit 2023-11-28 18:08 c28500a0

View on Github →

feat(CategoryTheory/Sites): internal hom of (pre)sheaves (#8622) 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).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Over.lean

Modified Mathlib/CategoryTheory/Over.lean

Created Mathlib/CategoryTheory/Sites/SheafHom.lean

added theorem CategoryTheory.Presheaf.IsSheaf.hom

added theorem CategoryTheory.PresheafHom.IsSheafFor.app_cond

added theorem CategoryTheory.PresheafHom.IsSheafFor.exists_app

added theorem CategoryTheory.PresheafHom.isAmalgamation_iff

added def CategoryTheory.presheafHom

added def CategoryTheory.presheafHomSectionsEquiv

added theorem CategoryTheory.presheafHom_isSheafFor

added theorem CategoryTheory.presheafHom_map_app

added theorem CategoryTheory.presheafHom_map_app_op_mk_id

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean