Documentation

Mathlib.CategoryTheory.Sites.Types

Grothendieck Topology and Sheaves on the Category of Types #

In this file we define a Grothendieck topology on the category of types, and construct the canonical functor that sends a type to a sheaf over the category of types, and make this an equivalence of categories.

Then we prove that the topology defined is the canonical topology.

A Grothendieck topology associated to the category of all types. A sieve is a covering iff it is jointly surjective.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.discreteSieve_apply (α : Type u) :
    ∀ (x : Type u) (f : x α), (CategoryTheory.discreteSieve α).arrows f = ∃ (x_1 : α), ∀ (y : x), f y = x_1

    The discrete sieve on a type, which only includes arrows whose image is a subsingleton.

    Equations
    Instances For
      theorem CategoryTheory.discreteSieve_mem (α : Type u) :
      CategoryTheory.discreteSieve α CategoryTheory.typesGrothendieckTopology α

      The discrete presieve on a type, which only includes arrows whose domain is a singleton.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.yoneda'_map_val :
        ∀ {X Y : Type u} (f : X Y), (CategoryTheory.yoneda'.map f).val = CategoryTheory.yoneda.map f
        @[simp]
        theorem CategoryTheory.yoneda'_obj_val (α : Type u) :
        (CategoryTheory.yoneda'.obj α).val = CategoryTheory.yoneda.obj α

        The yoneda functor that sends a type to a sheaf over the category of types.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def CategoryTheory.eval (P : CategoryTheory.Functor Type uᵒᵖ (Type u)) (α : Type u) (s : P.obj (Opposite.op α)) (x : α) :

          Given a presheaf P on the category of types, construct a map P(α) → (α → P(*)) for all type α.

          Equations
          Instances For

            Given a sheaf S on the category of types, construct a map (α → S(*)) → S(α) that is inverse to eval.

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

              Given a sheaf S, construct an equivalence S(α) ≃ (α → S(*)).

              Equations
              Instances For
                theorem CategoryTheory.eval_map (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (α : Type u) (β : Type u) (f : β α) (s : S.obj (Opposite.op α)) (x : β) :
                CategoryTheory.eval S β (S.map f.op s) x = CategoryTheory.eval S α s (f x)

                Given a sheaf S, construct an isomorphism S ≅ [-, S(*)].

                Equations
                Instances For

                  Given a sheaf S, construct an isomorphism S ≅ [-, S(*)].

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.typeEquiv_functor_obj_val_map (α : Type u) :
                    ∀ {X Y : Type uᵒᵖ} (f : X Y) (g : Opposite.unop X α) (a : Opposite.unop Y), (CategoryTheory.typeEquiv.functor.obj α).val.map f g a = g (f.unop a)
                    @[simp]
                    theorem CategoryTheory.typeEquiv_functor_map_val_app :
                    ∀ {X Y : Type u} (f : X Y) (Y_1 : Type uᵒᵖ) (g : ((fun (X : Type u) => { obj := fun (Y : Type uᵒᵖ) => Opposite.unop Y X, map := fun {X_1 Y : Type uᵒᵖ} (f : X_1 Y) (g : (fun (Y : Type uᵒᵖ) => Opposite.unop Y X) X_1) => CategoryTheory.CategoryStruct.comp f.unop g, map_id := , map_comp := }) X).obj Y_1) (a : Opposite.unop Y_1), (CategoryTheory.typeEquiv.functor.map f).val.app Y_1 g a = f (g a)
                    @[simp]
                    theorem CategoryTheory.typeEquiv_counitIso_hom_app_val_app (X : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) (X : Type uᵒᵖ) :
                    ∀ (a : (CategoryTheory.yoneda.obj (X✝.val.obj (Opposite.op PUnit.{u + 1} ))).obj X), (CategoryTheory.typeEquiv.counitIso.hom.app X✝).val.app X a = (CategoryTheory.evalEquiv X✝.val (Opposite.unop X)).symm a
                    @[simp]
                    theorem CategoryTheory.typeEquiv_functor_obj_val_obj (α : Type u) (Y : Type uᵒᵖ) :
                    (CategoryTheory.typeEquiv.functor.obj α).val.obj Y = (Opposite.unop Y α)
                    @[simp]
                    theorem CategoryTheory.typeEquiv_unitIso_hom_app (X : Type u) :
                    ∀ (a : (CategoryTheory.Functor.id (Type u)).obj X), CategoryTheory.typeEquiv.unitIso.hom.app X a = fun (x : PUnit.{u + 1} ) => a

                    yoneda' induces an equivalence of category between Type u and SheafOfTypes typesGrothendieckTopology.

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