Add properties: subobject-trivial and quotient-trivial

databases/catdat/data/002_category-properties/004_morphism-behavior.sql

@@ -142,4 +142,20 @@ VALUES
 	'https://ncatlab.org/nlab/show/gaunt+category',
 	'gaunt',
 	FALSE
+),
+(
+	'subobject-trivial',
+	'is',
+	'A category is <i>subobject-trivial</i> if every monomorphism is an isomorphism. Equivalently, the poset of subobjects of any object is trivial. This is no standard terminology. We have added it to the database since it clarifies the relationship between several related properties.',
+	NULL,
+	'quotient-trivial',
+	TRUE
+),
+(
+	'quotient-trivial',
+	'is',
+	'A category is <i>quotient-trivial</i> if every epimorphism is an isomorphism. Equivalently, the poset of quotients of any object is trivial. This is no standard terminology. We have added it to the database since it clarifies the relationship between several related properties.',
+	NULL,
+	'subobject-trivial',
+	TRUE
 );

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

@@ -231,6 +231,8 @@ VALUES
 ('right cancellative', 'groupoid'),
 ('groupoid', 'left cancellative'),
 ('groupoid', 'right cancellative'),
+('groupoid', 'subobject-trivial'),
+('groupoid', 'quotient-trivial'),
 ('wide pullbacks', 'pullbacks'),
 ('wide pushouts', 'pushouts'),
 ('split abelian', 'abelian'),
@@ -339,7 +341,9 @@ VALUES
 ('cofiltered', 'finitely complete'),
 ('cofiltered', 'cofiltered limits'),
 ('mono-regular', 'normal'),
+('mono-regular', 'subobject-trivial'),
 ('epi-regular', 'conormal'),
+('epi-regular', 'quotient-trivial'),
 ('normal', 'zero morphisms'),
 ('normal', 'mono-regular'),
 ('normal', 'kernels'),
@@ -403,4 +407,8 @@ VALUES
 ('CSP', 'zero morphisms'),
 ('CSP', 'unital'),
 ('CSP', 'cofiltered-limit-stable epimorphisms'),
-('finitary algebraic', 'locally strongly finitely presentable');
+('finitary algebraic', 'locally strongly finitely presentable'),
+('subobject-trivial', 'mono-regular'),
+('subobject-trivial', 'groupoid'),
+('quotient-trivial', 'epi-regular'),
+('quotient-trivial', 'groupoid');

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

@@ -53,12 +53,6 @@ VALUES
 	TRUE,
 	'If $f : X \to Y$ is an injective map of finite sets, it is the equalizer of the two injective maps $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$, and $Y \sqcup_X Y$ is finite.'
 ),
-(
-	'FI',
-	'epi-regular',
-	TRUE,
-	'This is because every epimorphism is actually an isomorphism (see below).'
-),
 (
 	'FI',
 	'semi-strongly connected',
@@ -71,12 +65,6 @@ VALUES
 	TRUE,
 	'IF $X$ is a finite set, the slice category $\mathbf{FI} / X$ is equivalent to the poset of subsets of $X$. This is cartesian closed because $A \cap B \subseteq C$ holds if and only if $B \subseteq (X \setminus A) \cup C$, where $A,B,C \subseteq X$.'
 ),
-(
-	'FI',
-	'cofiltered-limit-stable epimorphisms',
-	TRUE,
-	'This is because every epimorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of limit.'
-),
 (
 	'FI',
 	'small',

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

@@ -41,24 +41,12 @@ VALUES
 	TRUE,
 	'We construct coequalizers as in $\mathbf{FinSet}$ (or $\mathbf{Set}$) and observe that the universal property still holds when we restrict to surjective maps.'
 ),
-(
-	'FS',
-	'mono-regular',
-	TRUE,
-	'Every monomorphism is an isomorphism (see below), hence regular.'
-),
 (
 	'FS',
 	'epi-regular',
 	TRUE,
 	'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.'
 ),
-(
-	'FS',
-	'filtered-colimit-stable monomorphisms',
-	TRUE,
-	'This is because every monomorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of colimit.'
-),
 (
 	'FS',
 	'multi-terminal object',

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

@@ -37,7 +37,7 @@ VALUES
 ),
 (
 	'walking_idempotent',
-	'mono-regular',
+	'subobject-trivial',
     TRUE,
 	'This is because the identity is the only monomorphism.'
 ),

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

@@ -59,18 +59,6 @@ VALUES
 	FALSE,
 	'$0$ is not initial since it has two morphisms to $1$, and $1$ has not initial since it has no morphism to $0$.'
 ),
-(
-	'walking_pair',
-	'binary products',
-	FALSE,
-	'We cannot have $0 \times 1 = 1$ since there is no morphism $1 \to 0$. So assume $0 \times 1 = 0$, say with projections $\mathrm{id}_0 : 0 \to 0$ and $a : 0 \to 1$. By applying the universal property to  $\mathrm{id}_0 : 0 \to 0$ and the other morphism $b : 0 \to 1$, it immediately follows $a=b$, which is a contradiction.'
-),
-(
-	'walking_pair',
-	'equalizers',
-	FALSE,
-	'The two morphisms $a,b : 0 \rightrightarrows 1$ have no equalizer, since it would have to be the identity of $0$, but $a \neq b$.'
-),
 (
 	'walking_pair',
 	'pullbacks',

databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql

@@ -41,6 +41,13 @@ VALUES
 	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
 	FALSE
 ),
+(
+	'reflexive_pair_trivial_2',
+	'["subobject-trivial"]',
+	'["reflexive coequalizers", "coreflexive equalizers"]',
+	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
+	FALSE
+),
 (
 	'groupoid_consequence',
 	'["groupoid"]',
@@ -168,6 +175,13 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
+(
+	'filtered_monos_iso',
+	'["subobject-trivial", "filtered colimits"]',
+	'["filtered-colimit-stable monomorphisms"]',
+	'This is trivial.',
+	FALSE
+),
 (
 	'thin_groupoids',
 	'["groupoid", "core-thin"]',
@@ -188,4 +202,32 @@ VALUES
 	'["skeletal", "core-thin"]',
 	'This is trivial.',
 	TRUE
+),
+(
+	'thin_subobject-trivial',
+	'["subobject-trivial", "equalizers"]',
+	'["thin"]',
+	'If $f,g : X \rightrightarrows Y$ are morphisms, their equalizer is a monomorphism $E \hookrightarrow X$, hence an isomorphism. But this means $f = g$.',
+	FALSE
+),
+(
+	'subobject-trivial_consequence',
+	'["subobject-trivial"]',
+	'["mono-regular"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'subobject-trivial_groupoids',
+	'["groupoid"]',
+	'["subobject-trivial"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'subobject-trivial_criterion',
+	'["right cancellative", "epi-regular"]',
+	'["subobject-trivial"]',
+	'This is because a monomorphism which is also a regular epimorphism is an isomorphism.',
+	FALSE
 );

databases/catdat/scripts/expected-data/Ab.json

@@ -153,5 +153,7 @@
 	"cofiltered-limit-stable epimorphisms": false,
 	"exact cofiltered limits": false,
 	"gaunt": false,
-	"core-thin": false
+	"core-thin": false,
+	"subobject-trivial": false,
+	"quotient-trivial": false
 }

databases/catdat/scripts/expected-data/Set.json

@@ -153,5 +153,7 @@
 	"cofiltered-limit-stable epimorphisms": false,
 	"exact cofiltered limits": false,
 	"gaunt": false,
-	"core-thin": false
+	"core-thin": false,
+	"subobject-trivial": false,
+	"quotient-trivial": false
 }

databases/catdat/scripts/expected-data/Top.json

@@ -153,5 +153,7 @@
 	"cofiltered-limit-stable epimorphisms": false,
 	"exact cofiltered limits": false,
 	"gaunt": false,
-	"core-thin": false
+	"core-thin": false,
+	"subobject-trivial": false,
+	"quotient-trivial": false
 }