Theorems · Theorem · category theory

CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {J' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : CategoryTheory.Category.{v_2, u_2} J'] (e : J ≌ J')
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C],
  CategoryTheory.HasExactLimitsOfShape J' C

Transport a HasExactLimitsOfShape along an equivalence of the shape. Note: When C has finite colimits, this lemma holds with the equivalence replaced by an initial functor, see hasExactLimitsOfShape_of_initial below.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.HasExactLimitsOfShape