Add Barr-(co)exact properties

databases/catdat/data/categories/CompHaus.yaml

@@ -38,13 +38,8 @@ satisfied_properties:
   - property: cogenerator
     reason: 'The unit interval $[0, 1]$ is a cogenerator: Suppose we have $f, g : X \rightrightarrows Y$ with $f \ne g$. Choose $x\in X$ such that $f(x) \ne g(x)$. Then by Urysohn''s lemma, there is a continuous function $h : Y \to [0, 1]$ such that $h(f(x)) = 0$ and $h(g(x)) = 1$. Therefore, $h\circ f \ne h\circ g$.'
 
-  - property: effective congruences
-    # TODO: rework this when Barr-exact is added
-    reason: The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space#compact_hausdorff_spaces_are_monadic_over_sets">nLab</a>. Therefore, by <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact">this result</a>, $\CompHaus$ is Barr-exact, and in particular it has effective congruences.
-
-  - property: regular
-    # TODO: rework this when Barr-exact is added
-    reason: The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space#compact_hausdorff_spaces_are_monadic_over_sets">nLab</a>. Therefore, by <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact">this result</a>, $\CompHaus$ is Barr-exact and in particular is regular.
+  - property: Barr-exact
+    reason: The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space#compact_hausdorff_spaces_are_monadic_over_sets">nLab</a>. Therefore, by <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact">this result</a>, $\CompHaus$ is Barr-exact.
 
   - property: coregular
     reason:

databases/catdat/data/categories/Set_pointed.yaml

@@ -35,6 +35,7 @@ satisfied_properties:
 
   - property: coregular
     reason: 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 <a href="/category/Set">$\Set$</a> and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts.
+    check_redundancy: false
 
   - property: co-Malcev
     reason: Malcev categories are closed under slice categories by Prop. 2.2.14 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of <a href="/category/Set">$\Set$</a>, which is co-Malcev since every elementary topos is co-Malcev.
@@ -48,9 +49,8 @@ satisfied_properties:
   - property: CIP
     reason: The coproduct (wedge sum) of a family of pointed sets $(X_i)_{i \in I}$ can be realized as the subset of $\prod_{i \in I} X_i$ consisting of those tuples $x$ such that $x_i = 0$ for all but (at most) one index.
 
-  - property: effective cocongruences
-    # TODO: rework this when Barr-exact is added
-    reason: We have that $\Set_*^{\op}$ is a slice category of $\Set^{\op}$, which in turn is monadic over $\Set$. Therefore, by combining results from <a href="http://www.springer.com/us/book/9781402019616" target="_blank">Borceux and Bourn</a> Appendix A and <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact" target="_blank">nLab</a>, $\Set_*^{\op}$ is Barr-exact, and in particular it has effective congruences.
+  - property: Barr-coexact
+    reason: We have that $\Set_*^{\op}$ is a slice category of $\Set^{\op}$, which in turn is monadic over $\Set$. Therefore, by combining results from <a href="http://www.springer.com/us/book/9781402019616" target="_blank">Borceux and Bourn</a> Appendix A and <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact" target="_blank">nLab</a>, $\Set_*^{\op}$ is Barr-exact.
 
 unsatisfied_properties:
   - property: skeletal

databases/catdat/data/category-implications/congruences.yaml

@@ -129,3 +129,12 @@
     \end{align*}$$
     on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B' \to C$ such that $f, g$ is the kernel pair of $h$, that is, two generalized elements $x, y \in B + B'$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$, $y = g(e)$ for some $e \in E$. In particular, for $x \in B$, we have $h(x) = h(x')$ if and only if $x = f(e)$, $x' = g(e)$ for some $e \in E$. By disjointness of coproducts, we must necessarily have $e \in A$, and $x = \alpha(e)$. This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$.
   is_equivalence: false
+
+- id: Barr-exact_definition
+  assumptions:
+    - Barr-exact
+  conclusions:
+    - regular
+    - effective congruences
+  reason: This holds by definition.
+  is_equivalence: true

databases/catdat/data/category-properties/Barr-coexact.yaml

@@ -0,0 +1,10 @@
+id: Barr-coexact
+relation: is
+description: A category is <i>Barr-coexact</i> if its dual category is Barr-exact, i.e. if it is coregular and every cocongruence is effective.
+dual_property: Barr-exact
+invariant_under_equivalences: true
+
+related_properties:
+  - coregular
+  - effective cocongruences
+  - coquotients of cocongruences

databases/catdat/data/category-properties/Barr-exact.yaml

@@ -0,0 +1,11 @@
+id: Barr-exact
+relation: is
+description: A category is <i>Barr-exact</i> if it is regular and every congruence is effective.
+nlab_link: https://ncatlab.org/nlab/show/exact+category
+dual_property: Barr-coexact
+invariant_under_equivalences: true
+
+related_properties:
+  - regular
+  - effective congruences
+  - quotients of congruences

databases/catdat/data/category-properties/coquotients of cocongruences.yaml

@@ -9,3 +9,4 @@ related_properties:
   - effective cocongruences
   - equalizers
   - kernels
+  - Barr-coexact

databases/catdat/data/category-properties/coregular.yaml

@@ -7,3 +7,4 @@ invariant_under_equivalences: true
 related_properties:
   - coquotients of cocongruences
   - finitely cocomplete
+  - Barr-coexact

databases/catdat/data/category-properties/effective cocongruences.yaml

@@ -11,3 +11,4 @@ related_properties:
   - conormal
   - coquotients of cocongruences
   - epi-regular
+  - Barr-coexact

databases/catdat/data/category-properties/effective congruences.yaml

@@ -12,3 +12,4 @@ related_properties:
   - mono-regular
   - normal
   - quotients of congruences
+  - Barr-exact

databases/catdat/data/category-properties/quotients of congruences.yaml

@@ -10,3 +10,4 @@ related_properties:
   - cokernels
   - effective congruences
   - regular
+  - Barr-exact

databases/catdat/data/category-properties/regular.yaml

@@ -8,3 +8,4 @@ invariant_under_equivalences: true
 related_properties:
   - finitely complete
   - quotients of congruences
+  - Barr-exact

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

@@ -106,6 +106,8 @@
 	"coquotients of cocongruences": true,
 	"effective congruences": true,
 	"effective cocongruences": true,
+	"Barr-coexact": true,
+	"Barr-exact": true,
 
 	"cartesian closed": false,
 	"locally cartesian closed": false,

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

@@ -101,6 +101,8 @@
 	"coquotients of cocongruences": true,
 	"effective congruences": true,
 	"effective cocongruences": true,
+	"Barr-coexact": true,
+	"Barr-exact": true,
 
 	"Grothendieck abelian": false,
 	"Malcev": false,

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

@@ -158,5 +158,7 @@
 	"quotient-trivial": false,
 	"effective congruences": false,
 	"effective cocongruences": false,
-	"locally finite": false
+	"locally finite": false,
+	"Barr-coexact": false,
+	"Barr-exact": false
 }