Add more property assignments

Author: dschepler

.vscode/settings.json

@@ -231,10 +231,12 @@
 		"surjectivity",
 		"Tarski",
 		"tensoring",
+		"Tietze",
 		"Turso",
 		"Tychonoff",
 		"unital",
 		"unitalization",
+		"Urysohn",
 		"vercel",
 		"Vite",
 		"Wedderburn",

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

@@ -74,6 +74,18 @@ VALUES
 	TRUE,
 	'Every non-empty compact Hausdorff space is weakly terminal (by using constant maps).'
 ),
+(
+	'CompHaus',
+	'coregular',
+	TRUE,
+	'Since $\CompHaus$ is mono-regular and epi-regular, the regular-epi-mono factorization system from the regularity of $\CompHaus$ also serves as a regular-epi-mono factorization system for $\CompHaus^\op$. Therefore, it suffices to show that pushouts preserve (regular) monomorphisms in $\CompHaus$. Thus, suppose we have a pushout square
+	$$\begin{CD}
+	A @> i >> B \\
+	@V f VV @VV g V \\
+	C @>> j > D,
+	\end{CD}$$
+	with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c'' \in C$, by Urysohn''s lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c'') = 1$. Also, by Tietze''s extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c''))$, we conclude that $j(c) \ne j(c'')$. This shows that $j$ is injective, so it is a regular monomorphism.'
+),
 (
 	'CompHaus',
 	'Malcev',
@@ -100,9 +112,9 @@ VALUES
 ),
 (
 	'CompHaus',
-	'infinitary extensive',
+	'natural numbers object',
 	FALSE,
-	'Consider the coproduct of $\aleph_0$ copies of the one-point space, which is homeomorphic to $\beta \IN$. Take a non-principal ultrafilter of $\IN$, and let $f : 1 \to \beta \IN$ be the corresponding morphism. Then the pullback of $f$ and the coproduct inclusion $i_n : 1 \to \beta \IN$ is empty for each $n$. Therefore, this coproduct is not stable under pullbacks.'
+	'Let $I := [0, 1]$. If a natural numbers object $N$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(n, x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(n) \in N$ has a convergent subnet $(n_\lambda)_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(n_\lambda, x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition $I \overset{y \times \id}\longrightarrow N\times I \to I\times I \overset{p_2}\longrightarrow I$, $x \mapsto (y, x) \mapsto (x, \delta_{x,1}) \mapsto \delta_{x,1}$, would have to be continuous.'
 ),
 (
 	'CompHaus',