IsSheafOpensLeCover

Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.IsSheafOpensLeCover

Lean4

/-- An equivalent formulation of the sheaf condition
(which we prove equivalent to the usual one below as
`isSheaf_iff_isSheafOpensLeCover`).

A presheaf is a sheaf if `F` sends the cone `(opensLeCoverCocone U).op` to a limit cone.
(Recall `opensLeCoverCocone U`, has cone point `iSup U`,
mapping down to any `V` which is contained in some `U i`.)
-/
def IsSheafOpensLeCover : Prop :=
  ∀ ⦃ι : Type w⦄ (U : ι → Opens X), Nonempty (IsLimit (F.mapCone (opensLeCoverCocone U).op))

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

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

Разделы

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

Аффилиация

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