add properties: subobject-trivial / quotient-trivial

Author: ScriptRaccoon

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/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
 }