Theorems · Theorem · category theory

CategoryTheory.HasExactLimitsOfShape.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_1} D] [inst_2 : CategoryTheory.Category.{v_2, u_2} J]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  [CategoryTheory.HasExactLimitsOfShape J D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.ReflectsFiniteColimits F]
  [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesLimitsOfShape J F],
  CategoryTheory.HasExactLimitsOfShape J C

Pull back a HasExactLimitsOfShape J along a functor which preserves and reflects finite colimits and preserves limits 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.HasLimitsOfShapeCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.HasExactLimitsOfShapeCategoryTheory.Limits.PreservesFiniteColimitsCategoryTheory.Limits.ReflectsFiniteColimitsCategoryTheory.Limits.HasFiniteColimitsCategoryTheory.Limits.PreservesLimitsOfShape