The image of a point by a cocontinuous functor

Let F : C ⥤ D be a cocontinuous functor between sites (C, J) and (D, K). Let Φ be a point of (C, J). In this file, we define a point Φ.map F K of (D, K) and show that there are natural isomorphisms (Φ.map F K).presheafFiber ≅ (Functor.whiskeringLeft _ _ A).obj F.op ⋙ Φ.presheafFiber and (Φ.map F K).sheafFiber ≅ F.sheafPushforwardContinuous A J K ⋙ Φ.sheafFiber (the latter is defined only if F is also continuous).

theorem CategoryTheory.GrothendieckTopology.Point.map_aux {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] ⦃X : D⦄ (R : Sieve X) (hR : R ∈ K X) ⦃u : Φ.fiber.Elements⦄ (f : ((CategoryOfElements.π Φ.fiber).comp F).obj u ⟶ X) : ∃ (Y : D) (g : Y ⟶ X) (_ : R.arrows g) (v : Φ.fiber.Elements) (q : v ⟶ u) (a : F.obj v.fst ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (F.map ↑q) f

noncomputable def CategoryTheory.GrothendieckTopology.Point.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] : K.Point

The image of a point of a site by a cocontinuous functor.

noncomputable def CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : P.obj (Opposite.op (F.obj X)) ⟶ (Φ.map F K).presheafFiber.obj P

Given a cocontinuous functor F : C ⥤ D between sites (C, J) and (D, K), P a presheaf on D, X : C, x : Φ.fiber.obj X, this is the canonical morphism P.obj (op (F.obj X)) ⟶ (Φ.map F K).presheafFiber.obj P, which is part of the colimit cocone presheafFiberMapCocone.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {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 Dᵒᵖ A) : CategoryStruct.comp (P.map (F.map f).op) (Φ.toPresheafFiberMap F K P X x) = Φ.toPresheafFiberMap F K P Y (Φ.fiber.map f x)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {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 Dᵒᵖ A) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z) : CategoryStruct.comp (P.map (F.map f).op) (CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h) = CategoryStruct.comp (Φ.toPresheafFiberMap F K P Y (Φ.fiber.map f x)) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) : CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) ((Φ.map F K).presheafFiber.map g) = CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (Φ.toPresheafFiberMap F K Q X x)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj Q ⟶ Z) : CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (CategoryStruct.comp ((Φ.map F K).presheafFiber.map g) h) = CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (CategoryStruct.comp (Φ.toPresheafFiberMap F K Q X x) h)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_apply {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : Functor Dᵒᵖ 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 (F.obj X)))) : (ConcreteCategory.hom ((Φ.map F K).presheafFiber.map g)) ((ConcreteCategory.hom (Φ.toPresheafFiberMap F K P X x)) x✝) = (ConcreteCategory.hom (Φ.toPresheafFiberMap F K Q X x)) ((ConcreteCategory.hom (g.app (Opposite.op (F.obj X)))) x✝)

noncomputable def CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) : Limits.Cocone ((CategoryOfElements.π Φ.fiber).op.comp (F.op.comp P))

Given a cocontinuous functor F : C ⥤ D between sites (C, J) and (D, K), P a presheaf on D, this is the (colimit) cocone which expresses (Φ.map F K).presheafFiber.obj P as a colimit of P.obj (op (F.obj X)) for X : C, x : Φ.fiber.obj X.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) : (Φ.presheafFiberMapCocone F K P).pt = (Φ.map F K).presheafFiber.obj P

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) (x : Φ.fiber.Elementsᵒᵖ) : (Φ.presheafFiberMapCocone F K P).ι.app x = Φ.toPresheafFiberMap F K P (Opposite.unop x).fst (Opposite.unop x).snd

noncomputable def CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) : Limits.IsColimit (Φ.presheafFiberMapCocone F K P)

Given a cocontinuous functor F : C ⥤ D between sites (C, J) and (D, K), P a presheaf on D, then (Φ.map F K).presheafFiber.obj P is a colimit of P.obj (op (F.obj X)) for X : C, x : Φ.fiber.obj X.

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : Functor Dᵒᵖ A} {T : A} {f g : (Φ.map F K).presheafFiber.obj P ⟶ T} (h : ∀ (X : C) (x : Φ.fiber.obj X), CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f = CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g) : f = g

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} {Φ : J.Point} {F : Functor C D} {K : GrothendieckTopology D} [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : Functor Dᵒᵖ A} {T : A} {f g : (Φ.map F K).presheafFiber.obj P ⟶ T} : f = g ↔ ∀ (X : C) (x : Φ.fiber.obj X), CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f = CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g

noncomputable def CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) : (Φ.map F K).presheafFiber.obj P ≅ Φ.presheafFiber.obj (F.op.comp P)

Relation between the fiber functors on presheaves for the points Φ.map F K and Φ.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (Φ.presheafFiberMapObjIso F K P).hom = Φ.toPresheafFiber X x (F.op.comp P)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : Φ.presheafFiber.obj (F.op.comp P) ⟶ Z) : CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).hom h) = CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (Φ.presheafFiberMapObjIso F K P).inv = Φ.toPresheafFiberMap F K P X x

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z) : CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).inv h) = CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h

noncomputable def CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] (A : Type u'') [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] : (Φ.map F K).presheafFiber ≅ ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op).comp Φ.presheafFiber

Relation between the fiber functors on presheaves for the points Φ.map F K and Φ when F : C ⥤ D is a cocontinuous functor between sites (C, J) and (D, K).

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_hom_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] (A : Type u'') [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : Functor Dᵒᵖ A) : (Φ.presheafFiberMapIso F K A).hom.app X = (Φ.presheafFiberMapObjIso F K X).hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_inv_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] (A : Type u'') [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : Functor Dᵒᵖ A) : (Φ.presheafFiberMapIso F K A).inv.app X = (Φ.presheafFiberMapObjIso F K X).inv

noncomputable def CategoryTheory.GrothendieckTopology.Point.sheafFiberMapIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : GrothendieckTopology C} (Φ : J.Point) (F : Functor C D) (K : GrothendieckTopology D) [F.IsCocontinuous J K] [LocallySmall.{w, v', u'} D] (A : Type u'') [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] [F.IsContinuous J K] : (Φ.map F K).sheafFiber ≅ (F.sheafPushforwardContinuous A J K).comp Φ.sheafFiber

Relation between the fiber functors on presheaves for the points Φ.map F K and Φ when F : C ⥤ D is a cocontinuous and continuous functor between sites (C, J) and (D, K).