Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app

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

Defined in

Mathlib.CategoryTheory.Sites.Point.Comap

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.RepresentablyFlatCategoryTheory.InitiallySmallCategoryTheory.CategoryCategoryTheory.Limits.HasProductsCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsRightAdjointCategoryTheory.Limits.HasColimitsOfSize