save comments from deprecated sql files

Author: ScriptRaccoon

databases/catdat/data_yaml/categories/Grp.yaml

@@ -55,6 +55,7 @@ unsatisfied_properties:
     reason: The canonical morphism $F_2 = \IZ \sqcup \IZ \to \IZ \times \IZ$ is not a monomorphism since $F_2$ is not abelian.
 
   - property_id: CIP
+    # TODO: remove code duplication with "counital" proof
     reason: The canonical morphism $F_2 = \IZ \sqcup \IZ \to \IZ \times \IZ$ is not a monomorphism since $F_2$ is not abelian.
 
   - property_id: regular quotient object classifier

databases/catdat/data_yaml/categories/Man.yaml

@@ -32,6 +32,7 @@ satisfied_properties:
     reason: "[Sketch] Since $\\Top$ is infinitary extensive, a continuous map $f : M \\to \\coprod_i N_i$ corresponds to a decomposition $M = \\coprod_i M_i$ (as topological spaces) with continuous maps $f_i : M_i \\to N_i$. Endow the open subset $M_i \\subseteq M$ with the smooth structure inherited from $M$. Now remark that $f$ is smooth iff each $f_i$ is smooth."
 
   - property_id: countably distributive
+    # TODO: maybe add "countably extensive" to make this more conceptual
     reason: To construct countable coproducts, take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) Now we need to check that the canonical smooth map $\coprod_i X \times Y_i \to X \times \coprod_i Y_i$ is a diffeomorphism (for countable families). It is a homeomorphism since $\Top$ is infinitary distributive. The inverse $X \times \coprod_i Y_i \to \coprod_i X \times Y_i$ is smooth since the domain is covered by the open subsets $X \times Y_i$ on which the map is clearly smooth.
 
   - property_id: Cauchy complete

databases/catdat/data_yaml/categories/Mon.yaml

@@ -45,6 +45,7 @@ unsatisfied_properties:
     reason: The canonical morphism $\IN \sqcup \IN \to \IN \times \IN$ is not a monomorphism since $\IN \sqcup \IN$ is not commutative.
 
   - property_id: CIP
+    # TODO: remove code duplication with "counital" proof
     reason: The canonical morphism $\IN \sqcup \IN \to \IN \times \IN$ is not a monomorphism since $\IN \sqcup \IN$ is not commutative.
 
   - property_id: coregular

databases/catdat/data_yaml/categories/Rng.yaml

@@ -42,6 +42,7 @@ unsatisfied_properties:
     reason: If $\IZ\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism $\IZ\langle X,Y \rangle_0 = \IZ\langle X \rangle_0 \sqcup \IZ\langle Y \rangle_0 \to \IZ\langle X \rangle_0 \times \IZ\langle Y \rangle_0$ is not a monomorphism since $\IZ\langle X,Y \rangle_0$ is not commutative.
 
   - property_id: CIP
+    # TODO: remove code duplication with "counital" proof
     reason: If $\IZ\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism $\IZ\langle X,Y \rangle_0 = \IZ\langle X \rangle_0 \sqcup \IZ\langle Y \rangle_0 \to \IZ\langle X \rangle_0 \times \IZ\langle Y \rangle_0$ is not a monomorphism since $\IZ\langle X,Y \rangle_0$ is not commutative.
 
   - property_id: regular subobject classifier

databases/catdat/data_yaml/categories/SemiGrp.yaml

@@ -55,6 +55,8 @@ unsatisfied_properties:
           Let $A$ be the set of positive rational numbers of the form $m/2^n$ (with $m > 0$, $n \geq 0$), and let $B$ be the set of positive rational numbers of the form $m/3^n$ (with $m > 0$, $n \geq 0$). Both are semigroups under addition. The element $1 \in A$ is $2^\infty$-divisible, meaning that for every $n \geq 0$ there is some $a \in A$ with $1 = 2^n \cdot a$. But $B$ has no $2^\infty$-divisible element. Hence, there is no semigroup homomorphism $A \to B$. Likewise, there is no semigroup homomorphism $B \to A$.
 
   - property_id: cogenerating set
+    # TODO: find a variant of the lemma missing_cogenerating_sets
+    # (or missing_cogenerator) which handles this.
     reason: |-
       The proof is similar to the proof for <a href="/category/Grp">$\Grp$</a>. Assume that there is a cogenerating set $S$. There is an infinite simple group $G$ larger than all the semigroups in $S$ (such as an alternating group). Since $\id_G, 1 : G \rightrightarrows G$ are different, there is a semigroup $H \in S$ and a homomorphism of semigroups $f : G \to H$ with $f \neq f \circ 1$. Then
       	$$N := \{g \in G : f(g) = f(1)\}$$

databases/catdat/data_yaml/categories/Set_pointed.yaml

@@ -49,6 +49,7 @@ satisfied_properties:
     reason: The coproduct (wedge sum) of a family of pointed sets $(X_i)_{i \in I}$ can be realized as the subset of $\prod_{i \in I} X_i$ consisting of those tuples $x$ such that $x_i = 0$ for all but (at most) one index.
 
   - property_id: effective cocongruences
+    # TODO: rework this when Barr-exact is added
     reason: We have that $\Set_*^{\op}$ is a slice category of $\Set^{\op}$, which in turn is monadic over $\Set$. Therefore, by combining results from <a href="http://www.springer.com/us/book/9781402019616" target="_blank">Borceux and Bourn</a> Appendix A and <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact" target="_blank">nLab</a>, $\Set_*^{\op}$ is Barr-exact, and in particular it has effective congruences.
 
 unsatisfied_properties:
@@ -59,6 +60,7 @@ unsatisfied_properties:
     reason: "The joint image of $X \\to X \\times Y \\leftarrow Y$ is just $\\{(x,0) : x \\in X\\} \\cup \\{(0,y) : y \\in Y\\}$ (where $0$ denotes the base point), which is clearly a proper subset of $X \\times Y$ when both $X,Y$ are non-trivial."
 
   - property_id: CSP
+    # TODO: remove duplication with unital proof
     reason: "The image of $X \\vee Y$ in $X \\times Y$ is just $\\{(x,0) : x \\in X\\} \\cup \\{(0,y) : y \\in Y\\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial."
 
   - property_id: conormal

databases/catdat/data_yaml/categories/Top_pointed.yaml

@@ -88,15 +88,16 @@ unsatisfied_properties:
   - property_id: unital
     reason: "The joint image of $X \\to X \\times Y \\leftarrow Y$ is just $\\{(x,0) : x \\in X\\} \\cup \\{(0,y) : y \\in Y\\}$ (where $0$ denotes the base point), which is clearly a proper subset of $X \\times Y$ when both $X,Y$ are non-trivial."
 
+  - property_id: CSP
+    # TODO: remove duplication with unital proof
+    reason: "The image of $X \\vee Y$ in $X \\times Y$ is just $\\{(x,0) : x \\in X\\} \\cup \\{(0,y) : y \\in Y\\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial."
+
   - property_id: regular quotient object classifier
     reason: We can recycle the proof for the <a href="/category/Set*">category of pointed sets</a> using discrete topological spaces.
 
   - property_id: coaccessible
     reason: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since $\Set_*$ is not coaccessible, this is a contradiction.'
 
-  - property_id: CSP
-    reason: "The image of $X \\vee Y$ in $X \\times Y$ is just $\\{(x,0) : x \\in X\\} \\cup \\{(0,y) : y \\in Y\\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial."
-
   - property_id: cofiltered-limit-stable epimorphisms
     reason: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology.
 

databases/catdat/data_yaml/categories/walking_coreflexive_pair.yaml

@@ -68,6 +68,7 @@ unsatisfied_properties:
     reason: Assume that $[1] \xleftarrow{i} [0] \xrightarrow{i} [1]$ has a pushout in $\Delta^{\leq 1}$, where $i(0)=0$. This amounts to a universal totally ordered set of cardinality $\leq 2$ with elements $a,b,c$ satisfying $a \leq b$, $a \leq c$. Since a finite totally ordered set has trivial automorphism group, the automorphism defined by $a \mapsto a$, $b \mapsto c$, $c \mapsto b$ must be the identity, i.e., we have $b = c$. However, in $[1]$ the equations $0 \leq 0$, $0 \leq 1$ then show that the universal property fails.
 
   - property_id: multi-complete
+    # TODO: remove this manual proof once locally multi-presentable is dualized, cf. #139
     reason: 'This follows directly from existing results: If its dual, the walking reflexive pair, was multi-cocomplete, then since it is also accessible, it would be <a href="/category-property/locally_multi-presentable">locally multi-presentable</a>. But then it would have connected limits, in particular pullbacks.'
 
 special_objects:

databases/catdat/data_yaml/category-implications/filtered colimits.yaml

@@ -49,6 +49,8 @@
   is_equivalence: false
 
 - id: finite_filtered_colimits
+  # TODO: combine this with the implication with ID "finite_accessible"
+  # once its dual is added to the database.
   assumptions:
     - Cauchy complete
     - essentially finite