add result on additive functors

Author: ScriptRaccoon

databases/catdat/data/functor-implications/limits preservation.yaml

@@ -146,6 +146,19 @@
   proof: This is trivial.
   is_equivalence: false
 
+- id: biproduct_preserving_condition
+  assumptions:
+    - preserves finite products
+  mapped_assumptions:
+    source:
+      - biproducts
+    target:
+      - biproducts
+  conclusions:
+    - preserves finite coproducts
+  proof: This is trivial.
+  is_equivalence: false
+
 - id: lift_implies_preservation
   assumptions:
     - lifts small limits

databases/catdat/data/functors/p-torsion.yaml

@@ -20,9 +20,6 @@ satisfied_properties:
   - property: right adjoint
     proof: 'This functor is clearly right adjoint to $A \mapsto A/pA$.'
 
-  - property: preserves coproducts
-    proof: This is easy to check using the description of coproducts as direct sums.
-
   - property: finitary
     proof: >-
       This follows abstractly from the fact that $\IZ/p$ is finitely presentable. We nevertheless give a direct proof. Let $(A_i)$ be a filtered diagram of abelian groups. We need to show that the canonical map

databases/catdat/data/functors/torsion.yaml

@@ -14,12 +14,8 @@ related_functors:
   - p-torsion
 
 satisfied_properties:
-  - property: preserves coproducts
-    proof: This is easy to check using the description of coproducts as direct sums.
-
   - property: preserves finite products
-    # TODO: automate this with an implication
-    proof: Finite products coincide with finite direct sums.
+    proof: This is easy.
 
   - property: preserves equalizers
     proof: 'Let $E \subseteq A$ be the equalizer of two homomorphisms $f,g : A \rightrightarrows B$. If $a \in T(A)$ is equalized by $T(f),T(g) : T(A) \rightrightarrows T(B)$, then $a \in A$ is equalized by $f,g$, so that $a \in E$. It follows $a \in T(A) \cap E = T(E)$.'