Theorems · Theorem · category theory

PresheafOfModules.pushforward_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R)
  {T : CategoryTheory.Functor Eᵒᵖ RingCat} {G : CategoryTheory.Functor D E} (ψ : R ⟶ G.op.comp T)
  {T' : CategoryTheory.Functor E'ᵒᵖ RingCat} {G' : CategoryTheory.Functor E E'} (ψ' : T ⟶ G'.op.comp T'),
  (PresheafOfModules.pushforward ψ').isoWhiskerLeft (PresheafOfModules.pushforwardComp φ ψ) ≪≫
      PresheafOfModules.pushforwardComp (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ)) ψ' =
    ((PresheafOfModules.pushforward ψ').associator (PresheafOfModules.pushforward ψ)
          (PresheafOfModules.pushforward φ)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pushforwardComp ψ ψ')
          (PresheafOfModules.pushforward φ) ≪≫
        PresheafOfModules.pushforwardComp φ (CategoryTheory.CategoryStruct.comp ψ (G.op.whiskerLeft ψ'))

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category