Library UniMath.CategoryTheory.GrothendieckTopos

Grothendick toposes


  • Definition of Grothendieck topology
    • Grothendieck topologies
    • Precategory of sheaves
  • Grothendieck toposes

Definiton of Grothendieck topology

The following definition is a formalization of the definition in Sheaves in Geometry and Logic, Saunders Mac Lane and Ieke Moerdijk, pages 109 and 110.
Grothendieck topology is a collection J(c) of subobjects of the Yoneda functor, for every object of C, such that:
  • The Yoneda functor y(c) is in J(c).
  • Pullback of a subobject in J(c) along any morphism h : c' --> c is in J(c')
  • If S is a subobject of y(c) such that for all objects c' and all morphisms h : c' --> c in C the pullback of S along h is in J(c'), then S is in J(c).
Section def_grothendiecktopology.

  Variable C : precategory.
  Hypothesis hs : has_homsets C.

A sieve on c is a subobject of the yoneda functor.

Grothendieck topology

  Definition collection_of_sieves : UU := (c : C), hsubtype (sieve c).

  Definition isGrothendieckTopology_maximal_sieve (COS : collection_of_sieves) : UU :=
     (c : C), COS c (Subobjectscategory_ob
                        (functor_category_has_homsets (opp_precat C) HSET has_homsets_HSET)
                        (identity (yoneda C hs c)) (identity_isMonic _)).

  Definition isGrothendieckTopology_stability (COS : collection_of_sieves) : UU :=
     (c c' : C) (h : c' --> c) (s : sieve c),
    COS c s
    COS c' (PullbackSubobject
              (FunctorcategoryPullbacks (opp_precat C) HSET has_homsets_HSET HSET_Pullbacks)
              s (yoneda_morphisms C hs _ _ h)).

  Definition isGrothendieckTopology_transitivity (COS : collection_of_sieves) : UU :=
     (c : C) (s : sieve c),
    (∏ (c' : C) (h : c' --> c),
     COS c' (PullbackSubobject
               (FunctorcategoryPullbacks (opp_precat C) HSET has_homsets_HSET HSET_Pullbacks)
               s (yoneda_morphisms C hs _ _ h))
      COS c s).

  Definition isGrothendieckTopology (COS : collection_of_sieves) : UU :=
    (isGrothendieckTopology_maximal_sieve COS)
      × (isGrothendieckTopology_stability COS)
      × (isGrothendieckTopology_transitivity COS).

  Definition GrothendieckTopology : UU :=
     COS : collection_of_sieves, isGrothendieckTopology COS.

Accessor functions


For some reason I need the following
  Definition Presheaf : UU := functor (opp_precat C) HSET.

  Definition PresheafToFunctor (P : Presheaf) : functor (opp_precat C) HSET := P.

  Definition make_Presheaf (F : functor (opp_precat C) HSET) : Presheaf := F.

This is a formalization of the definition on page 122
  Definition isSheaf (P : Presheaf) (GT : GrothendieckTopology) : UU :=
     (c : C) (S : sieve c) (isCOS : GrothendieckTopology_COS GT c S)
      (τ : nat_trans (sieve_functor S) (PresheafToFunctor P)),
    iscontr ( η : nat_trans (FunctorPrecatObToFunctor (yoneda C hs c)) (PresheafToFunctor P),
                   nat_trans_comp _ _ _ (sieve_nat_trans S) η = τ).

  Lemma isaprop_isSheaf (GT : GrothendieckTopology) (P : Presheaf) : isaprop(isSheaf P GT).
    apply impred_isaprop; intros t.
    apply impred_isaprop; intros S.
    apply impred_isaprop; intros isCOS.
    apply impred_isaprop; intros τ.
    apply isapropiscontr.

The category of sheaves is the full subcategory of presheaves consisting of the presheaves which satisfy the isSheaf proposition.

Definition of Grothendieck topos

Grothendieck topos is a precategory which is equivalent to the category of sheaves on some Grothendieck topology.
Section def_grothendiecktopos.

  Variable C : precategory.
  Hypothesis hs : has_homsets C.

Here (pr1 D) is the precategory which is equivalent to the precategory of sheaves on the Grothendieck topology (pr2 D).
  Definition GrothendieckTopos : UU :=
     D' : ( D : precategory × (GrothendieckTopology C hs),
                  functor (pr1 D) (categoryOfSheaves C hs (pr2 D))),
           (adj_equivalence_of_precats (pr2 D')).

Accessor functions