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

@[simp]

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

def CategoryTheory.presheafHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Functor Cᵒᵖ A) (G : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Auxiliary definition for presheafHom_isSheafFor.

Equations

• CategoryTheory.PresheafHom.IsSheafFor.app hG x hx g = ⋯.choose

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

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

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

def CategoryTheory.sheafHom' {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Sheaf J A) (G : CategoryTheory.Sheaf J A) : CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• CategoryTheory.sheafHom'Iso F G = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => CategoryTheory.Sheaf.homEquiv.toIso) ⋯

def CategoryTheory.sheafHom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Sheaf J A) (G : CategoryTheory.Sheaf J A) : CategoryTheory.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.

Equations

• CategoryTheory.sheafHom F G = { val := CategoryTheory.sheafHom' F G, cond := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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