Theorems · Theorem · category theory

CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_hom_app

∀ {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)
  (G : CategoryTheory.Functor D E) (A : Type u) [inst_3 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (L : CategoryTheory.GrothendieckTopology E) [inst_4 : F.IsContinuous J K] [inst_5 : G.IsContinuous K L]
  (X : CategoryTheory.Sheaf L A) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuousComp G A J K L).hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj (Opposite.op (G.obj (F.obj (Opposite.unop X_1)))))

Defined in

Mathlib.CategoryTheory.Sites.Continuous

Cited by

0 results in Mathlib

Foundations

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

Assumes

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