Theorems · Theorem · category theory

CategoryTheory.HasExactColimitsOfShape.domain_of_functor

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_1, u_2} J] [inst_2 : CategoryTheory.Category.{v_2, u_1} D]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  [CategoryTheory.HasExactColimitsOfShape J D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.ReflectsFiniteLimits F]
  [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesColimitsOfShape J F],
  CategoryTheory.HasExactColimitsOfShape J C

Pull back a HasExactColimitsOfShape J along a functor which preserves and reflects finite limits and preserves colimits of shape J

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.HasExactColimitsOfShapeCategoryTheory.Limits.PreservesFiniteLimitsCategoryTheory.Limits.ReflectsFiniteLimitsCategoryTheory.Limits.HasFiniteLimitsCategoryTheory.Limits.PreservesColimitsOfShape