Theorems · Definition · category theory

SheafOfModules.pushforwardPushforwardEquivalence

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            (eqv : C ≌ D) →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : eqv.functor.IsContinuous J K] →
                    [inst_3 : eqv.inverse.IsContinuous K J] →
                      (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R) →
                        (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S) →
                          CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.obj =
                              CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom) →
                            CategoryTheory.CategoryStruct.comp φ.hom
                                  (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom)
                                    (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) =
                                CategoryTheory.CategoryStruct.id S.obj →
                              (SheafOfModules R ≌ SheafOfModules S)

If e : C ≌ D, then the pushforwards along e.functor and e.inverse forms an equivalence.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Cited by

2 results in Mathlib

Foundations

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

Assumes

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