Theorems · Theorem · category theory

SheafOfModules.pullback_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {D'' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D''] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_4 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [inst_5 : (SheafOfModules.pushforward φ).IsRightAdjoint]
  {K' : CategoryTheory.GrothendieckTopology D'} {K'' : CategoryTheory.GrothendieckTopology D''}
  {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [inst_6 : G.IsContinuous K K']
  [inst_7 : (F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R')
  [inst_8 : (SheafOfModules.pushforward ψ).IsRightAdjoint] {G' : CategoryTheory.Functor D' D''}
  {R'' : CategoryTheory.Sheaf K'' RingCat} [inst_9 : G'.IsContinuous K' K''] [inst_10 : (G.comp G').IsContinuous K K'']
  [inst_11 : ((F.comp G).comp G').IsContinuous J K''] [inst_12 : (F.comp (G.comp G')).IsContinuous J K'']
  (ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R'')
  [inst_13 : (SheafOfModules.pushforward ψ').IsRightAdjoint],
  (SheafOfModules.pullback φ).isoWhiskerLeft (SheafOfModules.pullbackComp ψ ψ') ≪≫
      SheafOfModules.pullbackComp φ
        (CategoryTheory.CategoryStruct.comp ψ ((G.sheafPushforwardContinuous RingCat K K').map ψ')) =
    ((SheafOfModules.pullback φ).associator (SheafOfModules.pullback ψ) (SheafOfModules.pullback ψ')).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pullbackComp φ ψ) (SheafOfModules.pullback ψ') ≪≫
        SheafOfModules.pullbackComp
          (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ)) ψ'

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsRightAdjointCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsRightAdjointCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsRightAdjoint