diff --git a/content/infinite-products-coproducts-additive-categories.md b/content/infinite-products-coproducts-additive-categories.md
new file mode 100644
index 000000000..728f09770
--- /dev/null
+++ b/content/infinite-products-coproducts-additive-categories.md
@@ -0,0 +1,72 @@
+---
+title: Infinite products and coproducts in additive categories
+description: We prove that in an additive category, an infinite coproduct of copies of a non-zero object cannot be isomorphic to the corresponding infinite product.
+---
+
+# Infinite products and coproducts in additive categories
+
+In a category with zero morphisms, there is a canonical morphism $\bigoplus_{i \in I} X_i \to \prod_{i \in I} X_i$ whenever the coproduct and product exist. In most categories, if $I$ is infinite and the objects $X_i$ are non-zero, this morphism is not an isomorphism. The following result generalizes this observation.
+
+::: Proposition
+Let $\C$ be an additive category with countable powers and countable copowers. Let $A \in \C$ be an object such that the canonical morphism
+$$\textstyle \alpha : \bigoplus_{n \geq 1} A \to \prod_{n \geq 1} A$$
+is an isomorphism. Then $A = 0$.
+:::
+
+::: Proof
+Define the diagonal morphism
+$$\textstyle \Delta : A \to \prod_{n \geq 1} A$$
+by $p_n \circ \Delta = \id_A$, and the codiagonal morphism
+$$\textstyle \nabla : \bigoplus_{n \geq 1} A \to A$$
+by $\nabla \circ i_n = \id_A$ for all $n \geq 1$. Define the endomorphism $x \in \End(A)$ by
+$$x \coloneqq \nabla \circ \alpha^{-1} \circ \Delta.$$
+
+Using the decompositions
+$$\textstyle \bigoplus_{n \geq 1} A \cong A \oplus \bigoplus_{n \geq 2} A,$$
+$$\textstyle \prod_{n \geq 1} A \cong A \oplus \prod_{n \geq 2} A,$$
+the morphisms $\alpha$, $\Delta$, and $\nabla$ have the following block matrix forms:
+
+- $\alpha = \begin{pmatrix} \id_A & 0 \\ 0 & \alpha' \end{pmatrix}$, where $\alpha' : \bigoplus_{n \geq 2} A \to \prod_{n \geq 2} A$ is the canonical morphism.
+- $\Delta = \begin{pmatrix} \id_A \\ \Delta' \end{pmatrix}$, where $\Delta' : A \to \prod_{n \geq 2} A$ is the diagonal morphism.
+- $\nabla = \begin{pmatrix} \id_A & \nabla' \end{pmatrix}$, where $\nabla' : \bigoplus_{n \geq 2} A \to A$ is the codiagonal morphism.
+
+Since $\alpha$ is an isomorphism, $\alpha'$ is an isomorphism as well. We compute:
+
+$$
+\begin{align*}
+x & = \nabla \circ \alpha^{-1} \circ \Delta \\
+& = \begin{pmatrix} \id_A & \nabla' \end{pmatrix} \circ \begin{pmatrix} \id_A & 0 \\ 0 & \alpha'^{-1} \end{pmatrix} \circ \begin{pmatrix} \id_A \\ \Delta' \end{pmatrix} \\
+& = \begin{pmatrix} \id_A & \nabla' \end{pmatrix} \circ \begin{pmatrix} \id_A \\ \alpha'^{-1} \circ \Delta' \end{pmatrix} \\
+& = {\id_A} \,+\, \nabla' \circ \alpha'^{-1} \circ \Delta'.
+\end{align*}
+$$
+
+Now define the isomorphism
+$$\textstyle \sigma : \bigoplus_{n \geq 1} A \to \bigoplus_{n \geq 2} A$$
+by $\sigma \circ i_n = i_{n+1}$ for $n \geq 1$. Likewise, define the isomorphism
+$$\textstyle \tau : \prod_{n \geq 1} A \to \prod_{n \geq 2} A$$
+by $p_n \circ \tau = p_{n-1}$ for $n \geq 2$.
+
+By the definitions of $\alpha'$, $\Delta'$, and $\nabla'$, we have
+
+$$
+\begin{align*}
+\alpha' & = \tau \circ \alpha \circ \sigma^{-1}, \\
+\Delta' & = \tau \circ \Delta, \\
+\nabla' & = \nabla \circ \sigma^{-1}.
+\end{align*}
+$$
+
+Therefore,
+
+$$
+\begin{align*}
+\nabla' \circ \alpha'^{-1} \circ \Delta' & = \nabla \circ \sigma^{-1} \circ (\tau \circ \alpha \circ \sigma^{-1})^{-1} \circ \tau \circ \Delta \\
+& = \nabla \circ \sigma^{-1} \circ \sigma \circ \alpha^{-1} \circ \tau^{-1} \circ \tau \circ \Delta \\
+& = \nabla \circ \alpha^{-1} \circ \Delta \\
+& = x.
+\end{align*}
+$$
+
+Thus $x = \id_A + x$, and hence $\id_A = 0$. Therefore $A = 0$.
+:::
diff --git a/database/data/categories/Sh(X,Ab).yaml b/database/data/categories/Sh(X,Ab).yaml
index 868f7ff38..90f961a7a 100644
--- a/database/data/categories/Sh(X,Ab).yaml
+++ b/database/data/categories/Sh(X,Ab).yaml
@@ -16,7 +16,7 @@ related:
comments:
# TODO: maybe create separate entries for specific spaces X
- - It is likely that neither of the currently remaining unknown properties (finitary algebraic, locally finitely presentable, CSP, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$.
+ - It is likely that neither of the currently remaining unknown properties (finitary algebraic, locally finitely presentable, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$.
satisfied_properties:
- property: locally small
diff --git a/database/data/categories/TorsAb.yaml b/database/data/categories/TorsAb.yaml
index 97ec2d691..d7dc64c92 100644
--- a/database/data/categories/TorsAb.yaml
+++ b/database/data/categories/TorsAb.yaml
@@ -45,9 +45,6 @@ unsatisfied_properties:
- property: split abelian
proof: The sequence $0 \to \IZ/2 \to \IZ/4 \to \IZ/2 \to 0$ does not split.
- - property: CSP
- proof: The canonical homomorphism $\bigoplus_{n \geq 0} \IZ/2 \to T(\prod_{n \geq 0} \IZ/2)$ is not surjective, since the torsion element $(1,1,\dotsc)$ does not lie in the image. Hence, it is no epimorphism.
-
- property: finitary algebraic
proof: >-
Assume that it is the category of models of a many-sorted finitary algebraic theory. For each sort $s$ let $F_s$ be the free algebra on one generator of sort $s$. One of them must be non-trivial, since otherwise the category would be thin. So assume $F_s \neq 0$. It is finitely presentable, hence a finite abelian group, and regular projective. Any direct summand will have the same properties. So we find that some $\IZ/p^k$ (with $k \geq 1$ and $p$ prime) is regular projective. However, the exact sequence in $\TorsAb$
diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml
index 49e73d9f1..d38425afb 100644
--- a/database/data/category-implications/accessible.yaml
+++ b/database/data/category-implications/accessible.yaml
@@ -105,9 +105,13 @@
- id: grothendieck_abelian_presentable
assumptions:
- Grothendieck abelian
+ - locally essentially small
conclusions:
- locally presentable
- proof: See Deriving Auslander's formula, Cor. 5.2, or Sheafifiable homotopy model categories, Prop. 3.10.
+ proof: >-
+ See Deriving Auslander's formula, Cor. 5.2, or Sheafifiable homotopy model categories, Prop. 3.10.
+
+ Remark: The assumption that the category is locally essentially small is necessary (and is implicit in most of the literature), as the example $[\Set_{\disc},\Ab]$ shows.
- id: algebraic_implies_lfp
assumptions:
diff --git a/database/data/category-implications/additive.yaml b/database/data/category-implications/additive.yaml
index 7b00f504e..1d26911b6 100644
--- a/database/data/category-implications/additive.yaml
+++ b/database/data/category-implications/additive.yaml
@@ -4,7 +4,6 @@
assumptions:
- preadditive
conclusions:
- - locally essentially small
- zero morphisms
proof: This is trivial.
@@ -65,17 +64,31 @@
- id: grothendieck_abelian_cogenerator
assumptions:
- Grothendieck abelian
+ - locally essentially small
conclusions:
- cogenerator
- proof: See Kashiwara-Schapira, Thm. 9.6.3.
+ proof: >-
+ See Kashiwara-Schapira, Thm. 9.6.3.
-- id: grothendieck_abelian_self-dual
+ Remark: The assumption that the category is locally essentially small is necessary (and is implicit in most of the literature), as the example $[\On,\Ab]$ shows.
+
+- id: additive_CIP_CSP
assumptions:
- - Grothendieck abelian
- - self-dual
+ - additive
+ - balanced
+ - CIP
+ - CSP
conclusions:
- trivial
- proof: This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, Abelian categories, p. 116.
+ proof: >-
+ We work in a balanced additive category with products and coproducts such that, for every family of objects $(X_i)$, the canonical morphism
+ $$\textstyle \alpha : \coprod_i X_i \to \prod_{i \in I} X_i$$
+ is a monomorphism and an epimorphism, and therefore an isomorphism. In particular, for every object $A$ the canonical morphism
+ $$\textstyle \alpha : \coprod_{n \geq 1} A \to \prod_{n \geq 1} A$$
+ is an isomorphism. By this proposition, this implies that $A = 0$.
+
+
+ Remark: This result strengthens the well-known theorem (and is inspired by it) stating that the dual of a Grothendieck abelian category can only be Grothendieck abelian when it is trivial, which appears as exercise B on p. 116 in Freyd's book Abelian categories. This follows from the result we have just proved since a Grothendieck abelian category with products is additive, balanced, and satisfies CIP (by this result).
- id: split_abelian_condition
assumptions:
diff --git a/database/data/category-implications/mono-regular.yaml b/database/data/category-implications/mono-regular.yaml
index ccb0ed096..5d0c045da 100644
--- a/database/data/category-implications/mono-regular.yaml
+++ b/database/data/category-implications/mono-regular.yaml
@@ -27,4 +27,4 @@
- preadditive
conclusions:
- normal
- proof: The a monomorphism is the equalizer of $f,g$, it is the kernel of $f-g$.
+ proof: If a monomorphism is the equalizer of $f,g$, it is the kernel of $f-g$.
diff --git a/database/data/category-properties/additive.yaml b/database/data/category-properties/additive.yaml
index 764eca804..cbd8c7427 100644
--- a/database/data/category-properties/additive.yaml
+++ b/database/data/category-properties/additive.yaml
@@ -10,6 +10,8 @@ related:
- finite coproducts
- finite products
- preadditive
+ - zero morphisms
+ - abelian
tags:
- morphism behavior
diff --git a/database/data/category-properties/preadditive.yaml b/database/data/category-properties/preadditive.yaml
index 41824ec15..c06e176e4 100644
--- a/database/data/category-properties/preadditive.yaml
+++ b/database/data/category-properties/preadditive.yaml
@@ -1,14 +1,19 @@
id: preadditive
relation: is
-description: |-
- A category is preadditive when it is locally essentially small* and each hom-set carries the structure of an abelian group such that the composition is bilinear. Notice that "preadditive" is an extra structure. The property here just says that some preadditive structure exists.
- *We demand this instead of the more common "locally small" to ensure that preadditive categories are invariant under equivalences of categories.
+description: >-
+ A category is preadditive if, for every pair of objects $A,B$, the collection of morphisms $\Hom(A,B)$ is equipped with the structure of an abelian group such that composition is bilinear:
+ $$\begin{align*}
+ f \circ (g + h) &= f \circ g + f \circ h \\
+ (f + g) \circ h &= f \circ h + g \circ h.
+ \end{align*}$$
+ Note that being preadditive is an extra structure. The property here merely says that a preadditive structure exists. Furthermore, since categories are not assumed to be locally small (see Foundations), the abelian group $\Hom(A,B)$ is not necessarily a set. In contrast, a locally small preadditive category is precisely an $(\Ab,\otimes)$-enriched category.
nlab_link: https://ncatlab.org/nlab/show/Ab-enriched+category
dual: preadditive
invariant_under_equivalences: true
related:
- additive
+ - zero morphisms
tags:
- morphism behavior
diff --git a/database/data/category-properties/zero morphisms.yaml b/database/data/category-properties/zero morphisms.yaml
index ab50ba9bf..505ff545d 100644
--- a/database/data/category-properties/zero morphisms.yaml
+++ b/database/data/category-properties/zero morphisms.yaml
@@ -7,6 +7,7 @@ invariant_under_equivalences: true
related:
- pointed
+ - additive
- preadditive
tags: