Theorems · Definition · category theory

PresheafOfModules.pullbackComp

{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] →
            {F : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
                {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
                  (φ : S ⟶ F.op.comp R) →
                    {G : CategoryTheory.Functor D E} →
                      {T : CategoryTheory.Functor Eᵒᵖ RingCat} →
                        (ψ : R ⟶ G.op.comp T) →
                          [inst_3 : (PresheafOfModules.pushforward φ).IsRightAdjoint] →
                            [inst_4 : (PresheafOfModules.pushforward ψ).IsRightAdjoint] →
                              (PresheafOfModules.pullback φ).comp (PresheafOfModules.pullback ψ) ≅
                                PresheafOfModules.pullback (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))

The composition of two pullback functors on presheaves of modules identifies to the pullback for the composition.

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Cited by

3 results in Mathlib

Foundations

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

Assumes

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