Theorems · Theorem · category theory

CategoryTheory.Limits.colimitLimitToLimitColimit_injective

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

This follows the proof from * Borceux, Handbook of categorical algebra 1, Theorem 2.13.4

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.CategoryCategoryTheory.CategorySmallCategoryTheory.IsFilteredFinite