Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.Scheme.Cover.ColimitGluingData

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.IsStableUnderBaseChange] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst : CategoryTheory.Category.{v_1, u_1} J] →
          CategoryTheory.Functor J (P.Over ⊤ S) →
            (𝒰 : S.OpenCover) →
              [inst : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] →
                [AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] → Type (max (max (u + 1) u_1) u_2)

The data required for gluing the colimits of the Dᵢ : J ⥤ P.Over ⊤ (𝒰.X i).

Defined in

Mathlib.AlgebraicGeometry.ColimitsOver

Cited by

26 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.CategoryCategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirected