CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks
theorem CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteWidePullbacks C]
{B : C}, CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Over B)
This theorem states that given a category `C` with all finite wide pullbacks, we can construct finite products in the over category `C/B`. In other words, for any object `B` in `C`, if `C` has finite wide pullbacks (a generalization of pullbacks in category theory), then the over category `C/B` (which consists of arrows in `C` with codomain `B`, with morphisms being commutative triangles) will have finite products (a generalization of the cartesian product in set theory).
More concisely: Given a category `C` with all finite wide pullbacks, the over category `C/B` has finite products for any object `B` in `C`.
|
CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback
theorem CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C},
CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over B)
This theorem states that for any category `C` with pullbacks and any object `B` in `C`, the over category `C/B` possesses binary products. In other words, given a pullback in a category, we can construct a binary product in the over category derived from that category and a specific object within it.
More concisely: For any category with pullbacks `C` and object `B`, the over category `C/B` has binary products.
|
CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks
theorem CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasWidePullbacks C]
{B : C}, CategoryTheory.Limits.HasProducts (CategoryTheory.Over B)
This theorem states that for any category `C` that has wide pullbacks, we can construct products in the over-category `C/B`. In other words, if `C` satisfies the property of having wide pullbacks (meaning that it has a limit for each diagram consisting of an arbitrary set of objects and a specified object from which there is a morphism to each of the other objects), then the over-category `C/B`, which includes all objects from `C` that have morphisms to a specified object `B`, has the ability to form products (which are limits of discrete diagrams).
More concisely: If category `C` has wide pullbacks, then `C/B` has products for any object `B` in `C`.
|
CategoryTheory.Over.over_hasTerminal
theorem CategoryTheory.Over.over_hasTerminal :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C),
CategoryTheory.Limits.HasTerminal (CategoryTheory.Over B)
This theorem states that for any category `C` and any object `B` in `C`, the over category `Over B` has a terminal object. The over category `Over B` is defined as a category consisting of arrows in `C` with codomain `B` and its morphisms are commutative triangles. A terminal object in a category is an object such that there is exactly one morphism from every object in the category to the terminal object. Please note that this construction of a terminal object in the over category is not typically the way terminal objects are defined, for example, it's different from the one given by `over_product_of_widePullback`.
More concisely: For any category `C` and object `B` in `C`, the over category `Over B` has a terminal object.
|
CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit
theorem CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C}
(F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
[inst_1 :
CategoryTheory.Limits.HasLimit (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)],
CategoryTheory.Limits.HasLimit F
This theorem states that for any category `C`, object `B` in `C`, and a functor `F` from a discrete category `J` to the over category of `B`, if there is a limit for the wide pullback diagram formed by applying the functor `F` over the arrows in `B`, then there exists a limit for the functor `F`. In other words, given a category, an object in the category, and a specific kind of functor, under the condition that a certain kind of limit exists, then we can prove that another kind of limit also exists.
More concisely: If `F` is a functor from a discrete category to the over category of an object `B` in a category `C`, and if there exists a limit for the wide pullback diagrams formed by applying `F` over the arrows in `B`, then `F` has a limit in `C`.
|
CategoryTheory.Over.ConstructProducts.over_product_of_widePullback
theorem CategoryTheory.Over.ConstructProducts.over_product_of_widePullback :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C] {B : C},
CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Over B)
The theorem `CategoryTheory.Over.ConstructProducts.over_product_of_widePullback` states that for any type `J`, any category `C` with wide pullbacks (which are a type of limit), and any object `B` in `C`, the over category `C/B` has limits of discrete shape `J`. In other words, if you have a category where you can construct wide pullbacks, then you are able to construct products in the over category of any object in the original category.
More concisely: For any category with wide pullbacks `C` and object `B` in `C`, the over category `C/B` has products indexed by any type `J`.
|