fac'

Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

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

← MathLib Explorer

English

Auxiliary construction yielding a morphism F.pt → P.obj X in the is-sheaf setup.

Русский

Вспомогательное построение образующее морфизм F.pt → P.obj X в системе is-sheaf.

LaTeX

$$$ lift : F.pt \\to P.obj(Op X)$$$

Lean4

@[reassoc]
theorem fac' (i : E.I₀) : lift hP hE le F ≫ P.map (E.f i).op = F.ι ⟨_, E.f i, le _ (Sieve.ofArrows_mk _ _ _)⟩ :=
  Multifork.IsLimit.fac (hP E hE).some _ _ i

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

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

Разделы

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

Аффилиация

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