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. (The commutation of Φ.sheafFiber with colimits is obtained in the file Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean.)

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.instIsSiftedOppositeElementsFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) : IsSifted Φ.fiber.Elementsᵒᵖ

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.

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.

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.

@[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✝ : 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.presheafFiberCocone {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) : Limits.Cocone ((CategoryOfElements.π Φ.fiber).op.comp P)

The (colimit) cocone which defines the fiber of a presheaf.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_ι_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] (P : Functor Cᵒᵖ A) (x : Φ.fiber.Elementsᵒᵖ) : (Φ.presheafFiberCocone P).ι.app x = Φ.toPresheafFiber (Opposite.unop x).fst (Opposite.unop x).snd P

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_pt {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) : (Φ.presheafFiberCocone P).pt = Φ.presheafFiber.obj P

noncomputable def CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberCocone {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) : Limits.IsColimit (Φ.presheafFiberCocone P)

The cocone Φ.presheafFiberCocone P is a colimit.

noncomputable def CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] : shrinkYoneda.{w, v, u}.comp Φ.presheafFiber ≅ Φ.fiber

The isomorphism shrinkYoneda.{w} ⋙ Φ.presheafFiber ≅ Φ.fiber.

theorem CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] {X : C} (x : Φ.fiber.obj X) : Φ.shrinkYonedaCompPresheafFiberIso.inv.app X x = Φ.toPresheafFiber X x (shrinkYoneda.{w, v, u}.obj X) (shrinkYonedaObjObjEquiv.symm (CategoryStruct.id X))

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) : Φ.presheafFiber.map (shrinkYoneda.{w, v, u}.map f) (Φ.shrinkYonedaCompPresheafFiberIso.inv.app X x) = Φ.toPresheafFiber X x (shrinkYoneda.{w, v, u}.obj Y) (shrinkYonedaObjObjEquiv.symm f)

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.

@[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

See also the lemma W_isInvertedBy_presheafFiber in the file Mathlib/CategoryTheory/Sites/Point/Basic.lean which may apply in more cases.

noncomputable def 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.

noncomputable def CategoryTheory.GrothendieckTopology.Point.sheafToPresheafCompPresheafFiberIso {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] : (sheafToPresheaf J A).comp Φ.presheafFiber ≅ Φ.sheafFiber

The fiber functor on sheaves is induced by the fiber functor on presheaves.

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.instPreservesFiniteLimitsFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] : Limits.PreservesFiniteLimits Φ.fiber

noncomputable def CategoryTheory.GrothendieckTopology.Point.isTerminalFiberObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] (T : C) (hT : Limits.IsTerminal T) : Limits.IsTerminal (Φ.fiber.obj T)

The fiber of the terminal object is a terminal object in Type w.

@[implicit_reducible]

noncomputable def CategoryTheory.GrothendieckTopology.Point.uniqueFiberObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] (T : C) (hT : Limits.IsTerminal T) : Unique (Φ.fiber.obj T)

The fiber of the terminal object contains a unique element.

theorem CategoryTheory.GrothendieckTopology.Point.fiber_map_injective_of_mono {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] {U T : C} (f : U ⟶ T) [Mono f] : Function.Injective (Φ.fiber.map f)

theorem CategoryTheory.GrothendieckTopology.Point.subsingleton_fiber_obj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) [LocallySmall.{w, v, u} C] {U T : C} (f : U ⟶ T) [Mono f] (hT : Limits.IsTerminal T) : Subsingleton (Φ.fiber.obj U)

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] : ((Functor.whiskeringRight Cᵒᵖ A B).obj F).comp Φ.presheafFiber ≅ Φ.presheafFiber.comp 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.

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] : (sheafCompose J F).comp Φ.sheafFiber ≅ Φ.sheafFiber.comp 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.

@[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) : (Φ.sheafFiberCompIso F).hom.app X = CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app X.obj) (CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj)))

@[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) : (Φ.sheafFiberCompIso F).inv.app X = CategoryStruct.comp (CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj))) ((Φ.presheafFiberCompIso F).inv.app X.obj)