Points of presheaf toposes #

Let C be a category. For the Grothendieck topology ⊥ on C, we know that the category of sheaves with values in A identifies to Cᵒᵖ ⥤ A (see sheafBotEquivalence in the file Mathlib/CategoryTheory/Sites/Sheaf.lean). In this file, we show that any X : C defines a point for this site, and that these points form a conservative family of points.

source

noncomputable def CategoryTheory.GrothendieckTopology.pointBot {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) :

⊥.Point

If X is an object of C, this is the point of the site (C, ⊥) (whose sheaves are presheaves, see sheafBotEquivalence) corresponding to X.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.pointBot_fiber {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) :

(pointBot X).fiber = shrinkYoneda.{w, v, u}.flip.obj (Opposite.op X)

source

noncomputable def CategoryTheory.GrothendieckTopology.pointBotFunctor {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] :

Functor C ⊥.Point

The functor C ⥤ Point.{w} (⊥ : GrothendieckTopology C) which sends X : C to the point corresponding to X.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.pointBotFunctor_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) :

pointBotFunctor.obj X = pointBot X

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.pointBotFunctor_map_hom {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :

(pointBotFunctor.map f).hom = shrinkYoneda.{w, v, u}.flip.map f.op

source

instance CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) (A : Type u_1) [Category.{u_2, u_1} A] [Limits.HasColimitsOfSize.{w, w, u_2, u_1} A] :

IsIso ((pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (CategoryStruct.id X)))

source

noncomputable def CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) (A : Type u_1) [Category.{u_2, u_1} A] [Limits.HasColimitsOfSize.{w, w, u_2, u_1} A] :

(pointBot X).presheafFiber ≅ (evaluation Cᵒᵖ A).obj (Opposite.op X)

The fiber functor (Cᵒᵖ ⥤ A) ⥤ A corresponding to the point of the Grothendieck topology ⊥ attached to an object X : C identifies to the evaluation functor at X.

Equations