Theorems · Theorem · category theory

CategoryTheory.Limits.colimitLimitToLimitColimit_surjective

∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] [inst_3 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v))
  [CategoryTheory.IsFiltered K],
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))

This follows the proof from Borceux, Handbook of categorical algebra 1, Theorem 2.13.4 although with different names.

Defined in

Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.CategorySmallCategoryTheory.FinCategoryCategoryTheory.IsFiltered