assign most properties to jonsson-tarski algebras

Author: ScriptRaccoon

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

@@ -0,0 +1,42 @@
+INSERT INTO category_property_assignments (
+	category_id,
+	property_id,
+	is_satisfied,
+	reason
+)
+VALUES
+(
+	'J2',
+	'locally small',
+	TRUE,
+	'This is trivial.'
+),
+(
+	'J2',
+	'finitary algebraic',
+	TRUE,
+	'The structure of a Jónsson-Tarski algebra on a set $X$ is equivalent to one binary operation $\mu : X^2 \to X$ and two unary operations $\lambda, \rho : X \rightrightarrows X$ such that $\mu(\lambda(x),\rho(x)) = x$, $\lambda(\mu(x,y))=x$, and $\rho(\mu(x,y))=y$.'
+),
+(
+	'J2',
+	'Grothendieck topos',
+	TRUE,
+	'See the <a href="https://ncatlab.org/nlab/show/J%C3%B3nsson-Tarski+topos" target="_blank">nLab</a>.'
+),
+(
+	'J2',
+	'skeletal',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'J2',
+	'semi-strongly connected',
+	FALSE,
+	'There is a bijection $\alpha = (\lambda,\rho) : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ such that $\lambda$ has a fixed point, but $\rho$ does not (see below). Then the isomorphism $\beta := (\rho,\lambda)$ has the opposite property. There cannot be any morphism $(\mathbb{N},\alpha) \to (\mathbb{N},\beta)$, as it would map the fixed point of $\lambda$ to a fixed point of $\rho$, and likewise there is no morphism $(\mathbb{N},\beta) \to (\mathbb{N},\alpha)$.<br>
+	To construct $\alpha$ or rather $\alpha^{-1} : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$, we can alter the standard bijection $(n,m) \mapsto 2^n (2m+1) - 1$ as follows:
+	$$\alpha^{-1}(n,m) = \begin{cases} 2 & (n,m) = (0,0) \\ 0 & (n,m) = (0,1) \\ 2^n (2m+1) - 1 & \text{otherwise} \end{cases}$$
+	Then $\alpha(0)=(0,1)$, i.e. $\lambda(0)=0$. The function $\rho$ has no fixed point, i.e. $\alpha^{-1}(n,m) \neq m$ for all $n,m$. Namely, if $(n,m)=(0,0)$, then $\alpha^{-1}(n,m)=2 \neq m$. If $(n,m)=(0,1)$, then $\alpha^{-1}(n,m)=0 \neq m$. Otherwise,
+	$$\alpha^{-1}(n,m) = 2^n (2m+1) - 1 \geq (2m+1)-1 = 2m \geq m,$$
+	and equality can only hold if $m=0$ and $n=0$, which we already excluded.'
+);

databases/catdat/data/005_special-objects/002_initial_objects.sql

@@ -22,6 +22,7 @@ VALUES
 ('FreeAb', 'trivial group'),
 ('Grp', 'trivial group'),
 ('Haus', 'empty space'),
+('J2', '$(\varnothing,!)$'),
 ('LRS', 'empty space'),
 ('M-Set', 'empty set with the unique action'),
 ('Man', 'empty manifold'),

databases/catdat/data/005_special-objects/003_terminal_objects.sql

@@ -21,6 +21,7 @@ VALUES
 ('FreeAb', 'trivial group'),
 ('Grp', 'trivial group'),
 ('Haus', 'singleton space'),
+('J2', '$(\{\ast\},!)$'),
 ('LRS', '$\mathrm{Spec}(\mathbb{Z})$'),
 ('M-Set', 'singleton set with the unique action'),
 ('Man', 'singleton manifold of dimension $0$'),

databases/catdat/data/005_special-objects/004_coproducts.sql

@@ -19,6 +19,7 @@ VALUES
 ('FreeAb', 'direct sums'),
 ('Grp', 'free products'),
 ('Haus', 'disjoint union with the disjoint union topology'),
+('J2', 'See <a href="https://matheplanet.de/matheplanet/nuke/html/article.php?sid=1713" target="_blank">here</a> for a description'),
 ('LRS', 'disjoint union with the product sheaf'),
 ('M-Set', 'disjoint union with obvious $M$-action'),
 ('Meas', 'disjoint union with the obvious $\sigma$-algebra'),

databases/catdat/data/005_special-objects/005_products.sql

@@ -18,6 +18,7 @@ VALUES
 ('CRing', 'direct products with pointwise operations'),
 ('Grp', 'direct products with pointwise operations'),
 ('Haus', 'direct product with the <a href="https://en.wikipedia.org/wiki/Product_topology" target="_blank">product topology</a>'),
+('J2', 'direct products with pointwise operations'),
 ('LRS', 'See <a href="https://arxiv.org/abs/1103.2139" target="_blank">Localization of ringed spaces</a> by W. Gillam. See also <a href="https://math.stackexchange.com/questions/1033675" target="_blank">MSE/1033675</a>.'),
 ('M-Set', 'direct products with the evident $M$-action'),
 ('Meas', 'direct products with the <a href="https://de.wikipedia.org/wiki/Produkt-%CF%83-Algebra" target="_blank">product $\sigma$-algebra</a>'),

databases/catdat/data/006_special-morphisms/002_isomorphisms.sql

@@ -145,6 +145,11 @@ VALUES
 	'homeomorphisms',
 	'This is easy.'
 ),
+(
+	'J2',
+	'bijective morphisms',
+	'This characterization holds in every algebraic category.'
+),
 (
 	'LRS',
 	'pairs $(f,f^{\sharp})$ consisting of a homeomorphism $f$ and an isomorphism of sheaves $f^{\sharp}$',

databases/catdat/data/006_special-morphisms/003_monomorphisms.sql

@@ -140,6 +140,11 @@ VALUES
 	'injective continuous maps',
 	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
+(
+	'J2',
+	'injective morphisms',
+	'This holds in every finitary algebraic category: the forgetful functor to $\mathbf{Set}$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'
+),
 (
 	'M-Set',
 	'injective $M$-maps',

databases/catdat/data/006_special-morphisms/004_epimorphisms.sql

@@ -141,6 +141,11 @@ VALUES
 	'continuous maps with dense image',
 	'It is clear that continuous maps with dense image are epimorphism, but the other direction is non-trivial. See <a href="https://math.stackexchange.com/questions/214045" target="_blank">MSE/214045</a> for a proof.'
 ),
+(
+	'J2',
+	'surjective morphisms',
+	'For the non-trivial direction: The category is epi-regular (since it is an elementary topos), and every regular epimorphism is surjective (this holds in any algebraic category).'
+),
 (
 	'M-Set',
 	'surjective $M$-maps',

databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql

@@ -115,6 +115,11 @@ VALUES
     'embeddings with closed image',
     'The explicit construction of equalizers shows that they are embeddings, and they have a closed image because of the well-known lemma that for a Hausdorff space the diagonal $X \to X \times X$ has closed image. For the other non-trivial direction, see <a href="https://math.stackexchange.com/questions/214045/" target="_blank">MSE/214045</a>.'
 ),
+(
+    'J2',
+    'same as monomorphisms',
+    'This is because the category is mono-regular.'
+),
 (
     'M-Set',
     'same as monomorphisms',

databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql

@@ -125,6 +125,11 @@ VALUES
     'surjective homomorphisms',
     'This holds in every finitary algebraic category.'
 ),
+(
+    'J2',
+    'same as epimorphisms',
+    'This is because the category is epi-regular.'
+),  
 (
     'M-Set',
     'surjective homomorphisms',