Theorems · Theorem · category theory

CategoryTheory.constantCommuteCompose_hom_app_hom

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (X : D),
  ((CategoryTheory.constantCommuteCompose J U).hom.app X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).inv
      (CategoryTheory.sheafifyMap J (CategoryTheory.Functor.constComp Cᵒᵖ X U).hom)

Defined in

Mathlib.CategoryTheory.Sites.ConstantSheaf

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.PreservesSheafificationCategoryTheory.GrothendieckTopology.HasSheafCompose