Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected

{S : AlgebraicGeometry.Scheme} →
  {X : CategoryTheory.Over S} →
    (𝒰 : X.left.OpenCover) →
      [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] →
        [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
          {Y : CategoryTheory.Over S} →
            (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) →
              (∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i) →
                (∀ (i : 𝒰.I₀),
                    CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) →
                  (X ⟶ Y)

If 𝒰 is a directed open cover of X, to glue morphisms {gᵢ : 𝒰ᵢ ⟶ Y} over S it suffices to check compatibility with the transition maps.

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirected