pushforwardContinuousSheafificationCompatibility

Mathlib.CategoryTheory.Sites.CoverLifting

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility

Lean4

/-- The natural isomorphism exhibiting compatibility between pushforward and sheafification. -/
def pushforwardContinuousSheafificationCompatibility [G.IsContinuous J K] :
    (whiskeringLeft _ _ A).obj G.op ⋙ presheafToSheaf J A ≅ presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K :=
  ((G.op.ranAdjunction A).comp (sheafificationAdjunction J A)).leftAdjointUniq
    ((sheafificationAdjunction K A).comp (G.sheafAdjunctionCocontinuous A J K))
      /- Implementation: This is primarily used to prove the lemma
      `pullbackSheafificationCompatibility_hom_app_val`. -/

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru