diff --git a/databases/catdat/data/categories/CompHaus.yaml b/databases/catdat/data/categories/CompHaus.yaml index 0ee0c8e6..40f50df0 100644 --- a/databases/catdat/data/categories/CompHaus.yaml +++ b/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 nLab. Therefore, by this result, $\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 nLab. Therefore, by this result, $\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 nLab. Therefore, by this result, $\CompHaus$ is Barr-exact. - property: coregular reason: diff --git a/databases/catdat/data/categories/Set_pointed.yaml b/databases/catdat/data/categories/Set_pointed.yaml index 47075655..99e6d452 100644 --- a/databases/catdat/data/categories/Set_pointed.yaml +++ b/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 $\Set$ 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 Malcev, protomodular, homological and semi-abelian categories. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of $\Set$, 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 Borceux and Bourn Appendix A and nLab, $\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 Borceux and Bourn Appendix A and nLab, $\Set_*^{\op}$ is Barr-exact. unsatisfied_properties: - property: skeletal diff --git a/databases/catdat/data/category-implications/congruences.yaml b/databases/catdat/data/category-implications/congruences.yaml index 689225cd..7496b165 100644 --- a/databases/catdat/data/category-implications/congruences.yaml +++ b/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 diff --git a/databases/catdat/data/category-properties/Barr-coexact.yaml b/databases/catdat/data/category-properties/Barr-coexact.yaml new file mode 100644 index 00000000..d7893c07 --- /dev/null +++ b/databases/catdat/data/category-properties/Barr-coexact.yaml @@ -0,0 +1,10 @@ +id: Barr-coexact +relation: is +description: A category is Barr-coexact 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 diff --git a/databases/catdat/data/category-properties/Barr-exact.yaml b/databases/catdat/data/category-properties/Barr-exact.yaml new file mode 100644 index 00000000..e4004125 --- /dev/null +++ b/databases/catdat/data/category-properties/Barr-exact.yaml @@ -0,0 +1,11 @@ +id: Barr-exact +relation: is +description: A category is Barr-exact 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 diff --git a/databases/catdat/data/category-properties/coquotients of cocongruences.yaml b/databases/catdat/data/category-properties/coquotients of cocongruences.yaml index 203730b3..2bf9b64a 100644 --- a/databases/catdat/data/category-properties/coquotients of cocongruences.yaml +++ b/databases/catdat/data/category-properties/coquotients of cocongruences.yaml @@ -9,3 +9,4 @@ related_properties: - effective cocongruences - equalizers - kernels + - Barr-coexact diff --git a/databases/catdat/data/category-properties/coregular.yaml b/databases/catdat/data/category-properties/coregular.yaml index b5b98413..ed9d719d 100644 --- a/databases/catdat/data/category-properties/coregular.yaml +++ b/databases/catdat/data/category-properties/coregular.yaml @@ -7,3 +7,4 @@ invariant_under_equivalences: true related_properties: - coquotients of cocongruences - finitely cocomplete + - Barr-coexact diff --git a/databases/catdat/data/category-properties/effective cocongruences.yaml b/databases/catdat/data/category-properties/effective cocongruences.yaml index a0c00327..85c2fe42 100644 --- a/databases/catdat/data/category-properties/effective cocongruences.yaml +++ b/databases/catdat/data/category-properties/effective cocongruences.yaml @@ -11,3 +11,4 @@ related_properties: - conormal - coquotients of cocongruences - epi-regular + - Barr-coexact diff --git a/databases/catdat/data/category-properties/effective congruences.yaml b/databases/catdat/data/category-properties/effective congruences.yaml index 004d99ee..ed2ecc2e 100644 --- a/databases/catdat/data/category-properties/effective congruences.yaml +++ b/databases/catdat/data/category-properties/effective congruences.yaml @@ -12,3 +12,4 @@ related_properties: - mono-regular - normal - quotients of congruences + - Barr-exact diff --git a/databases/catdat/data/category-properties/quotients of congruences.yaml b/databases/catdat/data/category-properties/quotients of congruences.yaml index c17dfa64..5308a5d8 100644 --- a/databases/catdat/data/category-properties/quotients of congruences.yaml +++ b/databases/catdat/data/category-properties/quotients of congruences.yaml @@ -10,3 +10,4 @@ related_properties: - cokernels - effective congruences - regular + - Barr-exact diff --git a/databases/catdat/data/category-properties/regular.yaml b/databases/catdat/data/category-properties/regular.yaml index 641a7517..ba26f045 100644 --- a/databases/catdat/data/category-properties/regular.yaml +++ b/databases/catdat/data/category-properties/regular.yaml @@ -8,3 +8,4 @@ invariant_under_equivalences: true related_properties: - finitely complete - quotients of congruences + - Barr-exact diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 5727343b..5adbeb58 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/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, diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 5e68abb2..1b231c2e 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/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, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index 1f714393..d3febb98 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/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 }