Library UniMath.CategoryTheory.GrothendieckTopos

Grothendick toposes

Contents

  • 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

Sheaves

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 mk_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).
  Proof.
    apply impred_isaprop; intros t.
    apply impred_isaprop; intros S.
    apply impred_isaprop; intros isCOS.
    apply impred_isaprop; intros τ.
    apply isapropiscontr.
  Qed.

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