sheafificationIso

Mathlib.CategoryTheory.Sites.Sheafification

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

Lean4

/-- A sheaf `P` is isomorphic to its own sheafification. -/
@[simps]
noncomputable def sheafificationIso (P : Sheaf J D) : P ≅ (presheafToSheaf J D).obj P.val
    where
  hom := ⟨(isoSheafify J P.2).hom⟩
  inv := ⟨(isoSheafify J P.2).inv⟩
  hom_inv_id := by
    ext1
    apply (isoSheafify J P.2).hom_inv_id
  inv_hom_id := by
    ext1
    apply (isoSheafify J P.2).inv_hom_id

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

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

Разделы

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

Аффилиация

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