Theorems · Definition · algebraic geometry

AlgebraicGeometry.PresheafedSpace.componentwiseDiagram

{J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F) → CategoryTheory.Functor Jᵒᵖ C

Given a diagram of PresheafedSpace Cs, its colimit is computed by pushing the sheaves onto the colimit of the underlying spaces, and taking componentwise limit. This is the componentwise diagram for an open set U of the colimit of the underlying spaces.

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimit