glueMorphismsOverOfLocallyDirected

Mathlib.AlgebraicGeometry.Cover.Directed

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

Lean4

/-- If `𝒰` is a directed open cover of `X`, to glue morphisms `{gᵢ : 𝒰ᵢ ⟶ Y}` over `S` it suffices
to check compatibility with the transition maps. -/
def glueMorphismsOverOfLocallyDirected {S : Scheme.{u}} {X : Over S} (𝒰 : X.left.OpenCover) [Category 𝒰.I₀]
    [𝒰.LocallyDirected] {Y : Over S} (g : ∀ i, 𝒰.X i ⟶ Y.left)
    (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), 𝒰.trans hij ≫ g j = g i) (w : ∀ i, g i ≫ Y.hom = 𝒰.f i ≫ X.hom) : X ⟶ Y :=
  Over.homMk (𝒰.glueMorphismsOfLocallyDirected g h) <|
    by
    apply 𝒰.hom_ext
    intro i
    simp [w]

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

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

Разделы

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

Аффилиация

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