Documentation

Mathlib.CategoryTheory.Sites.SheafHom

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:

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.
Instances For

    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.

    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.
    Instances For
      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
      Instances For

        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.
        Instances For

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

          Equations
          Instances For

            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
            Instances For

              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.
              Instances For