Inverse image of a point by a continuous functor

Let F : C ⥤ D be a representably flat continuous functor between sites (C, J) and (D, K). Let Φ be a point of (D, K). Assume hF : CoverPreserving J K F. In this file, we define a point Φ.comap F hF of the site (C, J) and construct an isomorphism (Φ.comap F hF).sheafFiber ≅ F.sheafPullback A J K ⋙ Φ.sheafFiber.

def CategoryTheory.GrothendieckTopology.Point.comap {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (Φ : K.Point) (F : Functor C D) [RepresentablyFlat F] {J : GrothendieckTopology C} (hF : CoverPreserving J K F) [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

• Φ.comap F hF = { fiber := F.comp Φ.fiber, isCofiltered := ⋯, initiallySmall := ⋯, jointly_surjective := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.comap_fiber {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (Φ : K.Point) (F : Functor C D) [RepresentablyFlat F] {J : GrothendieckTopology C} (hF : CoverPreserving J K F) [InitiallySmall (F.comp Φ.fiber).Elements] : (Φ.comap F hF).fiber = F.comp Φ.fiber

noncomputable def CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctorCompSheafPushforwardContinuous {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (Φ : K.Point) (F : Functor C D) [RepresentablyFlat F] {J : GrothendieckTopology C} (hF : CoverPreserving J K F) [InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [Category.{v, u_3} A] [Limits.HasProducts A] [F.IsContinuous J K] : Φ.skyscraperSheafFunctor.comp (F.sheafPushforwardContinuous A J K) ≅ (Φ.comap F hF).skyscraperSheafFunctor

Given a continuous functor F : C ⥤ D between sites (C, J) and (D, K), and a point Φ of (D, K), this is the isomorphism between Φ.skyscraperSheafFunctor ⋙ F.sheafPushforwardContinuous A J K and (Φ.comap F hF).skyscraperSheafFunctor.

Equations

• Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A = CategoryTheory.Iso.refl (Φ.skyscraperSheafFunctor.comp (F.sheafPushforwardContinuous A J K))

noncomputable def CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (Φ : K.Point) (F : Functor C D) [RepresentablyFlat F] {J : GrothendieckTopology C} (hF : CoverPreserving J K F) [InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [Category.{v, u_3} A] [Limits.HasProducts A] [F.IsContinuous J K] [(F.sheafPushforwardContinuous A J K).IsRightAdjoint] [Limits.HasColimitsOfSize.{w, w, v, u_3} A] : (Φ.comap F hF).sheafFiber ≅ (F.sheafPullback A J K).comp Φ.sheafFiber

Given a continuous functor F : C ⥤ D between sites (C, J) and (D, K), and a point Φ of (D, K), the fiber functor on sheaves of the point Φ.comap F hF on (C, J) identifies to the composition F.sheafPullback A J K ⋙ Φ.sheafFiber.

Equations

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

theorem CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (Φ : K.Point) (F : Functor C D) [RepresentablyFlat F] {J : GrothendieckTopology C} (hF : CoverPreserving J K F) [InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [Category.{v, u_3} A] [Limits.HasProducts A] [F.IsContinuous J K] [(F.sheafPushforwardContinuous A J K).IsRightAdjoint] [Limits.HasColimitsOfSize.{w, w, v, u_3} A] (X : Sheaf J A) : (Φ.sheafFiberComapIso F hF A).hom.app X = CategoryStruct.comp ((Φ.comap F hF).presheafFiber.map ((F.sheafAdjunctionContinuous A J K).unit.app X).hom) (CategoryStruct.comp ((Φ.comap F hF).presheafFiber.map ((F.sheafPushforwardContinuous A J K).map (Φ.skyscraperSheafAdjunction.unit.app ((F.sheafPullback A J K).obj X))).hom) (CategoryStruct.comp ((Φ.comap F hF).presheafFiber.map ((Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A).hom.app (Φ.presheafFiber.obj ((F.sheafPullback A J K).obj X).obj)).hom) ((Φ.comap F hF).skyscraperSheafAdjunction.counit.app (Φ.presheafFiber.obj ((F.sheafPullback A J K).obj X).obj))))

theorem CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (Φ : K.Point) (F : Functor C D) [RepresentablyFlat F] {J : GrothendieckTopology C} (hF : CoverPreserving J K F) [InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [Category.{v, u_3} A] [Limits.HasProducts A] [F.IsContinuous J K] [(F.sheafPushforwardContinuous A J K).IsRightAdjoint] [Limits.HasColimitsOfSize.{w, w, v, u_3} A] (X : Sheaf J A) : (Φ.sheafFiberComapIso F hF A).inv.app X = CategoryStruct.comp (Φ.presheafFiber.map ((F.sheafPullback A J K).map ((Φ.comap F hF).skyscraperSheafAdjunction.unit.app X)).hom) (CategoryStruct.comp (Φ.presheafFiber.map ((F.sheafPullback A J K).map ((Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A).inv.app ((Φ.comap F hF).presheafFiber.obj X.obj))).hom) (CategoryStruct.comp (Φ.presheafFiber.map ((F.sheafAdjunctionContinuous A J K).counit.app (Φ.skyscraperSheafFunctor.obj ((Φ.comap F hF).presheafFiber.obj X.obj))).hom) (Φ.skyscraperSheafAdjunction.counit.app ((Φ.comap F hF).presheafFiber.obj X.obj))))