Add kernels, cokernels, normal, conormal

database/data/003_properties/002_limits-colimits-existence.sql

@@ -215,6 +215,22 @@ VALUES
 	'equalizers',
 	TRUE
 ),
+(
+	'kernels',
+	'has',
+	'A category has <i>kernels</i> if it has zero morphisms and every morphism $f : A \to B$ has a kernel, i.e. an equalizer of $f$ with the zero morphism $0_{A,B} : A \to B$.',
+	'https://ncatlab.org/nlab/show/kernel',
+	'cokernels',
+	TRUE
+),
+(
+	'cokernels',
+	'has',
+	'A category has <i>cokernels</i> if it has zero morphisms and every morphism $f : A \to B$ has a cokernel, i.e. a coequalizer of $f$ with the zero morphism $0_{A,B} : A \to B$.',
+	'https://ncatlab.org/nlab/show/cokernel',
+	'kernels',
+	TRUE
+),
 (
 	'cofiltered limits',
 	'has',

database/data/003_properties/005_morphism-behavior.sql

@@ -18,19 +18,35 @@ VALUES
 (
 	'mono-regular',
 	'is',
-	'A category is <i>mono-regular</i> when every monomorphism is regular, i.e. the equalizer of a pair of morphisms. Notice that this is not standard terminology, <a href="https://math.stackexchange.com/questions/5031588" target="_blank">apparently</a> the literature has no name for this yet. A <i>preadditive</i> category is mono-regular iff every monomorphism is a kernel, and this type of category is commonly known as a <i>normal category</i>. We avoid this terminology here since it only applies to a certain type of categories, but mono-regular applies to all categories.',
+	'A category is <i>mono-regular</i> when every monomorphism is regular, i.e. the equalizer of a pair of morphisms. Notice that this is not standard terminology, <a href="https://math.stackexchange.com/questions/5031588" target="_blank">apparently</a> the literature has no name for this yet. A <i>preadditive</i> category is mono-regular iff it is normal. The notion of a normal category is reserved for categories with zero morphisms, while mono-regular applies to all categories.',
 	'https://ncatlab.org/nlab/show/regular+monomorphism',
 	'epi-regular',
 	TRUE
 ),
 (
 	'epi-regular',
 	'is',
-	'A category is <i>epi-regular</i> when every epimorphism is regular, i.e. the coequalizer of a pair of morphisms. Notice that this is not standard terminology, <a href="https://math.stackexchange.com/questions/5031588" target="_blank">apparently</a> the literature has no name for this yet. A <i>preadditive</i> category is epi-regular iff every epimorphism is a cokernel, and this type of category is commonly known as a <i>conormal category</i>. We avoid this terminology here since it only applies to a certain type of categories, but epi-regular applies to all categories.',
+	'A category is <i>epi-regular</i> when every epimorphism is regular, i.e. the coequalizer of a pair of morphisms. Notice that this is not standard terminology, <a href="https://math.stackexchange.com/questions/5031588" target="_blank">apparently</a> the literature has no name for this yet. A <i>preadditive</i> category is epi-regular iff it is conormal. The notion of a conormal category is reserved for categories with zero morphisms, while epi-regular applies to all categories.',
 	'https://ncatlab.org/nlab/show/regular+epimorphism',
 	'mono-regular',
 	TRUE
 ),
+(
+	'normal',
+	'is',
+	'A category is <i>normal</i> if it has zero morphisms and every monomorphism is a kernel of some morphism (in which case case it is also called a <i>normal monomorphism</i>). The assumption of having zero morphisms makes it possible to talk about kernels.',
+	'https://ncatlab.org/nlab/show/normal+monomorphism',
+	'conormal',
+	TRUE
+),
+(
+	'conormal',
+	'is',
+	'A category is <i>conormal</i> if it has zero morphisms and every epimorphism is a cokernel of some morphism (in which case case it is also called a <i>normal epimorphism</i>). The assumption of having zero morphisms makes it possible to talk about cokernels.',
+	'https://ncatlab.org/nlab/show/normal+epimorphism',
+	'normal',
+	TRUE
+),
 (
 	'left cancellative',
 	'is',

database/data/003_properties/100_related_properties.sql → database/data/003_properties/100_related-properties.sql

@@ -24,6 +24,10 @@ VALUES
 ('biproducts', 'finite products'),
 ('biproducts', 'finite coproducts'),
 ('abelian', 'additive'),
+('abelian', 'kernels'),
+('abelian', 'cokernels'),
+('abelian', 'normal'),
+('abelian', 'conormal'),
 ('finitely complete', 'complete'),
 ('finitely complete', 'finite products'),
 ('finitely complete', 'equalizers'),
@@ -54,8 +58,16 @@ VALUES
 ('complete', 'products'),
 ('equalizers', 'finitely complete'),
 ('equalizers', 'coreflexive equalizers'),
+('equalizers', 'kernels'),
 ('coequalizers', 'finitely cocomplete'),
 ('coequalizers', 'reflexive coequalizers'),
+('coequalizers', 'cokernels'),
+('kernels', 'zero morphisms'),
+('kernels', 'equalizers'),
+('kernels', 'normal'),
+('cokernels', 'zero morphisms'),
+('cokernels', 'coequalizers'),
+('cokernels', 'conormal'),
 ('cocomplete', 'coequalizers'),
 ('cocomplete', 'coproducts'),
 ('products', 'complete'),
@@ -252,4 +264,12 @@ VALUES
 ('filtered', 'finitely cocomplete'),
 ('filtered', 'filtered colimits'),
 ('cofiltered', 'finitely complete'),
-('cofiltered', 'cofiltered limits');
+('cofiltered', 'cofiltered limits'),
+('mono-regular', 'normal'),
+('epi-regular', 'conormal'),
+('normal', 'zero morphisms'),
+('normal', 'mono-regular'),
+('normal', 'kernels'),
+('conormal', 'zero morphisms'),
+('conormal', 'epi-regular'),
+('conormal', 'cokernels');

database/data/004_property-assignments/FinGrp.sql

@@ -55,9 +55,15 @@ VALUES
 ),
 (
 	'FinGrp',
-	'subobject classifier',
+	'conormal',
+	TRUE,
+	'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for finite groups.'
+),
+(
+	'FinGrp',
+	'normal',
 	FALSE,
-	'If there was a subgroup classifier $\Omega$, every subgroup of any finite group would be the kernel of a homomorphism to $\Omega$. But not every subgroup is normal.'
+	'Every non-normal subgroup of a finite group provides a counterexample.'
 ),
 (
 	'FinGrp',

database/data/004_property-assignments/Grp.sql

@@ -43,9 +43,15 @@ VALUES
 ),
 (
 	'Grp',
-	'subobject classifier',
+	'conormal',
+	TRUE,
+	'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for groups.'
+),
+(
+	'Grp',
+	'normal',
 	FALSE,
-	'If there was a subgroup classifier $\Omega$, every subgroup of any group would be the kernel of a homomorphism to $\Omega$. But not every subgroup is normal.'
+	'Every non-normal subgroup provides a counterexample.'
 ),
 (
 	'Grp',

database/data/004_property-assignments/Rel.sql

@@ -21,7 +21,7 @@ VALUES
 	'Rel',
 	'pointed',
 	TRUE,
-	'The empty set is clearly both initial and terminal.'
+	'The empty set is clearly both initial and terminal. The zero morphisms are the empty relations.'
 ),
 (
 	'Rel',
@@ -53,6 +53,12 @@ VALUES
 	TRUE,
 	'This is a consequence of the description of coproducts and products, both are disjoint unions (even for infinite families).'
 ),
+(
+	'Rel',
+	'kernels',
+	TRUE,
+	'Let $R : A \to B$ be a relation. Define $K = \bigl\{a \in A : \neg \exists b \in B ((a,b) \in R) \bigr\}$. We have an inclusion map $I : K \to A$, which can also be regarded as relation, and $R \circ I = \empty$ is the empty relation, i.e. the zero morphism. It is easy to check the universal property.'
+),
 (
 	'Rel',
 	'preadditive',
@@ -70,4 +76,10 @@ VALUES
 	'skeletal',
 	FALSE,
 	'This is trivial.'
+),
+(
+	'Rel',
+	'normal',
+	FALSE,
+	'The construction of equalizers in $\mathbf{Rel}$ shows that they are injective functions, but <a href="https://math.stackexchange.com/questions/350716" target="_blank">MSE/350716</a> shows that monomorphisms in $\mathbf{Rel}$ don''t have to be functions.'
 );

database/data/004_property-assignments/Set_pointed.sql

@@ -67,7 +67,7 @@ VALUES
 ),
 (
 	'Set*',
-	'quotient object classifier',
+	'conormal',
 	FALSE,
-	'If there was a quotient object classifier, every surjective pointed map would be a cokernel. However, every cokernel is "injective away from the base point". Formally, if $p : A \to B$ is a cokernel in $\mathbf{Set}_*$, it has the property that $p(x)=p(y) \neq 0$ implies $x=y$ (where $0$ denotes the base point). Clearly this is not satisfied for every surjective pointed map, consider $(\mathbb{N},0) \to (\{0,1\},0)$ defined by $0 \mapsto 0$ and $x \mapsto 1$ for $x > 0$.'
+	'Every cokernel is "injective away from the base point". Formally, if $p : A \to B$ is a cokernel in $\mathbf{Set}_*$, it has the property that $p(x)=p(y) \neq 0$ implies $x=y$ (where $0$ denotes the base point). Clearly this is not satisfied for every surjective pointed map, consider $(\mathbb{N},0) \to (\{0,1\},0)$ defined by $0 \mapsto 0$ and $x \mapsto 1$ for $x > 0$.'
 );

database/data/005_implications/001_limits-colimits-existence-implications.sql

@@ -139,6 +139,27 @@ VALUES
 	'If $e : X \to X$ is an idempotent, then the equalizer of $e, \mathrm{id}_X : X \rightrightarrows X$ provides a splitting of $e$.',
 	FALSE
 ),
+(
+	'kernels_condition',
+	'["kernels"]',
+	'["zero morphisms"]',
+	'This is part of our definition of having kernels.',
+	FALSE
+),
+(
+	'kernels_criterion',
+	'["zero morphisms", "equalizers"]',
+	'["kernels"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'equalizers_via_kernels',
+	'["preadditive", "kernels"]',
+	'["equalizers"]',
+	'The equalizer of $f,g$ is the kernel of $f-g$.',
+	FALSE
+),
 (
 	'sequential_colimits_consequence',
 	'["sequential colimits"]',

database/data/005_implications/004_morphism-behavior-implications.sql

@@ -104,6 +104,27 @@ VALUES
 	'Any regular monomorphism that is an epimorphism must be an isomorphism.',
 	FALSE
 ),
+(
+	'normal_condition',
+	'["normal"]',
+	'["zero morphisms"]',
+	'This is part of our definition of a normal category.',
+	FALSE
+),
+(
+	'mono_regular_via_kernels',
+	'["normal"]',
+	'["mono-regular"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'normal_criterion',
+	'["mono-regular", "preadditive"]',
+	'["normal"]',
+	'The a monomorphism is the equalizer of $f,g$, it is the kernel of $f-g$.',
+	FALSE
+),
 (
 	'direct_implies_one-way',
 	'["direct"]',

database/data/005_implications/005_additional-structure-implications.sql

@@ -44,7 +44,7 @@ VALUES
 (
 	'abelian_definition',
 	'["abelian"]',
-	'["additive", "equalizers", "coequalizers", "mono-regular", "epi-regular"]',
+	'["additive", "kernels", "cokernels", "normal", "conormal"]',
 	'This holds by definition.',
 	TRUE
 ),

database/data/005_implications/008_topos-theory-implications.sql

@@ -55,6 +55,13 @@ VALUES
 	'The first part holds by convention, and the second part: any monomorphism $U \to X$ is the equalizer of $\chi_U,\chi_X : X \to \Omega$.',
 	FALSE
 ),
+(
+	'subobject_classifier_pointed_case',
+	'["subobject classifier", "pointed"]',
+	'["normal"]',
+	'The universal property of $\top : 0 \to \Omega$ precisely says that every monomorphism $A \to B$ is the kernel of a unique morphism $B \to \Omega$, so it is normal.',
+	FALSE
+),
 (
 	'subobject_classifier_collapse',
 	'["subobject classifier", "strict terminal object"]',

scripts/expected-data/Ab.json

@@ -82,6 +82,10 @@
 	"cofiltered": true,
 	"sifted": true,
 	"cosifted": true,
+	"kernels": true,
+	"cokernels": true,
+	"normal": true,
+	"conormal": true,
 
 	"cartesian closed": false,
 	"locally cartesian closed": false,

scripts/expected-data/Set.json

@@ -120,5 +120,9 @@
 	"locally cocartesian coclosed": false,
 	"strongly connected": false,
 	"quotient object classifier": false,
-	"regular quotient object classifier": false
+	"regular quotient object classifier": false,
+	"kernels": false,
+	"cokernels": false,
+	"normal": false,
+	"conormal": false
 }

scripts/expected-data/Top.json

@@ -120,5 +120,9 @@
 	"locally cocartesian coclosed": false,
 	"strongly connected": false,
 	"quotient object classifier": false,
-	"regular quotient object classifier": false
+	"regular quotient object classifier": false,
+	"kernels": false,
+	"cokernels": false,
+	"normal": false,
+	"conormal": false
 }