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

We show that if (C, J) has enough points, then so does (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) : (J.over X).Point

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 elements y such that Φ.fiber.map f y = x.

Equations

• Φ.over x = { fiber := CategoryTheory.FunctorToTypes.fromOverFunctor Φ.fiber x, isCofiltered := ⋯, initiallySmall := ⋯, jointly_surjective := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.over_fiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [LocallySmall.{w, v, u} C] (Φ : J.Point) {X : C} (x : Φ.fiber.obj X) : (Φ.over x).fiber = FunctorToTypes.fromOverFunctor Φ.fiber x

theorem CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [LocallySmall.{w, v, u} C] {P : ObjectProperty J.Point} [ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P] [J.WEqualsLocallyBijective (Type w)] [HasSheafify J (Type w)] (hP : P.IsConservativeFamilyOfPoints) (X : C) [HasSheafify (J.over X) (Type w)] : (ofObj fun (ψ : (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X) => ψ.fst.obj.over ψ.snd).IsConservativeFamilyOfPoints

instance CategoryTheory.GrothendieckTopology.instHasEnoughPointsOverOverOfWEqualsLocallyBijectiveHomOfHasSheafifyType {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [LocallySmall.{w, v, u} C] [J.HasEnoughPoints] [J.WEqualsLocallyBijective (Type w)] [HasSheafify J (Type w)] (X : C) [HasSheafify (J.over X) (Type w)] : (J.over X).HasEnoughPoints