toCoverage

Mathlib.CategoryTheory.Sites.Coverage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pretopology.toCoverage

Lean4

/-- Any pretopology is a coverage. -/
def toCoverage [HasPullbacks C] (J : Pretopology C) : Coverage C
    where
  coverings := J
  pullback _ _ f R hR := ⟨R.pullbackArrows f, J.pullbacks _ _ hR, .pullbackArrows f R⟩

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

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

Разделы

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

Аффилиация

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