Internal hom of sheaves

In this file, given two sheaves F and G on a site (C, J) with values in a category A, we define a sheaf of types sheafHom F G which sends X : C to the type of morphisms between the restrictions of F and G to the categories Over X.

We first define presheafHom F G when F and G are presheaves Cᵒᵖ ⥤ A and show that it is a sheaf when G is a sheaf.

TODO:

• turn both presheafHom and sheafHom into bifunctors
• for a sheaf of types F, the sheafHom functor from F is right-adjoint to the product functor with F, i.e. for all X and Y, there is a natural bijection (X ⨯ F ⟶ Y) ≃ (X ⟶ sheafHom F Y).
• use these results in order to show that the category of sheaves of types is Cartesian closed

def CategoryTheory.presheafHom {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] (F G : Functor Cᵒᵖ A) : Functor Cᵒᵖ (Type (max (max u v) v'))

Given two presheaves F and G on a category C with values in a category A, this presheafHom 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.

@[simp]

theorem CategoryTheory.presheafHom_obj {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] (F G : Functor Cᵒᵖ A) (X : Cᵒᵖ) : (presheafHom F G).obj X = ((Over.forget (Opposite.unop X)).op.comp F ⟶ (Over.forget (Opposite.unop X)).op.comp G)

theorem CategoryTheory.presheafHom_map_app {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] {F G : Functor Cᵒᵖ A} {X Y Z : C} (f : Z ⟶ Y) (g : Y ⟶ X) (h : Z ⟶ X) (w : CategoryStruct.comp f g = h) (α : (presheafHom F G).obj (Opposite.op X)) : ((presheafHom F G).map g.op α).app (Opposite.op (Over.mk f)) = α.app (Opposite.op (Over.mk h))

Equational lemma for the presheaf structure on presheafHom. It is advisable to use this lemma rather than dsimp [presheafHom] which may result in the need to prove equalities of objects in an Over category.

@[simp]

theorem CategoryTheory.presheafHom_map_app_op_mk_id {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] {F G : Functor Cᵒᵖ A} {X Y : C} (g : Y ⟶ X) (α : (presheafHom F G).obj (Opposite.op X)) : ((presheafHom F G).map g.op α).app (Opposite.op (Over.mk (CategoryStruct.id Y))) = α.app (Opposite.op (Over.mk g))

def CategoryTheory.presheafHomSectionsEquiv {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] (F G : Functor Cᵒᵖ A) : ↑(presheafHom F G).sections ≃ (F ⟶ G)

The sections of the presheaf presheafHom F G identify to morphisms F ⟶ G.

theorem CategoryTheory.PresheafHom.isAmalgamation_iff {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] {F G : Functor Cᵒᵖ A} {X : C} (S : Sieve X) (x : Presieve.FamilyOfElements (presheafHom F G) S.arrows) (hx : x.Compatible) (y : (presheafHom F G).obj (Opposite.op X)) : x.IsAmalgamation y ↔ ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (Opposite.op (Over.mk g)) = (x g hg).app (Opposite.op (Over.mk (CategoryStruct.id Y)))

theorem CategoryTheory.PresheafHom.IsSheafFor.exists_app {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] {F G : Functor Cᵒᵖ A} {X : C} {S : Sieve X} (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → Limits.IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)) (x : Presieve.FamilyOfElements (presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible) (g : Y ⟶ X) : ∃ (φ : F.obj (Opposite.op Y) ⟶ G.obj (Opposite.op Y)), ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryStruct.comp p g)), CategoryStruct.comp φ (G.map p.op) = CategoryStruct.comp (F.map p.op) ((x (CategoryStruct.comp p g) hp).app (Opposite.op (Over.mk (CategoryStruct.id Z))))

noncomputable def CategoryTheory.PresheafHom.IsSheafFor.app {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] {F G : Functor Cᵒᵖ A} {X : C} {S : Sieve X} (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → Limits.IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)) (x : Presieve.FamilyOfElements (presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible) (g : Y ⟶ X) : F.obj (Opposite.op Y) ⟶ G.obj (Opposite.op Y)

Auxiliary definition for presheafHom_isSheafFor.

theorem CategoryTheory.PresheafHom.IsSheafFor.app_cond {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] {F G : Functor Cᵒᵖ A} {X : C} {S : Sieve X} (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → Limits.IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)) (x : Presieve.FamilyOfElements (presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible) (g : Y ⟶ X) {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryStruct.comp p g)) : CategoryStruct.comp (app hG x hx g) (G.map p.op) = CategoryStruct.comp (F.map p.op) ((x (CategoryStruct.comp p g) hp).app (Opposite.op (Over.mk (CategoryStruct.id Z))))

theorem CategoryTheory.presheafHom_isSheafFor {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] (F G : Functor Cᵒᵖ A) {X : C} (S : Sieve X) (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → Limits.IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)) : Presieve.IsSheafFor (presheafHom F G) S.arrows

theorem CategoryTheory.Presheaf.IsSheaf.hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F G : Functor Cᵒᵖ A) (hG : IsSheaf J G) : IsSheaf J (presheafHom F G)

def CategoryTheory.sheafHom' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F G : Sheaf J A) : Functor Cᵒᵖ (Type (max (max u v) v'))

The underlying presheaf of sheafHom F G. It is isomorphic to presheafHom F.1 G.1 (see sheafHom'Iso), but has better definitional properties.

def CategoryTheory.sheafHom'Iso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F G : Sheaf J A) : sheafHom' F G ≅ presheafHom F.val G.val

The canonical isomorphism sheafHom' F G ≅ presheafHom F.1 G.1.

def CategoryTheory.sheafHom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F G : Sheaf J A) : Sheaf J (Type (max (max u v') v))

Given two sheaves F and G on a site (C, J) with values in a category A, this sheafHom F G is the sheaf 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.

def CategoryTheory.sheafHomSectionsEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F G : Sheaf J A) : ↑(sheafHom F G).val.sections ≃ (F ⟶ G)

The sections of the sheaf sheafHom F G identify to morphisms F ⟶ G.

@[simp]

theorem CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {F G : Sheaf J A} (φ : F ⟶ G) (X : Cᵒᵖ) : ↑((sheafHomSectionsEquiv F G).symm φ) X = (J.overPullback A (Opposite.unop X)).map φ