Theorems · Definition · algebraic geometry

AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit

{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] →
          (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
            CategoryTheory.Functor J
              (TopCat.Presheaf C
                  (CategoryTheory.Limits.colimit (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))))ᵒᵖ

Given a diagram of presheafed spaces, we can push all the presheaves forward to the colimit X of the underlying topological spaces, obtaining a diagram in (Presheaf C X)ᵒᵖ.

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShape