Theorems · Theorem · category theory

CategoryTheory.HasExactColimitsOfShape.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.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C],
  CategoryTheory.HasExactColimitsOfShape J' C

Transport a HasExactColimitsOfShape along an equivalence of the shape. Note: When C has finite limits, this lemma holds with the equivalence replaced by a final functor, see hasExactColimitsOfShape_of_final 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.HasColimitsOfShapeCategoryTheory.HasExactColimitsOfShape