Add Barr-exact, Barr-coexact, pretopos properties

database/data/003_properties/003_limits-colimits-behavior.sql

@@ -196,6 +196,22 @@ VALUES
 	'infinitary extensive',
 	TRUE
 ),
+(
+	'Barr-exact',
+	'is',
+	'A category is <i>Barr-exact</i> if it is regular, and in addition, every internal equivalence relation is a kernel pair.  (Note that because of the regularity condition, that is equivalent to being the kernel pair of a coequalizer of the two projections.)',
+	'https://ncatlab.org/nlab/show/exact',
+	'Barr-coexact',
+	TRUE
+),
+(
+	'Barr-coexact',
+	'is',
+	'A category is <i>Barr-coexact</i> if its dual is Barr-exact, i.e. it is coregular, and in addition, every internal equivalence corelation is a cokernel pair.  (Note that because of the coregularity condition, that is equivalent to being the cokernel pair of an equalizer of the two coprojections.)',
+	NULL,
+	'Barr-exact',
+	TRUE
+),
 (
 	'unital',
 	'is',
@@ -211,4 +227,4 @@ VALUES
 	NULL,
 	'unital',
 	TRUE
-);
+);

database/data/003_properties/006_additional-structure.sql

@@ -62,4 +62,12 @@ VALUES
 	'https://ncatlab.org/nlab/show/Grothendieck+category',
 	NULL,
 	TRUE
-);
+),
+(
+	'monadically concrete',
+	'is',
+	'A category is <i>monadically concrete</i> if there exists a monadic functor to Set. Note this is not standard terminology, but is used in the CatDat system for its numerous implications.',
+	NULL,
+	NULL,
+	TRUE
+);

database/data/003_properties/009_topos-theory.sql

@@ -83,6 +83,14 @@ VALUES
 	'regular subobject classifier',
 	TRUE
 ),
+(
+	'pretopos',
+	'is a',
+	'A <i>pretopos</i> is a category which is both Barr-exact and extensive.',
+	'https://ncatlab.org/nlab/show/pretopos',
+	NULL,
+	TRUE
+),
 (
 	'elementary topos',
 	'is an',
@@ -109,4 +117,4 @@ VALUES
 	'https://ncatlab.org/nlab/show/natural+numbers+object',
 	NULL,
 	TRUE
-);
+);

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

@@ -60,7 +60,13 @@ VALUES
 ('elementary topos', 'finitely complete'),
 ('elementary topos', 'subobject classifier'),
 ('elementary topos', 'natural numbers object'),
+('elementary topos', 'pretopos'),
 ('Grothendieck topos', 'elementary topos'),
+('Grothendieck topos', 'pretopos'),
+('pretopos', 'extensive'),
+('pretopos', 'Barr-exact'),
+('pretopos', 'elementary topos'),
+('pretopos', 'Grothendieck topos'),
 ('natural numbers object', 'elementary topos'),
 ('natural numbers object', 'finite products'),
 ('initial object', 'finite coproducts'),
@@ -229,6 +235,10 @@ VALUES
 ('strongly connected', 'inhabited'),
 ('regular', 'finitely complete'),
 ('coregular', 'finitely cocomplete'),
+('Barr-exact', 'regular'),
+('Barr-exact', 'coequalizers'),
+('Barr-coexact', 'coregular'),
+('Barr-coexact', 'equalizers'),
 ('extensive', 'infinitary extensive'),
 ('extensive', 'finite coproducts'),
 ('extensive', 'disjoint finite coproducts'),

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

@@ -49,9 +49,9 @@ VALUES
 ),
 (
 	'FinGrp',
-	'regular', 
+	'Barr-exact', 
 	TRUE,
-	'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.'
+	'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. This shows the category is regular. For exactness, quotients of equivalence relations are inherited from Group, with a quotient of a finite group clearly being finite as well.'
 ),
 (
 	'FinGrp',
@@ -118,4 +118,4 @@ VALUES
 	'countable',
 	FALSE,
 	'This is trivial.'
-);
+);

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

@@ -47,6 +47,12 @@ VALUES
 	TRUE,
 	'The inclusion $\mathbf{FinSet} \hookrightarrow \mathbf{Set}$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\mathbf{Set}$, it is still ℵ₁-presentable in $\mathbf{FinSet}$. Therefore, $\mathbf{FinSet}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.'
 ),
+(
+	'FinSet',
+	'Barr-coexact',
+	TRUE,
+	'If an equivalence corelation is a cokernel pair of $f : Y \to X$ where $Y$ is gotten from Barr-coexactness of $\mathbf{Set}$, then we can replace $Y$ with the appropriate equalizer which is finite.'
+),
 (
 	'FinSet',
 	'small',

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

@@ -84,4 +84,10 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509715" target="_blank">MO/509715</a>.'
-);
+),
+(
+	'FreeAb',
+	'Barr-exact',
+	FALSE,
+	'Any kernel pair $E$ of a morphism to a free Abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$.  However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.'
+);

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

@@ -94,4 +94,11 @@ VALUES
 	'regular subobject classifier',
 	FALSE,
 	'Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\mathrm{Hom}(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\mathrm{Hom}(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).'
+),
+(
+	'Haus',
+	'Barr-exact',
+	FALSE,
+	'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.'
 );
+

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

@@ -144,4 +144,4 @@ VALUES
 	'If $(N,z,s)$ is a natural numbers object in $\mathbf{Met}$, then
 	<p>$1 \xrightarrow{z} N \xleftarrow{s} N$</p>
 	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
-);
+);

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

@@ -100,4 +100,10 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a>.'
+),
+(
+	'Met_c',
+	'Barr-exact',
+	FALSE,
+	'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.'
 );

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

@@ -82,4 +82,10 @@ VALUES
 	'co-Malcev',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509552">MO/509552</a>: Consider the forgetful functor $U : \mathbf{Met}_{\infty} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(a,b) \in U(X)^2 : d(x,y) \leq 1 \}$. Both are representable: $U$ by the singleton metric space and $R$ by the metric space $\{ 0,1 \}$ where $d(0,1) := 1$. It is clear that $R$ is reflexive, but not transitive.'
+),
+(
+	'Met_oo',
+	'Barr-exact',
+	FALSE,
+	'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.'
 );

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

@@ -94,4 +94,10 @@ VALUES
 	'co-Malcev',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509552">MO/509552</a>: Consider the forgetful functor $U : \mathbf{Prost} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.'
+),
+(
+	'Prost',
+	'Barr-coexact',
+	FALSE,
+	'Consider the space $X$ with one point, and the corelation $R$ with two points and the full relation.  Then for any $Y$, the morphisms $R \to Y$ correspond to pairs of points $(y_1, y_2) \in Y \times Y$ such that $y_1 \le y_2$ and $y_2 \le y_1$, which induces an equivalence relation on pairs of maps $X \to Y$.  It follows that $R$ is an equivalence corelation.  However, the equalizer of the two maps $X \to R$ is empty, and the cokernel pair of the map $\emptyset \to X$ is the proset with two elements and the equality relation.'
 );

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

@@ -29,6 +29,12 @@ VALUES
 	TRUE,
 	'Use the empty algebraic theory.'
 ),
+(
+	'Set',
+	'Barr-coexact',
+	TRUE,
+	'$\mathbf{Set}^{\operatorname{op}}$ is monadic over $\mathbf{Set}$.'
+),
 (
 	'Set',
 	'skeletal',
@@ -40,4 +46,10 @@ VALUES
 	'Malcev',
 	FALSE,
 	'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.'
+),
+(
+	'Set_op',
+	'monadically concrete',
+	TRUE,
+	'The contravariant powerset functor $\mathsf{Set}^{\operatorname{op}} \to \mathsf{Set}$ is monadic.'
 );

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

@@ -43,9 +43,9 @@ VALUES
 ),
 (
 	'Set*',
-	'coregular',
+	'Barr-coexact',
 	TRUE,
-	'From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for the <a href="/category/Set">category of sets</a> and the observation that the forgetful functor $\mathbf{Set}_* \to \mathbf{Set}$ preserves pushouts.'
+	'According to <a href="https://ncatlab.org/nlab/show/exact+category">nLab</a> with a citation to <a href="http://www.springer.com/us/book/9781402019616">Borceux and Bourn</a>, Appendix A, any slice or co-slice of a Barr-exact category is also Barr-exact.  It follows that any slice or co-slice of a Barr-coexact category is also Barr-coexact, and $\mathbf{Set}_*$ is a coslice category of $\mathbf{Set}$, which is Barr-coexact since $\mathbf{Set}^{\operatorname{op}}$ is monadic over $\mathbf{Set}$.'
 ),
 (
 	'Set*',

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

@@ -23,6 +23,12 @@ VALUES
     TRUE,
     'Take the two-sorted algebraic theory with no operations and no equations.'
 ),
+(
+	'SetxSet',
+	'Barr-coexact',
+	TRUE,
+	'$(\mathbf{Set} \times \mathbf{Set})^{\operatorname{op}}$ is monadic over $\mathbf{Set} \times \mathbf{Set}$.'
+),
 (
 	'SetxSet',
 	'skeletal',

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

@@ -118,4 +118,10 @@ VALUES
 	'coaccessible',
 	FALSE,
 	'Assume $\mathbf{Top}$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\mathbf{Set}$, is coaccessible by Prop. 4.7 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since $\mathbf{Set}$ is not coaccessible, this is a contradiction.'
+),
+(
+	'Top',
+	'Barr-coexact',
+	FALSE,
+	'Consider the one-point space $X$, and $R$ is the corelation with two points and the indiscrete topology.  Then for any space $Y$, the continuous functions $R \to Y$ correspond to the pairs of points which are indistinguishable in $Y$, which induces an equivalence relation on the pairs of maps $X \to Y$; this implies that $R$ is an equivalence corelation on $X$.  However, the equalizer of the two maps $X \to R$ is empty, and the map $\emptyset \to X$ has cokernel pair given by the two-point discrete space.'
 );

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

@@ -143,7 +143,10 @@ VALUES
 	'coaccessible',
 	FALSE,
 	'We can adjust the proof for $\mathbf{Top}$ as follows: Assume $\mathbf{Top}_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\mathbf{Set}_*$, is coaccessible by Prop. 4.7 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since $\mathbf{Set}_*$ is not coaccessible, this is a contradiction.'
+),
+(
+	'Top*',
+	'Barr-coexact',
+	FALSE,
+	'Consider the two-point discrete space $X$, and $R$ is the corelation with three points $\{ *, a, b \}$ and topology $\{ \emptyset, \{ * \}, \{ a, b \}, \{ *, a, b \}$.  Then for any space $Y$, the continuous functions $R \to Y$ correspond to the pairs of points which are indistinguishable in $Y$, which induces an equivalence relation on the pairs of maps $X \to Y$; this implies that $R$ is an equivalence corelation on $X$.  However, the equalizer of the two maps $X \to R$ is just the base point, and the map $\{ * \} \to X$ has cokernel pair given by the three-point discrete space.'
 );
-
-
-

database/data/005_implications/002_limits-colimits-behavior-implications.sql

@@ -251,6 +251,13 @@ VALUES
 	'This holds by definition of a regular category.',
 	FALSE
 ),
+(
+	'barr_exact_def',
+	'["Barr-exact"]',
+	'["regular"]',
+	'By definition',
+	FALSE
+),
 (
 	'power_construction',
 	'["copowers", "cartesian closed"]',
@@ -268,4 +275,4 @@ VALUES
 	'["countable powers"]',
 	'We can recycle <a href="/category-implication/power_construction">this proof</a>.',
 	FALSE
-);
+);

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

@@ -7,10 +7,17 @@ INSERT INTO implication_input (
 )
 VALUES
 (
-	'finitary_algebraic_consequence',
+	'finitary_algebraic_consequences',
 	'["finitary algebraic"]',
-	'["locally strongly finitely presentable"]',
-	'This is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras.',
+	'["locally strongly finitely presentable", "monadically concrete"]',
+	'The first is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras. For the second, the forgetful functor to Set is monadic because the corresponding monad on Set takes a set to the collection of formal expressions in those variables modulo provable equality, and so it is easy to see an equivalence between an algebra over that monad and a model of the algebraic theory.',
+	FALSE
+),
+(
+	'monadically_concrete_consequences',
+	'["monadically concrete"]',
+	'["complete", "cocomplete", "Barr-exact", "locally essentially small"]',
+	'It is complete because a monadic functor creates limits.  For cocompleteness, see for example Handbook of Categorial Algebra Vol. 2, Thm. 4.3.5.  For Barr-exactness, see <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact">here</a>.  The local smallness condition is easy from the fact that the monadic functor must be faithful.',
 	FALSE
 ),
 (
@@ -49,10 +56,10 @@ VALUES
 	TRUE
 ),
 (
-	'abelian_implies_regular',
+	'abelian_implies_exact',
 	'["abelian"]',
-	'["regular"]',
-	'In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.',
+	'["Barr-exact"]',
+	'In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.  This shows the category is regular.  For exactness, strict quotients of internal equivalence relations can be constructed as cokernels.',
 	FALSE
 ),
 (
@@ -110,4 +117,4 @@ VALUES
 	'["trivial"]',
 	'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, <i>Abelian categories</i>, p. 116.',
 	FALSE
-);
+);

database/data/005_implications/006_trivial-categories-implications.sql

@@ -119,10 +119,10 @@ VALUES
 	FALSE
 ),
 (
-	'thin_implies_regular',
+	'thin_implies_barr_exact',
 	'["thin", "finitely complete"]',
-	'["regular"]',
-	'In a thin category, regular epimorphisms are isomorphisms, and the rest is clear as well.',
+	'["Barr-exact"]',
+	'In a thin category, regular epimorphisms are isomorphisms, and the rest of regularity is clear as well.  For exactness, any internal equivalence relation (in fact any reflexive relation) is the full relation i.e. an isomorphism, and is therefore the kernel pair of the identity map.',
 	FALSE
 ),
 (
@@ -152,4 +152,4 @@ VALUES
 	'["exact filtered colimits"]',
 	'In a thin category, every (finite) limit can be reduced to a (finite) product.',
 	FALSE
-);
+);

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

@@ -41,13 +41,34 @@ VALUES
 	'If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal.',
 	FALSE
 ),
+(
+	'pretopos_definition',
+	'["pretopos"]',
+	'["Barr-exact", "extensive"]',
+	'By definition.',
+	TRUE
+),
+(
+	'pretopos_consequence',
+	'["pretopos"]',
+	'["balanced"]',
+	'See <a href="https://ncatlab.org/nlab/show/balanced+category">NLab, Example 2.2</a> with a citation of Peter Johnstone, Cor. 1.22 in: Topos theory, London Math. Soc. Monographs 10, Acad. Press (1977), Dover (2014).',
+	FALSE
+),
 (
 	'topos_definition',
 	'["elementary topos"]',
 	'["cartesian closed", "finitely complete", "subobject classifier"]',
 	'This holds by definition.',
 	TRUE
 ),
+(
+	'topos_pretopos',
+	'["elementary topos"]',
+	'["pretopos"]',
+	'All properties of a pretopos can be proved in a way similar to the way they are proved for Set, using the internal language and internal logic of an elementary topos.',
+	FALSE
+),
 (
 	'subobject_classifier_consequence',
 	'["subobject classifier"]',
@@ -222,4 +243,4 @@ VALUES
 	'["natural numbers object"]',
 	'The triple $(1, \mathrm{id}_1, \mathrm{id}_1)$ is clearly a NNO.',
 	FALSE
-);
+);