Theorems · Theorem · category theory

SheafOfModules.pushforward_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) {K' : CategoryTheory.GrothendieckTopology D'}
  {K'' : CategoryTheory.GrothendieckTopology D''} {G : CategoryTheory.Functor D D'}
  {R' : CategoryTheory.Sheaf K' RingCat} [inst_5 : G.IsContinuous K K']
  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') {G' : CategoryTheory.Functor D' D''}
  {R'' : CategoryTheory.Sheaf K'' RingCat} [inst_6 : G'.IsContinuous K' K''] [inst_7 : (G.comp G').IsContinuous K K'']
  [inst_8 : (F.comp G).IsContinuous J K'] (ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R''),
  (SheafOfModules.pushforward ψ').isoWhiskerLeft (SheafOfModules.pushforwardComp φ ψ) ≪≫
      SheafOfModules.pushforwardComp
        (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ)) ψ' =
    ((SheafOfModules.pushforward ψ').associator (SheafOfModules.pushforward ψ) (SheafOfModules.pushforward φ)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pushforwardComp ψ ψ') (SheafOfModules.pushforward φ) ≪≫
        SheafOfModules.pushforwardComp φ
          (CategoryTheory.CategoryStruct.comp ψ ((G.sheafPushforwardContinuous RingCat K K').map ψ'))

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsContinuous