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.

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.

@[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)

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.

@[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

@[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

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)))

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.

@[simp]

theorem CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso_inv {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] : (pointBotPresheafFiberIso X A).inv = (pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (CategoryStruct.id X))

noncomputable def CategoryTheory.GrothendieckTopology.pointsBot (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : ObjectProperty ⊥.Point

The family of points on the site (C, ⊥) (whose sheaves are presheaves, see sheafBotEquivalence) given by the objects of X.

instance CategoryTheory.GrothendieckTopology.instSmallPointBotPointsBotOfSmall {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [Small.{w, u} C] : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} (pointsBot C)

theorem CategoryTheory.GrothendieckTopology.isConservative_pointsBot (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : (pointsBot C).IsConservativeFamilyOfPoints

instance CategoryTheory.GrothendieckTopology.instHasEnoughPointsBot {C : Type w} [SmallCategory C] : ⊥.HasEnoughPoints