Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected

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

If 𝒰 is a directed open cover of X, to glue morphisms {gᵢ : 𝒰ᵢ ⟶ Y} it suffices to check compatibility with the transition maps. See OpenCover.isColimitCoconeOfLocallyDirected for this result stated in the language of colimits.

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirected