CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial
theorem CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
[inst_2 : CategoryTheory.Limits.HasInitial C], CategoryTheory.Limits.HasFiniteCoproducts C
This theorem states that if a category `C` possesses an initial object and binary coproducts, then `C` has finite coproducts. In the language of category theory, an initial object is an object in `C` that has a unique morphism to any other object in `C`. A binary coproduct is a coproduct, or a type of limit, for a pair of objects, while finite coproducts extend this to any finite set of objects. Thus, this theorem presents a condition under which finite coproducts exist in a category, namely, the presence of an initial object and binary coproducts.
More concisely: If a category has an initial object and binary coproducts, then it has finite coproducts.
|
CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal
theorem CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
[inst_2 : CategoryTheory.Limits.HasTerminal C], CategoryTheory.Limits.HasFiniteProducts C
The theorem `CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal` states that for any category `C`, if `C` has both a terminal object and binary products, then `C` necessarily also has finite products. In simpler terms, this theorem asserts that in the context of category theory, the existence of a terminal object (an object with precisely one morphism going to it from any other object in the category) and binary products (an object representing the product of two objects in the category) together ensure that the category has finite products (an object representing the product of any finite number of objects in the category).
More concisely: In any category with a terminal object and binary products, finite products exist.
|