Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.IsLocallyDirected.glueData

{J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [Quiver.IsThin J] → [Small.{u, w} J] → AlgebraicGeometry.Scheme.GlueData

(Implementation detail) The glue data associated to a locally directed diagram. One usually does not want to use this directly, and instead use the generic colimit API.

Defined in

Mathlib.AlgebraicGeometry.Gluing

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.IsOpenImmersionCategoryTheory.Functor.IsLocallyDirectedQuiver.IsThinSmall