Points of a site #
Let C be a category equipped with a Grothendieck topology J. In this file,
we define the notion of point of the site (C, J), as a
structure GrothendieckTopology.Point. Such a Φ : J.Point consists
in a functor Φ.fiber : C ⥤ Type w such that the category Φ.fiber.Elements
is cofiltered (and initially small) and such that if x : Φ.fiber.obj X
and R is a covering sieve of X, then x belongs to the image
of some y : Φ.fiber.obj Y by a morphism f : Y ⟶ X which belongs to R.
(This definition is essentially the definition of a fiber functor on a site
from SGA 4 IV 6.3.)
The fact that Φ.fiber.Elementsᵒᵖ is filtered allows to define
Φ.presheafFiber : (Cᵒᵖ ⥤ A) ⥤ A by taking the filtering colimit
of the evaluation functors at op X when (X : C, x : F.obj X) varies in
Φ.fiber.Elementsᵒᵖ. We define Φ.sheafFiber : Sheaf J A ⥤ A as the
restriction of Φ.presheafFiber to the full subcategory of sheaves.
Under certain assumptions, we show that if A is concrete and
P ⟶ Q is a locally bijective morphism between presheaves,
then the induced morphism on fibers is a bijection. It follows
that not only Φ.sheafFiber : Sheaf J A ⥤ A is the restriction of
Φ.presheafFiber but it may also be thought as a localization
of this functor with respect to the class of morphisms J.W.
In particular, the fiber of a presheaf identifies to the fiber of
its associated sheaf.
Under suitable assumptions on the target category A, we show that
both Φ.presheafFiber and Φ.sheafFiber commute with finite limits
and with arbitrary colimits.
structure
CategoryTheory.GrothendieckTopology.Point
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
:
Type (max (max u v) (w + 1))
Given J a Grothendieck topology on a category C, a point of the site (C, J)
consists of a functor fiber : C ⥤ Type w such that the category fiber.Elements
is initially small (which allows defining the fiber functor on presheaves by
taking colimits) and cofiltered (so that the fiber functor on presheaves is exact),
and such that covering sieves induce jointly surjective maps on fibers (which
allows to show that the fibers of a presheaf and its associated sheaf are isomorphic).
the fiber functor on the underlying category of the site
- isCofiltered : IsCofiltered self.fiber.Elements
- initiallySmall : InitiallySmall self.fiber.Elements
Instances For
instance
CategoryTheory.GrothendieckTopology.Point.instHasColimitsOfShapeOppositeElementsFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
:
instance
CategoryTheory.GrothendieckTopology.Point.instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[LocallySmall.{w, v, u} C]
[AB5OfSize.{w, w, v', u'} A]
[Limits.HasFiniteLimits A]
:
noncomputable def
CategoryTheory.GrothendieckTopology.Point.presheafFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
:
The fiber functor on categories of presheaves that is given by a point of a site.
Equations
Instances For
noncomputable def
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
(X : C)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
:
Given a point Φ of a site (C, J), X : C and x : Φ.fiber.obj X, this
is the canonical map P.obj (op X) ⟶ Φ.presheafFiber.obj P.
Equations
Instances For
theorem
CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P : Functor Cᵒᵖ A}
{T : A}
{f g : Φ.presheafFiber.obj P ⟶ T}
(h :
∀ (X : C) (x : Φ.fiber.obj X),
CategoryStruct.comp (Φ.toPresheafFiber X x P) f = CategoryStruct.comp (Φ.toPresheafFiber X x P) g)
:
theorem
CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext_iff
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{Φ : J.Point}
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P : Functor Cᵒᵖ A}
{T : A}
{f g : Φ.presheafFiber.obj P ⟶ T}
:
f = g ↔ ∀ (X : C) (x : Φ.fiber.obj X),
CategoryStruct.comp (Φ.toPresheafFiber X x P) f = CategoryStruct.comp (Φ.toPresheafFiber X x P) g
noncomputable def
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
(X : C)
(x : Φ.fiber.obj X)
:
Given a point Φ of a site (C, J), X : C and x : Φ.fiber.obj X,
this is the map P.obj (op X) ⟶ Φ.presheafFiber.obj P for any P : Cᵒᵖ ⥤ A
as a natural transformation.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans_app
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
(X : C)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
:
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{X Y : C}
(f : X ⟶ Y)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
:
CategoryStruct.comp (P.map f.op) (Φ.toPresheafFiber X x P) = Φ.toPresheafFiber Y (Φ.fiber.map f x) P
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_assoc
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{X Y : C}
(f : X ⟶ Y)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
{Z : A}
(h : Φ.presheafFiber.obj P ⟶ Z)
:
CategoryStruct.comp (P.map f.op) (CategoryStruct.comp (Φ.toPresheafFiber X x P) h) = CategoryStruct.comp (Φ.toPresheafFiber Y (Φ.fiber.map f x) P) h
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{X Y : C}
(f : X ⟶ Y)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
{F : A → A → Type uF}
{carrier : A → Type w_1}
{instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory A F]
(x✝ : carrier (P.obj (Opposite.op Y)))
:
(ConcreteCategory.hom (Φ.toPresheafFiber X x P)) ((ConcreteCategory.hom (P.map f.op)) x✝) = (ConcreteCategory.hom (Φ.toPresheafFiber Y (Φ.fiber.map f x) P)) x✝
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P Q : Functor Cᵒᵖ A}
(g : P ⟶ Q)
(X : C)
(x : Φ.fiber.obj X)
:
CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.presheafFiber.map g) = CategoryStruct.comp (g.app (Opposite.op X)) (Φ.toPresheafFiber X x Q)
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P Q : Functor Cᵒᵖ A}
(g : P ⟶ Q)
(X : C)
(x : Φ.fiber.obj X)
{Z : A}
(h : Φ.presheafFiber.obj Q ⟶ Z)
:
CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryStruct.comp (Φ.presheafFiber.map g) h) = CategoryStruct.comp (g.app (Opposite.op X)) (CategoryStruct.comp (Φ.toPresheafFiber X x Q) h)
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P Q : Functor Cᵒᵖ A}
(g : P ⟶ Q)
(X : C)
(x : Φ.fiber.obj X)
{F : A → A → Type uF}
{carrier : A → Type w_1}
{instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory A F]
(x✝ : carrier (P.obj (Opposite.op X)))
:
(ConcreteCategory.hom (Φ.presheafFiber.map g)) ((ConcreteCategory.hom (Φ.toPresheafFiber X x P)) x✝) = (ConcreteCategory.hom (Φ.toPresheafFiber X x Q)) ((ConcreteCategory.hom (g.app (Opposite.op X))) x✝)
noncomputable def
CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P : Functor Cᵒᵖ A}
{T : A}
(φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T))
(hφ :
∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X), CategoryStruct.comp (P.map f.op) (φ X x) = φ Y (Φ.fiber.map f x) := by
cat_disch)
:
Constructor for morphisms from the fiber of a presheaf.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P : Functor Cᵒᵖ A}
{T : A}
(φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T))
(hφ :
∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X), CategoryStruct.comp (P.map f.op) (φ X x) = φ Y (Φ.fiber.map f x) := by
cat_disch)
(X : C)
(x : Φ.fiber.obj X)
:
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc_assoc
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
{P : Functor Cᵒᵖ A}
{T : A}
(φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T))
(hφ :
∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X), CategoryStruct.comp (P.map f.op) (φ X x) = φ Y (Φ.fiber.map f x) := by
cat_disch)
(X : C)
(x : Φ.fiber.obj X)
{Z : A}
(h : T ⟶ Z)
:
CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryStruct.comp (Φ.presheafFiberDesc φ hφ) h) = CategoryStruct.comp (φ X x) h
instance
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{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)]
[LocallySmall.{w, v, u} C]
:
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
{P : Functor Cᵒᵖ A}
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
(p : ToType (Φ.presheafFiber.obj P))
:
∃ (X : C) (x : Φ.fiber.obj X) (z : ToType (P.obj (Opposite.op X))),
(ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z = p
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective₂
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
{P : Functor Cᵒᵖ A}
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
(p₁ p₂ : ToType (Φ.presheafFiber.obj P))
:
∃ (X : C) (x : Φ.fiber.obj X) (z₁ : ToType (P.obj (Opposite.op X))) (z₂ : ToType (P.obj (Opposite.op X))),
(ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = p₁ ∧ (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ = p₂
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_eq_iff'
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
{P : Functor Cᵒᵖ A}
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
(X : C)
(x : Φ.fiber.obj X)
(z₁ z₂ : ToType (P.obj (Opposite.op X)))
:
(ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ ↔ ∃ (Y : C) (f : Y ⟶ X) (y : Φ.fiber.obj Y),
Φ.fiber.map f y = x ∧ (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
{P Q : Functor Cᵒᵖ A}
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
(f : P ⟶ Q)
[Presheaf.IsLocallySurjective J f]
:
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_injective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
{P Q : Functor Cᵒᵖ A}
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
(f : P ⟶ Q)
[Presheaf.IsLocallyInjective J f]
:
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
{P Q : Functor Cᵒᵖ A}
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
(f : P ⟶ Q)
[Presheaf.IsLocallyInjective J f]
[Presheaf.IsLocallySurjective J f]
:
theorem
CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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)]
[LocallySmall.{w, v, u} C]
[J.WEqualsLocallyBijective A]
[(forget A).ReflectsIsomorphisms]
:
@[reducible, inline]
noncomputable abbrev
CategoryTheory.GrothendieckTopology.Point.sheafFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
:
The fiber functor on the category of sheaves that is given a by a point of a site.
Equations
Instances For
instance
CategoryTheory.GrothendieckTopology.Point.instIsIsoMapFunctorOppositePresheafFiberToSheafify
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
(P : Functor Cᵒᵖ A)
[HasWeakSheafify J A]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
[J.WEqualsLocallyBijective A]
[(forget A).ReflectsIsomorphisms]
:
IsIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J P))
noncomputable def
CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
(A : Type u')
[Category.{v', u'} A]
[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]
[HasWeakSheafify J A]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
[J.WEqualsLocallyBijective A]
[(forget A).ReflectsIsomorphisms]
:
The fiber functor on sheaves is obtained from the fiber functor on presheaves
by localization with respect to the class of morphisms J.W.
Equations
Instances For
instance
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[LocallySmall.{w, v, u} C]
[Limits.HasFiniteLimits A]
[AB5OfSize.{w, w, v', u'} A]
:
instance
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[LocallySmall.{w, v, u} C]
[Limits.HasFiniteLimits A]
[AB5OfSize.{w, w, v', u'} A]
:
instance
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeFunctorOppositePresheafFiber
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
:
instance
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeSheafSheafFiberOfHasSheafifyOfWEqualsLocallyBijectiveOfReflectsIsomorphismsOfPreservesFilteredColimitsOfSizeForgetOfLocallySmall
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
[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]
[HasSheafify J A]
[J.WEqualsLocallyBijective A]
[(forget A).ReflectsIsomorphisms]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)]
[LocallySmall.{w, v, u} C]
:
noncomputable def
CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
{B : Type u''}
[Category.{v'', u''} B]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v'', u''} B]
(F : Functor A B)
[LocallySmall.{w, v, u} C]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
:
If Φ is a point of a site and F : A ⥤ B is a functor which preserves
filtered colimits, then taking fibers of presheaves at Φ commutes with F.
Equations
Instances For
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
{B : Type u''}
[Category.{v'', u''} B]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v'', u''} B]
(F : Functor A B)
[LocallySmall.{w, v, u} C]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
(X : C)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
:
CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) ((Φ.presheafFiberCompIso F).hom.app P) = F.map (Φ.toPresheafFiber X x P)
theorem
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app_assoc
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
{B : Type u''}
[Category.{v'', u''} B]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v'', u''} B]
(F : Functor A B)
[LocallySmall.{w, v, u} C]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
(X : C)
(x : Φ.fiber.obj X)
(P : Functor Cᵒᵖ A)
{Z : B}
(h : F.obj (Φ.presheafFiber.obj P) ⟶ Z)
:
CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) (CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app P) h) = CategoryStruct.comp (F.map (Φ.toPresheafFiber X x P)) h
noncomputable def
CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
{B : Type u''}
[Category.{v'', u''} B]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v'', u''} B]
(F : Functor A B)
[LocallySmall.{w, v, u} C]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
[J.HasSheafCompose F]
:
If Φ is a point of a site and F : A ⥤ B is a functor which preserves
filtered colimits, then taking fibers of sheaves at Φ commutes with F.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
{B : Type u''}
[Category.{v'', u''} B]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v'', u''} B]
(F : Functor A B)
[LocallySmall.{w, v, u} C]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
[J.HasSheafCompose F]
(X : Sheaf J A)
:
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
(Φ : J.Point)
{A : Type u'}
[Category.{v', u'} A]
{B : Type u''}
[Category.{v'', u''} B]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v'', u''} B]
(F : Functor A B)
[LocallySmall.{w, v, u} C]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
[J.HasSheafCompose F]
(X : Sheaf J A)
:
def
CategoryTheory.GrothendieckTopology.Point.comap
{C : Type u_2}
{D : Type u_3}
[Category.{v_1, u_2} C]
[Category.{v_2, u_3} D]
{J : GrothendieckTopology C}
{K : GrothendieckTopology D}
(F : Functor C D)
[RepresentablyFlat F]
(H : CoverPreserving J K F)
(Φ : K.Point)
[InitiallySmall (F.comp Φ.fiber).Elements]
:
J.Point
If F : C ⥤ D is a representably flat and cover preserving functor between sites, then
any point on D induces a point on C by precomposing the fiber functor with F.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Point.comap_fiber
{C : Type u_2}
{D : Type u_3}
[Category.{v_1, u_2} C]
[Category.{v_2, u_3} D]
{J : GrothendieckTopology C}
{K : GrothendieckTopology D}
(F : Functor C D)
[RepresentablyFlat F]
(H : CoverPreserving J K F)
(Φ : K.Point)
[InitiallySmall (F.comp Φ.fiber).Elements]
: