toPresieveOver

Mathlib.AlgebraicGeometry.Sites.Small

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Cover.toPresieveOver

Lean4

/-- The presieve defined by a `P`-cover of `S`-schemes. -/
def toPresieveOver {X : Over S} (𝒰 : Cover.{u} (precoverage P) X.left) [𝒰.Over S] : Presieve X :=
  Presieve.ofArrows (fun i ↦ (𝒰.X i).asOver S) (fun i ↦ (𝒰.f i).asOver S)

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

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

Разделы

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

Аффилиация

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