Theorems · Theorem · category theory

SheafOfModules.pushforwardNatTrans_app_val_app

∀ {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}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  (α : F ⟶ G) (M : SheafOfModules S) (U : Cᵒᵖ) (x : ↑(((SheafOfModules.pushforward φ).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardNatTrans φ α).app M).val.app U)) x =
    (CategoryTheory.ConcreteCategory.hom (M.val.map (α.app (Opposite.unop U)).op)) x

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Cited by

0 results in Mathlib

Foundations

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

Assumes

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