$1 \xrightarrow{z} N \xleftarrow{s} N$
is a coproduct cocone by Johnstone, 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 MSE/1778408.' -); \ No newline at end of file +); diff --git a/database/data/004_property-assignments/Met_c.sql b/database/data/004_property-assignments/Met_c.sql index 2dd5084b..e76f3f9d 100644 --- a/database/data/004_property-assignments/Met_c.sql +++ b/database/data/004_property-assignments/Met_c.sql @@ -100,4 +100,10 @@ VALUES 'sequential colimits', FALSE, 'See MO/510316.' +), +( + '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}$.' ); diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index 79cd4b3d..632f727b 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -82,4 +82,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509552: 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}$.' ); diff --git a/database/data/004_property-assignments/Prost.sql b/database/data/004_property-assignments/Prost.sql index 3b0a67b5..91411889 100644 --- a/database/data/004_property-assignments/Prost.sql +++ b/database/data/004_property-assignments/Prost.sql @@ -94,4 +94,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509552: 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.' ); diff --git a/database/data/004_property-assignments/Set.sql b/database/data/004_property-assignments/Set.sql index 8e266208..b04f6277 100644 --- a/database/data/004_property-assignments/Set.sql +++ b/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.' ); diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql index a0719751..4d04aec6 100644 --- a/database/data/004_property-assignments/Set_pointed.sql +++ b/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 category of sets and the observation that the forgetful functor $\mathbf{Set}_* \to \mathbf{Set}$ preserves pushouts.' + 'According to nLab with a citation to Borceux and Bourn, 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*', diff --git a/database/data/004_property-assignments/SetxSet.sql b/database/data/004_property-assignments/SetxSet.sql index d5c9beac..2fbdfa3d 100644 --- a/database/data/004_property-assignments/SetxSet.sql +++ b/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', diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index 7b8cbdf8..3a694749 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/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 Adamek-Rosicky. 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.' ); diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index fa4e679d..034a2064 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/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 Adamek-Rosicky. 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.' ); - - - diff --git a/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql index 26cc5805..619f5dac 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/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 this proof.', FALSE -); \ No newline at end of file +); diff --git a/database/data/005_implications/005_additional-structure-implications.sql b/database/data/005_implications/005_additional-structure-implications.sql index 97962495..f65b08cf 100644 --- a/database/data/005_implications/005_additional-structure-implications.sql +++ b/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 here. 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 Mac Lane, Ch. VIII.', + '["Barr-exact"]', + 'In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see Mac Lane, 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, Abelian categories, p. 116.', FALSE -); \ No newline at end of file +); diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index 6ad51eb0..2008453a 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/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 -); \ No newline at end of file +); diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 60bf7679..3ba0c906 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -41,6 +41,20 @@ 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 NLab, Example 2.2 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"]', @@ -48,6 +62,13 @@ VALUES '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 -); \ No newline at end of file +); diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 97ebd8eb..48224d80 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -100,6 +100,9 @@ "multi-initial object": true, "cartesian filtered colimits": true, "cocartesian cofiltered limits": true, + "Barr-coexact": true, + "Barr-exact": true, + "monadically concrete": true, "cartesian closed": false, "locally cartesian closed": false, @@ -144,5 +147,6 @@ "essentially countable": false, "natural numbers object": false, "countably distributive": false, - "countably codistributive": false + "countably codistributive": false, + "pretopos": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 00206fe0..ac1d08f0 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -96,6 +96,10 @@ "cocartesian cofiltered limits": true, "natural numbers object": true, "countably distributive": true, + "Barr-coexact": true, + "Barr-exact": true, + "monadically concrete": true, + "pretopos": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0e6ea903..f9600169 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -144,5 +144,9 @@ "countable": false, "essentially countable": false, "cartesian filtered colimits": false, - "countably codistributive": false + "countably codistributive": false, + "Barr-coexact": false, + "Barr-exact": false, + "monadically concrete": false, + "pretopos": false }