isLimit

Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.isLimit

Lean4

/-- Auxiliary definition for `OneHypercoverFamily.isSheaf_iff`. -/
noncomputable def isLimit [H.IsGenerating] : IsLimit (Cover.multifork ⟨S, J.superset_covering le E.mem₀⟩ P) :=
  Multifork.IsLimit.mk _ (fun F => lift hP hE le F)
    (fun F => by
      rintro ⟨Y, f, hf⟩
      apply fac)
    (fun F m hm => by
      apply hom_ext H P hP S (J.superset_covering le E.mem₀)
      intro Y f hf
      rw [fac _ _ _ _ _ hf]
      exact hm ⟨_, _, hf⟩)

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

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

Разделы

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

Аффилиация

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