# 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

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 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).
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).
Accessor functions