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

Author: ScriptRaccoon

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

@@ -94,4 +94,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \IC$ for all $n \geq 0$. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ <i>and</i> $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \IC$ is no epimorphism.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Ban'
+AND property_id IN ('pointed');

databases/catdat/data/003_category-property-assignments/CAlg(R).sql

@@ -88,4 +88,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'Let $K$ be a field over $R$. Consider the sequence of projections $\cdots \to K[X]/\langle X^2 \rangle \to K[X]/\langle X \rangle$ and the constant sequence $\cdots \to K[X] \to K[X]$. The surjective homomorphisms $K[X] \to K[X]/\langle X^n \rangle$ induce the inclusion $K[X] \hookrightarrow K[[X]]$ in the limit, where $K[[X]]$ is the algebra of formal power series. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\CAlg(R)$, or equivalently, in $\CRing$. For a proof, see <a href="https://math.stackexchange.com/questions/2391187" target="_blank">MSE/2391187</a>.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'CAlg(R)'
+AND property_id IN ('strict terminal object');

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

@@ -82,4 +82,10 @@ VALUES
 	'CSP',
 	FALSE,
 	'First of all, epimorphisms in $\CMon$ are preserved and reflected by the forgetful functor to $\Mon$ (see below). Furthermore, if $M \to N$ is an epimorphism in $\Mon$ and $M$ is infinite, then $\card(N) \leq \card(M)$ (see <a href="https://mathoverflow.net/questions/510431/" target="_blank">MO/510431</a>). This implies that in $\CMon$ the canonical homomorphism $\bigoplus_{n \geq 0} \IN \to \prod_{n \geq 0} \IN$ is not an epimorphism because its domain is countable and its codomain is uncountable.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'CMon'
+AND property_id IN ('pointed');

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

@@ -89,3 +89,9 @@ VALUES
 	FALSE,
 	'For a prime $p$ consider the sequence of projections $\cdots \to \IZ/p^2 \to \IZ/p$ and the constant sequence $\cdots \to \IZ \to \IZ$. The surjective homomorphisms $\IZ \to \IZ/p^n$ induce the homomorphism $\IZ \to \IZ_p$ in the limit, where $\IZ_p$ is the ring of $p$-adic integers. It is not surjective since $\IZ_p$ is uncountable, but this is not sufficient (at least, for this category): We need to use <a href="https://stacks.math.columbia.edu/tag/04W0" target="_blank">SP/04W0</a> to conclude that it is no epimorphism in $\CRing$.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'CRing'
+AND property_id IN ('strict terminal object');

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

@@ -11,12 +11,6 @@ VALUES
 	TRUE,
 	'There is a forgetful functor $\FI \to \Set$ and $\Set$ is locally small.'
 ),
-(
-	'FI',
-	'initial object',
-	TRUE,
-	'Take the empty set.'
-),
 (
 	'FI',
 	'left cancellative',

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

@@ -23,12 +23,6 @@ VALUES
 	TRUE,
 	'The underlying set of a finite structure can be chosen to be a subset of $\IN$.'
 ),
-(
-	'FinGrp',
-	'epi-regular',
-	TRUE,
-	'This holds since every epimorphism is surjective (see below), and a surjective homomorphism $A \to B$ is the coequalizer of its kernel pair $A \times_B A \rightrightarrows A$.'
-),
 (
 	'FinGrp',
 	'mono-regular',
@@ -119,3 +113,9 @@ VALUES
 	FALSE,
 	'This is trivial.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'FinGrp'
+AND property_id IN ('pointed');

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

@@ -29,12 +29,6 @@ VALUES
 	TRUE,
 	'See Prop. 4.2 at the <a href="https://ncatlab.org/nlab/show/regular+monomorphism#Examples" target="_blank">nLab</a>.'
 ),
-(
-	'Grp',
-	'epi-regular',
-	TRUE,
-	'This holds since every epimorphism is surjective, and a surjective homomorphism $A \to B$ is the coequalizer of its kernel pair $A \times_B A \rightrightarrows A$.'
-),
 (
 	'Grp',
 	'Malcev',
@@ -116,4 +110,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Grp'
+AND property_id IN ('pointed');

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

@@ -134,3 +134,9 @@ VALUES
 	FALSE,
 	'If $\Man$ had quotients of congruences, then by <a href="/lemma/pushouts-of-monos-via-congruence-quotients">this lemma</a>, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$.  This contradicts <a href="https://mathoverflow.net/questions/19116">MO/19916</a>.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Man'
+AND property_id IN ('finite products');

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

@@ -113,3 +113,9 @@ VALUES
 	$$E \to M_{2\times 2}(\IZ), \quad p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix},\quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix},$$
 	we can see that $p \ne q$ in $E$, so the equalizer of the two maps $X \rightrightarrows E$ is the trivial submonoid $\{ 1 \}$. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.'
 );
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'Mon'
+AND property_id IN ('pointed');

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

@@ -35,12 +35,6 @@ VALUES
 	TRUE,
 	'Every non-empty set of natural numbers has a minimum.'
 ),
-(
-	'N',
-	'skeletal',
-	TRUE,
-	'The relation $\leq$ is antisymmetric.'
-),
 (
 	'N',
 	'semi-strongly connected',
@@ -64,4 +58,10 @@ VALUES
 	'countable coproducts',
 	FALSE,
 	'The numbers $0,1,2,\dotsc$ have no supremum, i.e. no coproduct.'
-);
+);
+
+-- properties that should be ignored by the redundancy check script
+UPDATE category_property_assignments
+SET check_redundancy = FALSE
+WHERE category_id = 'N'
+AND property_id IN ('thin', 'finitely cocomplete');