instOverBind

Mathlib.AlgebraicGeometry.Cover.Over

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

Lean4

instance {X : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) (𝒱 : ∀ x, (𝒰.X x).Cover (precoverage P)) [X.Over S] [𝒰.Over S]
    [∀ x, (𝒱 x).Over S] : Cover.Over S (𝒰.bind 𝒱)
    where
  over := fun ⟨i, j⟩ ↦ inferInstanceAs <| ((𝒱 i).X j).Over S
  isOver_map := fun ⟨i, j⟩ ↦ { comp_over := by simp }

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

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

Разделы

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

Аффилиация

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