Points of Over sites #
Given a point Φ of a site (C, J), an object X : C, and x : Φ.fiber.obj X,
we define a point Φ.over x of the site (Over X, J.over X).
def
CategoryTheory.GrothendieckTopology.Point.over
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
[LocallySmall.{w, v, u} C]
(Φ : J.Point)
{X : C}
(x : Φ.fiber.obj X)
:
Given a point Φ of a site (C, J), an object X : C, and x : Φ.fiber.obj X,
this is the point of the site (Over X, J.over X) such that the fiber of
an object of Over X corresponding to a morphism f : Y ⟶ X identifies
to subtype of Φ.fiber.obj Y consisting of elemnts y such
that Φ.fiber.map f y = x.