presheafToSheafCompComposeAndSheafifyIso

Mathlib.CategoryTheory.Sites.PreservesSheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.presheafToSheafCompComposeAndSheafifyIso

Lean4

/-- The canonical isomorphism between `presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F`
and `(whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B` when `F : A ⥤ B`
preserves sheafification. -/
@[simps! inv_app]
noncomputable def presheafToSheafCompComposeAndSheafifyIso :
    presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F ≅ (whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B :=
  (asIso (toPresheafToSheafCompComposeAndSheafify J F)).symm

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

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

Разделы

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

Аффилиация

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