Points of a site #

Let C be a category equipped with a Grothendieck topology J. In this file, we define the notion of point of the site (C, J), as a structure GrothendieckTopology.Point. Such a Φ : J.Point consists in a functor Φ.fiber : C ⥤ Type w such that the category Φ.fiber.Elements is cofiltered (and initially small) and such that if x : Φ.fiber.obj X and R is a covering sieve of X, then x belongs to the image of some y : Φ.fiber.obj Y by a morphism f : Y ⟶ X which belongs to R. (This definition is essentially the definition of a fiber functor on a site from SGA 4 IV 6.3.)

The fact that Φ.fiber.Elementsᵒᵖ is filtered allows to define Φ.presheafFiber : (Cᵒᵖ ⥤ A) ⥤ A by taking the filtering colimit of the evaluation functors at op X when (X : C, x : F.obj X) varies in Φ.fiber.Elementsᵒᵖ. We define Φ.sheafFiber : Sheaf J A ⥤ A as the restriction of Φ.presheafFiber to the full subcategory of sheaves.

source

structure CategoryTheory.GrothendieckTopology.Point {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) :

Type (max (max u v) (w + 1))

Given J a Grothendieck topology on a category C, a point of the site (C, J) consists of a functor fiber : C ⥤ Type w such that the category fiber.Elements is initally small (which allows defining the fiber functor on presheaves by taking colimits) and cofiltered (so that the fiber functor on presheaves is exact), and such that covering sieves induce jointly surjective maps on fibers (which allows to show that the fibers of a presheaf and its associated sheaf are isomorphic).

fiber : Functor C (Type w)
the fiber functor on the underlying category of the site
isCofiltered : IsCofiltered self.fiber.Elements
initiallySmall : InitiallySmall self.fiber.Elements
jointly_surjective {X : C} (R : Sieve X) (h : R ∈ J X) (x : self.fiber.obj X) : ∃ (Y : C) (f : Y ⟶ X) (_ : R.arrows f) (y : self.fiber.obj Y), self.fiber.map f y = x