CategoryTheory.Limits.comp_lim_obj_ext
theorem CategoryTheory.Limits.comp_lim_obj_ext :
∀ {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] {j : J}
{G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))}
(x y : (G.comp CategoryTheory.Limits.lim).obj j),
(∀ (k : K), CategoryTheory.Limits.limit.π (G.obj j) k x = CategoryTheory.Limits.limit.π (G.obj j) k y) → x = y
This theorem, `CategoryTheory.Limits.comp_lim_obj_ext`, states that for any categories `J` and `K`, and for any functor `G` from `J` to the category of functors from `K` to the category of types, if we have two objects `x` and `y` in the image of `j` under the composition of `G` and the limit functor, and if for all objects `k` in `K` the morphism from the limit of the functor `G.obj j` to `k` applied to `x` is equal to the same morphism applied to `y`, then `x` is equal to `y`. In other words, this is a uniqueness property for objects in the image of the composition of a functor with the limit functor, in terms of how they map to the limits of the functors in the image of `j`.
More concisely: If `G` is a functor from category `J` to Functors from `K` to Types, `j : J`, `x` and `y` are objects in the image of `G.obj j` under the limit functor, and for all `k` in `K`, the limit morphism from `G.obj j` to `k` maps `x` to the same image as it maps `y`, then `x` is equal to `y`.
|
CategoryTheory.Limits.colimitLimitToLimitColimit_injective
theorem 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)) [inst_3 : CategoryTheory.IsFiltered K] [inst_4 : Finite J],
Function.Injective (CategoryTheory.Limits.colimitLimitToLimitColimit F)
This theorem, referenced from Borceux's "Handbook of categorical algebra 1", Theorem 2.13.4, states that for any types `J` and `K` which are categories, and for a small `K`, given a functor `F` from the product of `J` and `K` to some type `v`, if `K` is filtered and `J` is finite, then the function `colimitLimitToLimitColimit` applied to `F` is injective. In other words, if two inputs to `colimitLimitToLimitColimit F` produce the same output, then those two inputs must have been the same. This result is particularly important in the study of category theory where concepts of limits and colimits are central.
More concisely: For a small, filtered category `K` and a finite category `J`, the functor `colimitLimitToLimitColimit` from `Functor (J × K) → Type` to `Type` is injective when applied to any functor `F` from the product of `J` and `K` to some type.
|
CategoryTheory.Limits.colimitLimitToLimitColimit_surjective
theorem 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))
[inst_4 : CategoryTheory.IsFiltered K],
Function.Surjective (CategoryTheory.Limits.colimitLimitToLimitColimit F)
This theorem, named `CategoryTheory.Limits.colimitLimitToLimitColimit_surjective` and referencing Theorem 2.13.4 from Borceux's Handbook of Categorical Algebra 1, states that for any given types `J` and `K`, where `J` forms a small category and `K` is a category, and `K` is small and `J` has a finite number of objects (is a fincategory), then for any functor `F` from the product of `J` and `K` to some type `v`, and assuming that `K` is a filtered category, the function `colimitLimitToLimitColimit` applied to `F` is surjective.
In more mathematical terms, this means that for each element in the codomain of this function, there exists at least one element in the domain such that the function maps this element to the given element in the codomain.
More concisely: For any small finitary functor from the product of a small category J with a filtered category K to a type, the colimit-limit to colimit functor is surjective.
|