Conservative families of points

Let J be a Grothendieck topology on a category C. Let P : ObjectProperty J.Point be a family of points. We say that P is a conservative family of points if the corresponding fiber functors Sheaf J (Type w) ⥤ Type w jointly reflect isomorphisms. Under suitable assumptions on the coefficient category A, this implies that the fiber functors Sheaf J A ⥤ A corresponding to the points in P jointly reflect isomorphisms, epimorphisms and monomorphisms, and they are also jointly faithful.

TODO

• Formalize SGA 4 IV 6.5 (a) which characterizes conservative families of points.

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

Let P : ObjectProperty J.Point a family of points of a site (C, J)). We say that it is a conservative family of points if the corresponding fiber functors Sheaf J (Type w) ⥤ Type w jointly reflect isomorphisms.

• jointlyReflectIsomorphisms_type : JointlyReflectIsomorphisms fun (Φ : P.FullSubcategory) => Φ.obj.sheafFiber

theorem CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [Category.{v', u'} A] [LocallySmall.{w, v, u} C] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory A FC] [(forget A).ReflectsIsomorphisms] [Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)] [hJ : J.HasSheafCompose (forget A)] : JointlyReflectIsomorphisms fun (Φ : P.FullSubcategory) => Φ.obj.sheafFiber

Stacks Tag 00YK ((1))

theorem CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [Category.{v', u'} A] [LocallySmall.{w, v, u} C] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory A FC] [(forget A).ReflectsIsomorphisms] [Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)] [hJ : J.HasSheafCompose (forget A)] [AB5OfSize.{w, w, v', u'} A] [Limits.HasFiniteLimits A] : JointlyReflectMonomorphisms fun (Φ : P.FullSubcategory) => Φ.obj.sheafFiber

Stacks Tag 00YL ((1))

theorem CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [Category.{v', u'} A] [LocallySmall.{w, v, u} C] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory A FC] [(forget A).ReflectsIsomorphisms] [Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)] [hJ : J.HasSheafCompose (forget A)] [J.WEqualsLocallyBijective A] [HasSheafify J A] : JointlyReflectEpimorphisms fun (Φ : P.FullSubcategory) => Φ.obj.sheafFiber

Stacks Tag 00YL ((2))

theorem CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [Category.{v', u'} A] [LocallySmall.{w, v, u} C] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory A FC] [(forget A).ReflectsIsomorphisms] [Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)] [hJ : J.HasSheafCompose (forget A)] [AB5OfSize.{w, w, v', u'} A] [Limits.HasFiniteLimits A] : JointlyFaithful fun (Φ : P.FullSubcategory) => Φ.obj.sheafFiber

Stacks Tag 00YL ((3))

class CategoryTheory.GrothendieckTopology.HasEnoughPoints {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Prop

A site has enough points (relatively to a universe w) if it has a w-small conservative family of points.

• exists_objectProperty : ∃ (P : ObjectProperty J.Point), ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P ∧ P.IsConservativeFamilyOfPoints