Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitGluedCocone

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                      [inst_5 :
                          ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                            CategoryTheory.Limits.PreservesColimitsOfShape J
                              (CategoryTheory.MorphismProperty.Over.pullback P ⊤
                                (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))] →
                        [inst_6 : Quiver.IsThin 𝒰.I₀] →
                          [inst_7 : Small.{u, u_2} 𝒰.I₀] →
                            [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P] →
                              CategoryTheory.Limits.IsColimit d.gluedCocone

The glued cocone is colimiting.

Defined in

Mathlib.AlgebraicGeometry.ColimitsOver

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.CategoryCategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirectedCategoryTheory.Limits.PreservesColimitsOfShapeQuiver.IsThinSmallAlgebraicGeometry.IsZariskiLocalAtTarget