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.
We provide a constructor ObjectProperty.IsConservativeFamilyOfPoints.mk'
which allows to verify that a family of points is conservative
using a condition involving covering sieves (SGA 4 IV 6.5 (a)).
structure
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(P : ObjectProperty J.Point)
:
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
Instances For
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)]
[HasWeakSheafify J A]
[Limits.HasProducts 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))
theorem
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective
{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]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)]
[J.WEqualsLocallyBijective (Type w)]
[HasSheafify J (Type w)]
{X Y : Functor Cᵒᵖ A}
(f : X ⟶ Y)
(hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
:
theorem
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{P : ObjectProperty J.Point}
[LocallySmall.{w, v, u} C]
[HasSheafify J (Type w)]
[J.WEqualsLocallyBijective (Type w)]
(hP : P.IsConservativeFamilyOfPoints)
{X : C}
{ι : Type u_1}
[Small.{w, u_1} ι]
{U : ι → C}
(f : (i : ι) → U i ⟶ X)
:
theorem
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{P : ObjectProperty J.Point}
[LocallySmall.{w, v, u} C]
[HasSheafify J (Type w)]
[J.WEqualsLocallyBijective (Type w)]
(hP : P.IsConservativeFamilyOfPoints)
[ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P]
{X : C}
{ι : Type u_1}
{U : ι → C}
(f : (i : ι) → U i ⟶ X)
:
theorem
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{P : ObjectProperty J.Point}
[LocallySmall.{w, v, u} C]
[HasSheafify J (Type w)]
(hP :
∀ ⦃X : C⦄ (S : Sieve X),
(∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj.fiber.obj Y), Φ.obj.fiber.map g y = x) →
S ∈ J X)
:
class
CategoryTheory.GrothendieckTopology.HasEnoughPoints
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
:
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