redundant satisfied properties: remove some, ignore others (part 2)

Author: ScriptRaccoon

databases/catdat/data/003_category-property-assignments/FreeAb.sql

@@ -35,12 +35,6 @@ VALUES
 	TRUE,
 	'See <a href="https://math.stackexchange.com/questions/5025660" target="_blank">MSE/5025660</a>.'
 ),
-(
-	'FreeAb',
-	'equalizers',
-	TRUE,
-	'Subgroups of free abelian groups are free abelian.'
-),
 (
 	'FreeAb',
 	'generator',

databases/catdat/data/003_category-property-assignments/Haus.sql

@@ -113,3 +113,9 @@ VALUES
 	FALSE,
 	'Recall the counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) <a href="/lemma/filtered-monos">this lemma</a> to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Haus'
+AND property_id IN ('cocomplete');

databases/catdat/data/003_category-property-assignments/Met.sql

@@ -43,15 +43,17 @@ VALUES
 ),
 (
 	'Met',
-	'directed colimits',
+	'filtered colimits',
 	TRUE,
-	'This is because the <a href="/category/PMet">category of pseudo-metric spaces</a> has directed colimits and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the directed colimit in the category of pseudo-metric spaces and then identify points with distance zero.' 
+	'This is because the <a href="/category/PMet">category of pseudo-metric spaces</a> has filtered colimits and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the filtered colimit in the category of pseudo-metric spaces and then identify points with distance zero.' 
 ),
 (
 	'Met',
 	'cartesian filtered colimits',
 	TRUE,
-	'The canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is an isomorphism for directed diagrams $(Y_i)$: It is surjective by the concrete description of directed colimits. It is isometric because of the elementary observation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ for $r, s_i \in \IR$, where $i \leq j \implies s_i \geq s_j$.'
+	'We already saw that filtered colimits and finite products exist. The canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is an isomorphism for filtered diagrams $(Y_i)$: It is surjective by the concrete description of filtered colimits. It is isometric because of the elementary observation
+	$$\textstyle\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$$
+	for $r, s_i \in \IR$, where $i \leq j \implies s_i \geq s_j$.'
 ),
 (
 	'Met',
@@ -163,3 +165,8 @@ VALUES
 	On the other hand, if this cocongruence were effective, then by the dual of <a href="/lemma/effective-congruence-quotients">this result</a>, it would be the cokernel pair of the equalizer of the two inclusion maps. However, that equalizer is empty, so $E$ would have to be a binary copower of $(0,1)$, which does not exist in $\Met$.'
 );
 
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Met'
+AND property_id IN ('terminal object', 'binary products', 'filtered colimits');

databases/catdat/data/003_category-property-assignments/Met_c.sql

@@ -17,6 +17,12 @@ VALUES
 	TRUE,
 	'Just restrict the metric to the equalizer built from the sets.'
 ),
+(
+	'Met_c',
+	'countable products',
+	TRUE,
+	'For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking''s book <i>General Topology</i>.'
+),
 (
 	'Met_c',
 	'coproducts',
@@ -27,7 +33,7 @@ VALUES
 	'Met_c',
 	'infinitary extensive',
 	TRUE,
-	'This follows from the existence of coproducts and from the fact that $\Top$ is infinitary extensive.'
+	'This follows from the existence of coproducts and finite products, and from the fact that $\Top$ is infinitary extensive.'
 ),
 (
 	'Met_c',
@@ -47,12 +53,6 @@ VALUES
 	TRUE,
 	'The same proof as for $\Met$ shows that $\IR$ with the usual metric is a cogenerator.'
 ),
-(
-	'Met_c',
-	'countable products',
-	TRUE,
-	'For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) := \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking''s book <i>General Topology</i>.'
-),
 (
 	'Met_c',
 	'well-copowered',
@@ -113,3 +113,9 @@ VALUES
 	FALSE,
 	'If $\Met_c$ had quotients of congruences, then by <a href="/lemma/monic-sequential-colimits-via-congruence-quotients">this lemma</a> it would have sequential colimits of sequences of monomorphisms. This contradicts <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a>.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Met_c'
+AND property_id IN ('coproducts');

databases/catdat/data/003_category-property-assignments/Set_c.sql

@@ -19,21 +19,27 @@ VALUES
 ),
 (
 	'Set_c',
-	'generator',
+	'finitely complete',
 	TRUE,
-	'The one-point set is clearly a generator.'
+	'The embedding $\Set_\c \hookrightarrow \Set$ is closed under finite products and equalizers, hence under finite limits.'
 ),
 (
 	'Set_c',
-	'cogenerator',
+	'finitely cocomplete',
 	TRUE,
-	'The two-point set is a cogenerator in $\Set$, hence also in $\Set_\c$.'
+	'The embedding $\Set_\c \hookrightarrow \Set$ is closed under finite coproducts and coequalizers, hence under finite colimits.'
+),
+(
+	'Set_c',
+	'generator',
+	TRUE,
+	'The one-point set is clearly a generator.'
 ),
 (
 	'Set_c',
-	'equalizers',
+	'cogenerator',
 	TRUE,
-	'We can use the same construction as in $\Set$ since subsets of countable sets are again countable.'
+	'The two-point set is a cogenerator in $\Set$, hence also in $\Set_\c$.'
 ),
 (
 	'Set_c',
@@ -51,37 +57,37 @@ VALUES
 	'Set_c',
 	'countably distributive',
 	TRUE,
-	'By elementary set theory, a countable (disjoint) union of countable sets is again countable, and a finite direct product of countable sets is countable. Hence, countable coproducts and finite products exists in $\Set_\c$. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts.'
+	'By elementary set theory, a countable (disjoint) union of countable sets is again countable. Hence, countable coproducts exist in $\Set_\c$, and we already saw that finite products exist. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts.'
 ),
 (
 	'Set_c',
-	'mono-regular',
+	'epi-regular',
 	TRUE,
-	'If $f : X \to Y$ is a monomorphism, i.e. an injective map, it is an equalizer of the maps $\chi_Y, \chi_{f(X)} : Y \to \{0,1\}$ in $\Set$ and hence also in $\Set_\c$.'
+	'If $X \to Y$ is an epimorphism in $\Set_\c$, i.e. a surjective map, it is coequalizer of the two maps $X \times_Y X \rightrightarrows X$ in $\Set$ and hence also in $\Set_\c$.'
 ),
 (
 	'Set_c',
-	'epi-regular',
+	'subobject classifier',
 	TRUE,
-	'If $X \to Y$ is an epimorphism in $\Set_\c$, i.e. a surjective map, it is coequalizer of the two maps $X \times_Y X \rightrightarrows X$ in $\Set$ and hence also in $\Set_\c$.'
+	'This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide.'
 ),
 (
 	'Set_c',
-	'co-Malcev',
+	'effective congruences',
 	TRUE,
-	'For finite colimits we can use the same construction as in $\Set$ since quotients and finite unions of countable sets are again countable. The co-Malcev property now can be easily deduced from the corresponding fact for $\Set$.'
+	'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using <a href="/lemma/effective-congruence-quotients">this result</a>, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects limits</a>. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.'
 ),
 (
 	'Set_c',
-	'subobject classifier',
+	'regular',
 	TRUE,
-	'This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide.'
+	'From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide.'
 ),
 (
 	'Set_c',
-	'effective congruences',
+	'coregular',
 	TRUE,
-	'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using <a href="/lemma/effective-congruence-quotients">this result</a>, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects limits</a>. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.'
+	'From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushout since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide.'
 ),
 (
 	'Set_c',
@@ -95,18 +101,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'Set_c',
-	'regular',
-	TRUE,
-	'From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide.'
-),
-(
-	'Set_c',
-	'coregular',
-	TRUE,
-	'From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushout since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide.'
-),
 (
 	'Set_c',
 	'countable powers',
@@ -120,3 +114,8 @@ VALUES
 	'In fact, $\Set_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).'
 );
 
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Set_c'
+AND property_id IN ('finitely complete', 'finitely cocomplete');

databases/catdat/data/003_category-property-assignments/Setne.sql

@@ -23,18 +23,6 @@ VALUES
 	TRUE,
 	'The two-point set is a cogenerator, this follows as for $\Set$.'
 ),
-(
-	'Setne',
-	'well-powered',
-	TRUE,
-	'This follows from the description of monomorphisms as injective functions.'
-),
-(
-	'Setne',
-	'well-copowered',
-	TRUE,
-	'This follows from the description of epimorphisms as surjective functions.'
-),
 (
 	'Setne',
 	'products',
@@ -47,18 +35,6 @@ VALUES
 	TRUE,
 	'The disjoint union of two non-empty sets is non-empty.'
 ),
-(
-	'Setne',
-	'wide pushouts',
-	TRUE,
-	'The wide pushout taken in $\Set$ is clearly non-empty, and it still satisfies the universal property.'
-),
-(
-	'Setne',
-	'coequalizers',
-	TRUE,
-	'The coequalizer taken in $\Set$ is clearly non-empty, and it still satisfies the universal property.'
-),
 (
 	'Setne',
 	'cartesian closed',

databases/catdat/data/003_category-property-assignments/SetxSet.sql

@@ -23,12 +23,6 @@ VALUES
     TRUE,
     'Take the two-sorted algebraic theory with no operations and no equations.'
 ),
-(
-	'SetxSet',
-	'effective cocongruences',
-	TRUE,
-	'Suppose we have a cocongruence $X \rightrightarrows E$ in $\Set \times \Set$. Then each component is a cocongruence, so they are the kernel pairs of some maps $Z_1\to X_1$, $Z_2 \to X_2$. Then $E$ is the cokernel pair of $(Z_1, Z_2) \to (X_1, X_2)$.'
-),
 (
 	'SetxSet',
 	'skeletal',

databases/catdat/data/003_category-property-assignments/Top_pointed.sql

@@ -11,11 +11,17 @@ VALUES
 	TRUE,
 	'There is a forgetful functor $\Top_* \to \Set_*$ and $\Set_*$ is locally small.'
 ),
+(
+	'Top*',
+	'pointed',
+	TRUE,
+	'The singleton space $\{0\}$ with base point $0$ is a zero object.'
+),
 (
 	'Top*',
 	'complete',
 	TRUE,
-	'This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ is complete.'
+	'This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ is complete. Concretely, the limit of pointed spaces $(X_i,x_i)$ is the limit of the underlying spaces $X_i$ equipped with the base point that projects down to each $x_i$.'
 ),
 (
 	'Top*',
@@ -41,24 +47,12 @@ VALUES
 	TRUE,
 	'This is clear from the classification of epimorphisms as surjective pointed continuous maps.'
 ),
-(
-	'Top*',
-	'pointed',
-	TRUE,
-	'The singleton space $\{0\}$ with base point $0$ is a zero object.'
-),
 (
 	'Top*',
 	'generator',
 	TRUE,
 	'The discrete space $\{0,1\}$ with base point $0$ is a generator since it represents the forgetful functor $\Top_* \to \Set$.'
 ),
-(
-	'Top*',
-	'disjoint finite coproducts',
-	TRUE,
-	'This follows from the corresponding fact for $\Set_*$.'
-),
 (
 	'Top*',
 	'cogenerator',
@@ -181,3 +175,9 @@ VALUES
 	FALSE,
 	'This counterexample is adapted from the <a href="/category/Top">counterexample for $\Top$</a>. Consider the pointed topological space $I := \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Top*'
+AND property_id IN ('complete', 'coequalizers', 'coproducts', 'pointed');