Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
            {𝒰 : S.OpenCover} →
              [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] →
                [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                  AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 →
                    (i : 𝒰.I₀) →
                      CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))

The cocones on the Dᵢ.

Defined in

Mathlib.AlgebraicGeometry.ColimitsOver

Cited by

16 results in Mathlib

Foundations

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

Assumes

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