Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.glueMorphisms

{X : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    {Y : AlgebraicGeometry.Scheme} →
      (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) →
        (∀ (x y : 𝒰.I₀),
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) →
          (X ⟶ Y)

Given an open cover of X, and a morphism 𝒰.X x ⟶ Y for each open subscheme in the cover, such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms together into a morphism X ⟶ Y. Note: If X is exactly (defeq to) the gluing of U i, then using Multicoequalizer.desc suffices.

Defined in

Mathlib.AlgebraicGeometry.Gluing

Cited by

10 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound