toPresieveOverProp

Mathlib.AlgebraicGeometry.Sites.Small

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

Lean4

/-- The presieve defined by a `P`-cover of `S`-schemes with `Q`. -/
def toPresieveOverProp {X : Q.Over ⊤ S} (𝒰 : Cover.{u} (precoverage P) X.left) [𝒰.Over S] (h : ∀ j, Q (𝒰.X j ↘ S)) :
    Presieve X :=
  Presieve.ofArrows (fun i ↦ (𝒰.X i).asOverProp S (h i)) (fun i ↦ (𝒰.f i).asOverProp S)

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

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

Разделы

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

Аффилиация

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