CategoryTheory.Limits.hasFiniteProducts_of_hasProducts
theorem CategoryTheory.Limits.hasFiniteProducts_of_hasProducts :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C],
CategoryTheory.Limits.HasFiniteProducts C
This theorem states that if a category has all products, it necessarily has finite products as well. In other words, given a category 'C', if for every type 'J', the category 'C' has limits of shape 'Discrete J' (which essentially means the category has all products), then the category 'C' also has finite products. This is part of the larger field of category theory in mathematics, which is particularly useful in areas like algebra and topology.
More concisely: If a category has all products, then it has finite products.
|
CategoryTheory.Limits.HasFiniteProducts.out
theorem CategoryTheory.Limits.HasFiniteProducts.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteProducts C] (n : ℕ),
CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete (Fin n)) C
This theorem states that for any category `C` which has finite products, given a natural number `n`, the category `C` has limits of shape `CategoryTheory.Discrete (Fin n)`. In other words, it states that in a category with finite products, finite limit objects exist for every natural number `n`. Here, `CategoryTheory.Discrete (Fin n)` describes a category with `n` discrete objects, and the limit of such a category in `C` essentially represents an `n`-ary product in `C`.
More concisely: In a category with finite products, for every natural number n, there exists an n-ary product as the limit of the discrete category with n objects.
|
CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts
theorem CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C],
CategoryTheory.Limits.HasFiniteCoproducts C
The theorem `CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts` states that if a category `C` has all coproducts (which is a particular type of colimit), then it also has finite coproducts. In other words, the existence of coproducts for all indexing categories in `C` implies the existence of coproducts for finite indexing categories in `C`.
More concisely: If a category has all coproducts, then it has finite coproducts.
|
CategoryTheory.Limits.HasFiniteCoproducts.out
theorem CategoryTheory.Limits.HasFiniteCoproducts.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteCoproducts C]
(n : ℕ), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C
The theorem `CategoryTheory.Limits.HasFiniteCoproducts.out` states that for any natural number `n`, and for any category `C` that has all finite coproducts, `C` also has colimits of shape `CategoryTheory.Discrete (Fin n)`. In the language of category theory, a coproduct is the categorical dual of a product, and colimits generalize the coproduct. Specifically, in this context, `CategoryTheory.Discrete (Fin n)` refers to the discrete category on `n` objects. Therefore, this theorem essentially asserts that in a category with all finite coproducts, we can also form all finite "discrete" colimits.
More concisely: In a category with finite coproducts, it has finite discrete colimits.
|