Theorems · Definition · algebraic geometry

AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp

{J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] →
              (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
                (s : CategoryTheory.Limits.Cocone F) →
                  (U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ) →
                    s.pt.presheaf.obj U ⟶
                      ((TopCat.Presheaf.pushforward C
                                (CategoryTheory.Limits.colimit.desc
                                  (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
                                  ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).obj
                            (CategoryTheory.Limits.limit
                              (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp)).obj
                        U

Auxiliary definition for AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit.

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.Limits.HasLimitsOfShape