pretopology

Mathlib.CategoryTheory.Sites.MorphismProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.pretopology

Lean4

/-- If `P` is a multiplicative morphism property which is stable under base change on a category
`C` with pullbacks, then `P` induces a pretopology, where coverings are given by presieves whose
elements satisfy `P`. -/
@[simps! toPrecoverage]
def pretopology (P : MorphismProperty C) [P.IsMultiplicative] [P.IsStableUnderBaseChange] : Pretopology C :=
  (precoverage P).toPretopology

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

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

Разделы

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

Аффилиация

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