Add properties: effective congruences / effective cocongruences

Author: dschepler

databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql

@@ -343,6 +343,38 @@ VALUES
 	'quotients of congruences',
 	TRUE
 ),
+(
+	'effective congruences',
+	'has',
+	'A congruence $f, g : E \rightrightarrows X$ (see definition <a href="/category-property/quotients_of_congruences">here</a>) is <i>effective</i> if it is the kernel pair of some morphism, i.e. if there is a morphism $h : X \to Y$ such that we have a cartesian square
+	$$
+	\begin{CD}
+	E @> f >> X \\
+	@V g VV @VV h V \\
+	X @>> h > Y.
+	\end{CD}
+	$$
+	A category <i>has effective congruences</i> if every congruence in the category is effective.',
+	'https://ncatlab.org/nlab/show/congruence',
+	'effective cocongruences',
+	TRUE
+),
+(
+	'effective cocongruences',
+	'has',
+	'A cocongruence $f, g : X \rightrightarrows E$ (see definition <a href="/category-property/coquotients_of_cocongruences">here</a>) is <i>effective</i> if it is the cokernel pair of some morphism, i.e. if there is a morphism $h : Y \to X$ such that we have a cocartesian square
+	$$
+	\begin{CD}
+	Y @> h >> X \\
+	@V h VV @VV f V \\
+	X @>> g > E.
+	\end{CD}
+	$$
+	A category <i>has effective cocongruences</i> if every cocongruence in the category is effective.',
+	NULL,
+	'effective congruences',
+	TRUE
+),
 (
 	'cosifted limits',
 	'has',

databases/catdat/data/002_category-properties/100_related-category-properties.sql

@@ -293,9 +293,17 @@ VALUES
 ('quotients of congruences', 'coequalizers'),
 ('quotients of congruences', 'cokernels'),
 ('quotients of congruences', 'regular'),
+('quotients of congruences', 'effective congruences'),
 ('coquotients of cocongruences', 'equalizers'),
 ('coquotients of cocongruences', 'kernels'),
 ('coquotients of cocongruences', 'coregular'),
+('coquotients of cocongruences', 'effective cocongruences'),
+('effective congruences', 'normal'),
+('effective congruences', 'quotients of congruences'),
+('effective congruences', 'mono-regular'),
+('effective cocongruences', 'conormal'),
+('effective cocongruences', 'coquotients of cocongruences'),
+('effective cocongruences', 'epi-regular'),
 ('direct', 'one-way'),
 ('direct', 'skeletal'),
 ('inverse', 'one-way'),
@@ -341,15 +349,19 @@ VALUES
 ('cofiltered', 'finitely complete'),
 ('cofiltered', 'cofiltered limits'),
 ('mono-regular', 'normal'),
+('mono-regular', 'effective congruences'),
 ('mono-regular', 'subobject-trivial'),
 ('epi-regular', 'conormal'),
+('epi-regular', 'effective cocongruences'),
 ('epi-regular', 'quotient-trivial'),
 ('normal', 'zero morphisms'),
 ('normal', 'mono-regular'),
 ('normal', 'kernels'),
+('normal', 'effective congruences'),
 ('conormal', 'zero morphisms'),
 ('conormal', 'epi-regular'),
 ('conormal', 'cokernels'),
+('conormal', 'effective cocongruences'),
 ('multi-complete', 'complete'),
 ('multi-complete', 'multi-terminal object'),
 ('multi-terminal object', 'multi-complete'),