redundant satisfied properties: remove some, ignore others

Author: ScriptRaccoon

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

@@ -35,12 +35,6 @@ VALUES
 	TRUE,
 	'The unique object is a generator for trivial reasons.'
 ),
-(
-	'BN',
-	'pullbacks',
-	TRUE,
-	'For natural numbers $n,m$ we need to find a universal pair $p,q$ of natural numbers satisfying $n + p = m + q$. We may assume w.l.o.g. $n \leq m$. Then take $p = m-n$, $q = 0$.'
-),
 (
 	'BN',
 	'left cancellative',

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

@@ -47,12 +47,6 @@ VALUES
 	TRUE,
 	'This is because $0$ is the only ordinal number with an additive inverse.'
 ),
-(
-	'BOn',
-	'pullbacks',
-	TRUE,
-	'If $\alpha,\beta$ are ordinals, w.l.o.g. $\alpha \leq \beta$, choose $\delta$ with $\beta = \alpha + \delta$. Then the pair $\delta,0$ is a pullback of $\alpha,\beta$: We have $\alpha + \delta = \beta + 0$, and if $\epsilon_1,\,\epsilon_2$ is a pair of ordinals with $\alpha + \epsilon_1 = \beta + \epsilon_2$, we may cancel $\alpha$ to get $\epsilon_1 = \delta + \epsilon_2$, so that the pair factors as $\delta + \epsilon_2,\, 0 + \epsilon_2$.'
-),
 (
 	'BOn',
 	'cofiltered limits',

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/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/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');