update dictionary + fix typo

Author: ScriptRaccoon

.vscode/settings.json

@@ -18,7 +18,9 @@
 		"SetxSet",
 		"hilberts",
 		"maxage",
-		"ndash"
+		"ndash",
+		"emptyset",
+		"varnothing"
 	],
 	"cSpell.words": [
 		"abelian",
@@ -182,6 +184,7 @@
 		"precomposition",
 		"preimage",
 		"preimages",
+		"preorder",
 		"preordered",
 		"prerender",
 		"prerendered",

databases/catdat/data/categories/FreeAb.yaml

@@ -35,7 +35,7 @@ satisfied_properties:
 
   - property_id: regular
     reason: |-
-      This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the <a href="https://ncatlab.org/nlab/show/regular+category">nlab</a> it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup, hence free, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms.
+      This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a> it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup, hence free, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms.
       (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\Ab$. Since $A \times_B A$ is free abelian, $f$ is also an coequalizer in $\FreeAb$.
       (2) If $f : A \to B$ is a regular epimorphism in $\FreeAb$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective.