diff --git a/database/data/003_properties/002_limits-colimits-existence.sql b/database/data/003_properties/002_limits-colimits-existence.sql
index 85f65b47..a13baac0 100644
--- a/database/data/003_properties/002_limits-colimits-existence.sql
+++ b/database/data/003_properties/002_limits-colimits-existence.sql
@@ -215,6 +215,22 @@ VALUES
'equalizers',
TRUE
),
+(
+ 'kernels',
+ 'has',
+ 'A category has kernels 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 cokernels 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',
diff --git a/database/data/003_properties/005_morphism-behavior.sql b/database/data/003_properties/005_morphism-behavior.sql
index cd8d400b..86b416e1 100644
--- a/database/data/003_properties/005_morphism-behavior.sql
+++ b/database/data/003_properties/005_morphism-behavior.sql
@@ -18,7 +18,7 @@ VALUES
(
'mono-regular',
'is',
- 'A category is mono-regular when every monomorphism is regular, i.e. the equalizer of a pair of morphisms. Notice that this is not standard terminology, apparently the literature has no name for this yet. A preadditive category is mono-regular iff every monomorphism is a kernel, and this type of category is commonly known as a normal category. 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 mono-regular when every monomorphism is regular, i.e. the equalizer of a pair of morphisms. Notice that this is not standard terminology, apparently the literature has no name for this yet. A preadditive 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
@@ -26,11 +26,27 @@ VALUES
(
'epi-regular',
'is',
- 'A category is epi-regular when every epimorphism is regular, i.e. the coequalizer of a pair of morphisms. Notice that this is not standard terminology, apparently the literature has no name for this yet. A preadditive category is epi-regular iff every epimorphism is a cokernel, and this type of category is commonly known as a conormal category. 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 epi-regular when every epimorphism is regular, i.e. the coequalizer of a pair of morphisms. Notice that this is not standard terminology, apparently the literature has no name for this yet. A preadditive 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 normal if it has zero morphisms and every monomorphism is a kernel of some morphism (in which case case it is also called a normal monomorphism). 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 conormal if it has zero morphisms and every epimorphism is a cokernel of some morphism (in which case case it is also called a normal epimorphism). 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',
diff --git a/database/data/003_properties/100_related_properties.sql b/database/data/003_properties/100_related-properties.sql
similarity index 94%
rename from database/data/003_properties/100_related_properties.sql
rename to database/data/003_properties/100_related-properties.sql
index e05c8483..724d263d 100644
--- a/database/data/003_properties/100_related_properties.sql
+++ b/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');
\ No newline at end of file
+('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');
\ No newline at end of file
diff --git a/database/data/004_property-assignments/FinGrp.sql b/database/data/004_property-assignments/FinGrp.sql
index de11c7ee..096cc4aa 100644
--- a/database/data/004_property-assignments/FinGrp.sql
+++ b/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',
diff --git a/database/data/004_property-assignments/Grp.sql b/database/data/004_property-assignments/Grp.sql
index 82be805c..8b4feaad 100644
--- a/database/data/004_property-assignments/Grp.sql
+++ b/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',
diff --git a/database/data/004_property-assignments/Rel.sql b/database/data/004_property-assignments/Rel.sql
index 17bbb152..adef9a73 100644
--- a/database/data/004_property-assignments/Rel.sql
+++ b/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 MSE/350716 shows that monomorphisms in $\mathbf{Rel}$ don''t have to be functions.'
);
diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql
index c170c0b4..efe845f3 100644
--- a/database/data/004_property-assignments/Set_pointed.sql
+++ b/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$.'
);
diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql
index 03676930..15eaa5a3 100644
--- a/database/data/005_implications/001_limits-colimits-existence-implications.sql
+++ b/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"]',
diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql
index 59160bee..76eb8456 100644
--- a/database/data/005_implications/004_morphism-behavior-implications.sql
+++ b/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"]',
diff --git a/database/data/005_implications/005_additional-structure-implications.sql b/database/data/005_implications/005_additional-structure-implications.sql
index 203e6005..97962495 100644
--- a/database/data/005_implications/005_additional-structure-implications.sql
+++ b/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
),
diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql
index 738db56c..418e8223 100644
--- a/database/data/005_implications/008_topos-theory-implications.sql
+++ b/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"]',
diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json
index 52b1c8c6..b387f2e5 100644
--- a/scripts/expected-data/Ab.json
+++ b/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,
diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json
index 946d3f50..e714c158 100644
--- a/scripts/expected-data/Set.json
+++ b/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
}
diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json
index 35c6f9fe..0458704a 100644
--- a/scripts/expected-data/Top.json
+++ b/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
}