Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.hasColimit_of_locallyDirected

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange] [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 𝒰],
  (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)) →
    ∀
      [∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
          CategoryTheory.Limits.PreservesColimitsOfShape J
            (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
      [∀ (i : 𝒰.I₀),
          CategoryTheory.Limits.HasColimit (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))]
      [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [AlgebraicGeometry.IsZariskiLocalAtTarget P],
      CategoryTheory.Limits.HasColimit D

Defined in

Mathlib.AlgebraicGeometry.ColimitsOver

Cited by

0 results in Mathlib

Foundations

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

Assumes

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