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

• fiber : Functor C (Type w)

  the fiber functor on the underlying category of the site

• isCofiltered : IsCofiltered self.fiber.Elements
• initiallySmall : InitiallySmall self.fiber.Elements
• jointly_surjective {X : C} (R : Sieve X) (h : R ∈ J X) (x : self.fiber.obj X) : ∃ (Y : C) (f : Y ⟶ X) (_ : R.arrows f) (y : self.fiber.obj Y), self.fiber.map f y = x

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] : Limits.HasColimitsOfShape Φ.fiber.Elementsᵒᵖ 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] : HasExactColimitsOfShape Φ.fiber.Elementsᵒᵖ 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] : Functor (Functor Cᵒᵖ A) A

The fiber functor on categories of presheaves that is given by a point of a site.

Equations

• Φ.presheafFiber = ((CategoryTheory.Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A).obj (CategoryTheory.CategoryOfElements.π Φ.fiber).op).comp CategoryTheory.Limits.colim

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) : P.obj (Opposite.op X) ⟶ Φ.presheafFiber.obj P

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

• Φ.toPresheafFiber X x P = CategoryTheory.Limits.colimit.ι ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp P) (Opposite.op ⟨X, x⟩)

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) : f = 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) : (evaluation Cᵒᵖ A).obj (Opposite.op X) ⟶ Φ.presheafFiber

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

• Φ.toPresheafFiberNatTrans X x = { app := Φ.toPresheafFiber X x, naturality := ⋯ }

@[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) : (Φ.toPresheafFiberNatTrans X x).app P = Φ.toPresheafFiber X x P

@[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✝ : ToType (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✝ : ToType (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) : Φ.presheafFiber.obj P ⟶ T

Constructor for morphisms from the fiber of a presheaf.

Equations

• One or more equations did not get rendered due to their size.

@[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) : CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.presheafFiberDesc φ hφ) = φ X 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] : Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (forget A)

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] : Function.Surjective ⇑(ConcreteCategory.hom (Φ.presheafFiber.map 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] : Function.Injective ⇑(ConcreteCategory.hom (Φ.presheafFiber.map 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] : Function.Bijective ⇑(ConcreteCategory.hom (Φ.presheafFiber.map 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] : J.W.IsInvertedBy Φ.presheafFiber

@[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] : Functor (Sheaf J A) A

The fiber functor on the category of sheaves that is given a by a point of a site.

Equations

• Φ.sheafFiber = (CategoryTheory.sheafToPresheaf J A).comp Φ.presheafFiber

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] : (presheafToSheaf J A).comp Φ.sheafFiber ≅ Φ.presheafFiber

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

• One or more equations did not get rendered due to their size.

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] : Limits.PreservesFiniteLimits Φ.presheafFiber

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] : Limits.PreservesFiniteLimits Φ.sheafFiber

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] : Limits.PreservesColimitsOfSize.{w, w, max u v', v', max (max (max u u') v) v', u'} Φ.presheafFiber

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] : Limits.PreservesColimitsOfSize.{w, w, max u v', v', max (max (max u u') v) v', u'} Φ.sheafFiber