Add the category of Jónsson-Tarski algebras

.vscode/settings.json

@@ -144,6 +144,7 @@
 		"injectivity",
 		"Isbell",
 		"Johnstone",
+		"Jónsson",
 		"Kashiwara",
 		"katex",
 		"Kolmogorov",
@@ -219,6 +220,7 @@
 		"surjections",
 		"surjective",
 		"surjectivity",
+		"Tarski",
 		"tensoring",
 		"Turso",
 		"unital",

databases/catdat/data/001_categories/002_algebra.sql

@@ -209,4 +209,14 @@ VALUES
 	'This is the category of small categories and functors between them. It is the prototype of a 2-category, but here we only treat it as a 1-category.',
 	'https://ncatlab.org/nlab/show/Cat',
 	NULL
+),
+(
+	'J2',
+	'category of Jónsson-Tarski algebras',
+	'$\mathcal{J}_2$',
+	'pairs $(X,\alpha)$, where $X$ is a set and $\alpha : X \to X \times X$ is an isomorphism',
+	'A morphism $(X,\alpha) \to (Y,\beta)$ is a map $f : X \to Y$ satisfying $$(f \times f) \circ \alpha = \beta \circ f.$$',
+	'This is interesting example of a category in the intersection of topos theory and algebra.',
+	'https://ncatlab.org/nlab/show/J%C3%B3nsson-Tarski+algebra',
+	NULL
 );

databases/catdat/data/001_categories/100_related-categories.sql

@@ -63,9 +63,11 @@ VALUES
 ('FinGrp', 'FinAb'),
 ('Haus', 'Top'),
 ('Haus', 'Met_c'),
+('J2', 'M-Set'),
 ('LRS', 'Sch'),
 ('M-Set', 'R-Mod'),
 ('M-Set', 'Set'),
+('M-Set', 'J2'),
 ('Man', 'Top'),
 ('Man', 'Haus'),
 ('Meas', 'Top'),

databases/catdat/data/001_categories/200_category-tags.sql

@@ -46,6 +46,8 @@ VALUES
 ('FS', 'set theory'),
 ('Grp', 'algebra'),
 ('Haus', 'topology'),
+('J2', 'algebra'),
+('J2', 'set theory'),
 ('LRS', 'algebraic geometry'),
 ('M-Set', 'algebra'),
 ('Man', 'topology'),

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

@@ -71,12 +71,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'FinSet',
-	'Malcev',
-	FALSE,
-	'There are lots of non-symmetric reflexive relations.'
-),
 (
 	'FinSet',
 	'countable',

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

@@ -105,5 +105,5 @@ VALUES
 	'Haus',
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
-	'Our <a href="/category/Set">counterexample for $\mathbf{Set}$</a> (using infinite intersections) also works in $\mathbf{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 $\mathbf{Set} \to \mathbf{Haus}$, which does not preserve all cofiltered limits, but does preserve intersections.'
+	'Recall the counterexample for sets: The unique maps $\mathbb{N}_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \mathbb{N}_{\geq n} \to 1$ is not. This also works in $\mathbf{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 $\mathbf{Set} \to \mathbf{Haus}$, which does not preserve all cofiltered limits, but does preserve intersections.'
 );

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/003_category-property-assignments/M-Set.sql

@@ -31,15 +31,9 @@ VALUES
 ),
 (
 	'M-Set',
-	'Malcev',
+	'trivial',
 	FALSE,
-	'Endow the set $\mathbb{N}$ with the trivial $M$-action, and consider the subset $\{(a,b) : a \leq b \}$ of $\mathbb{N}^2$.'
-),
-(
-	'M-Set',
-	'cofiltered-limit-stable epimorphisms',
-	FALSE,
-	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to M{-}\mathbf{Set}$ that equips a set with the trivial $M$-action.'
+	'This is trivial.'
 );
 
 INSERT INTO category_property_comments (category_id, property_id, comment)

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

@@ -37,13 +37,7 @@ VALUES
 ),
 (
 	'Set',
-	'Malcev',
+	'trivial',
 	FALSE,
-	'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.'
-),
-(
-	'Set',
-	'cofiltered-limit-stable epimorphisms',
-	FALSE,
-	'Pick any decreasing sequence of non-empty sets $X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \mathbb{N}_{\geq n}$. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.'
+	'This is trivial.'
 );

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

@@ -89,12 +89,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'Set_c',
-	'Malcev',
-	FALSE,
-	'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.'
-),
 (
 	'Set_c',
 	'regular',

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

@@ -29,12 +29,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'SetxSet',
-	'Malcev',
-	FALSE,
-	'There are lots of pairs of non-symmetric reflexive relations.'
-),
 (
 	'SetxSet',
 	'semi-strongly connected',
@@ -46,10 +40,4 @@ VALUES
 	'generator',
 	FALSE,
 	'Assume that $(A,B)$ is a generator. Of course, $A$ and $B$ cannot be both empty. Assume w.l.o.g. that $A$ is non-empty. Then there is no morphism $(A,B) \to (0,1)$, but there are two different morphisms $(0,1) \rightrightarrows (0,2)$.'
-),
-(
-	'SetxSet',
-	'cofiltered-limit-stable epimorphisms',
-	FALSE,
-	'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the diagonal functor $\mathbf{Set} \to \mathbf{Set} \times \mathbf{Set}$.'
 );

databases/catdat/data/003_category-property-assignments/Sh(X).sql

@@ -17,12 +17,6 @@ VALUES
 	TRUE,
 	'This holds by definition of a Grothendieck topos.'
 ),
-(
-	'Sh(X)',
-	'Malcev',
-	FALSE,
-	'Consider the subsheaf of $\underline{\mathbb{N}} \times \underline{\mathbb{N}}$ consisting of locally constant functions $(f,g) : X \to \mathbb{N} \times \mathbb{N}$ with $f \leq g$ pointwise. This is reflexive, but not symmetric.'
-),
 (
 	'Sh(X)',
 	'skeletal',
@@ -31,7 +25,7 @@ VALUES
 ),
 (
 	'Sh(X)',
-	'cofiltered-limit-stable epimorphisms',
+	'trivial',
 	FALSE,
-	'Our <a href="/category/Set">counterexample for $\mathbf{Set}$</a> (using infinite intersections) also works in $\mathbf{Sh}(X)$ by using constant sheaves. We could also apply a variant of (the dual of) <a href="/lemma/filtered-monos">this lemma</a> to the constant sheaf functor $\mathbf{Set} \to \mathbf{Sh}(X)$, which does not preserve all cofiltered limits, but does preserve intersections.'
+	'This is because $X$ is assumed to be non-empty.'
 );

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

@@ -47,12 +47,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'Sp',
-	'Malcev',
-	FALSE,
-	'Since $\mathbf{FinSet}$ is not Malcev, there is some finite set $X$ with a non-symmetric reflexive relation $R \subseteq X^2$. Now consider these as constant functors $\mathbb{B} \to \mathbf{FinSet}$.'
-),
 (
 	'Sp',
 	'semi-strongly connected',

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

@@ -41,12 +41,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'sSet',
-	'Malcev',
-	FALSE,
-	'Any counterexample for $\mathbf{Set}$ (i.e., any non-symmetric reflexive relation) yields one for this category by taking constant simplicial sets.'
-),
 (
 	'sSet',
 	'finitary algebraic',

databases/catdat/data/004_category-implications/008_topos-theory-implications.sql

@@ -182,12 +182,19 @@ VALUES
 	FALSE
 ),
 (
-	'topos_is_malcev',
+	'topos_is_co-malcev',
 	'["elementary topos"]',
 	'["co-Malcev"]',
 	'This is Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof is given later in A.5.17.',
 	FALSE
 ),
+(
+	'subobject_classifier_disallows_malcev',
+	'["subobject classifier", "Malcev"]',
+	'["thin"]',
+	'The subobject classifier $\Omega$ is an internal poset (cf. <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). Concretely, the intersection of subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every monomorphism must be an isomorphism. Applying this to equalizers, we see that the category is thin. (And from here, we can infer that it is trivial.)',
+	FALSE
+),
 (
 	'nno_assumption',
 	'["natural numbers object"]',
@@ -222,4 +229,11 @@ VALUES
 	'["natural numbers object"]',
 	'The triple $(1, \mathrm{id}_1, \mathrm{id}_1)$ is clearly a NNO.',
 	FALSE
+),
+(
+	'topos_no_stable_epis',
+	'["elementary topos", "countable coproducts", "cofiltered-limit-stable epimorphisms"]',
+	'["trivial"]',
+	'Let $N := \coprod_{m \in \mathbb{N}} 1$ and consider for every $n \in \mathbb{N}$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n''$ we have $N_{\geq n''} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.',
+	FALSE
 );

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',

src/lib/content/foundations.md

@@ -49,6 +49,8 @@ When $f \in \mathrm{Mor}(\mathcal{C})$ is a morphism with $s(f) = X$ and $t(f) =
 $$f : X \to Y.$$
 We write $\mathrm{Hom}(X,Y)$ or $\mathrm{Mor}(X,Y)$ for the collection of such morphisms. This collection need not be a set. If it is a set for all $X,Y$, the category is called _locally small_.
 
+When a morphism $f : X \to Y$ happens to be uniquely determined, it will be written as $!_{X,Y}$ or even just $!$.
+
 A _small category_ is defined as above, but using _sets_ $O$ and $M$ (instead of collections). A _hypercategory_ is defined similarly using _hypercollections_ $O$ and $M$. Every small category is a category, and every category is a hypercategory. Notice that there is a collection of all small categories $\mathrm{Cat}$, and likewise a hypercollection of all categories $\mathrm{Cat}^+$.
 
 For example, the category of sets $\mathbf{Set}$ has $\mathrm{Ob}(\mathbf{Set}) = \mathrm{Set}$, the collection of all sets. The category of groups $\mathbf{Grp}$ has $\mathrm{Ob}(\mathbf{Grp}) = \mathrm{Grp}$, the collection of all groups. Other typical categories (topological spaces, graphs, metric spaces, etc.) are constructed as usual. All these examples are locally small.