diff --git a/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql b/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql index c7ff080c..4b951d50 100644 --- a/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql +++ b/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql @@ -343,6 +343,38 @@ VALUES 'quotients of congruences', TRUE ), +( + 'effective congruences', + 'has', + 'A congruence $f, g : E \rightrightarrows X$ (see definition here) is effective if it is the kernel pair of some morphism, i.e. if there is a morphism $h : X \to Y$ such that we have a cartesian square + $$ + \begin{CD} + E @> f >> X \\ + @V g VV @V h VV \\ + X @> h >> Y. + \end{CD} + $$ + A category has effective congruences if every congruence in the category is effective.', + 'https://ncatlab.org/nlab/show/congruence', + 'effective cocongruences', + TRUE +), +( + 'effective cocongruences', + 'has', + 'A cocongruence $f, g : X \rightrightarrows E$ (see definition here) is effective if it is the cokernel pair of some morphism, i.e. if there is a morphism $h : Y \to X$ such that we have a cocartesian square + $$ + \begin{CD} + Y @> h >> X \\ + @V h VV @V f VV \\ + X @> g >> E. + \end{CD} + $$ + A category has effective cocongruences if every cocongruence in the category is effective.', + NULL, + 'effective congruences', + TRUE +), ( 'cosifted limits', 'has', diff --git a/databases/catdat/data/002_category-properties/100_related-category-properties.sql b/databases/catdat/data/002_category-properties/100_related-category-properties.sql index c1ac9d71..4e05b383 100644 --- a/databases/catdat/data/002_category-properties/100_related-category-properties.sql +++ b/databases/catdat/data/002_category-properties/100_related-category-properties.sql @@ -291,9 +291,17 @@ VALUES ('quotients of congruences', 'coequalizers'), ('quotients of congruences', 'cokernels'), ('quotients of congruences', 'regular'), +('quotients of congruences', 'effective congruences'), ('coquotients of cocongruences', 'equalizers'), ('coquotients of cocongruences', 'kernels'), ('coquotients of cocongruences', 'coregular'), +('coquotients of cocongruences', 'effective cocongruences'), +('effective congruences', 'normal'), +('effective congruences', 'quotients of congruences'), +('effective congruences', 'mono-regular'), +('effective cocongruences', 'conormal'), +('effective cocongruences', 'coquotients of cocongruences'), +('effective cocongruences', 'epi-regular'), ('direct', 'one-way'), ('direct', 'skeletal'), ('inverse', 'one-way'), @@ -339,13 +347,17 @@ VALUES ('cofiltered', 'finitely complete'), ('cofiltered', 'cofiltered limits'), ('mono-regular', 'normal'), +('mono-regular', 'effective congruences'), ('epi-regular', 'conormal'), +('epi-regular', 'effective cocongruences'), ('normal', 'zero morphisms'), ('normal', 'mono-regular'), ('normal', 'kernels'), +('normal', 'effective congruences'), ('conormal', 'zero morphisms'), ('conormal', 'epi-regular'), ('conormal', 'cokernels'), +('conormal', 'effective cocongruences'), ('multi-complete', 'complete'), ('multi-complete', 'multi-terminal object'), ('multi-terminal object', 'multi-complete'), diff --git a/databases/catdat/data/003_category-property-assignments/FinGrp.sql b/databases/catdat/data/003_category-property-assignments/FinGrp.sql index bf80a30b..35c11cd6 100644 --- a/databases/catdat/data/003_category-property-assignments/FinGrp.sql +++ b/databases/catdat/data/003_category-property-assignments/FinGrp.sql @@ -65,6 +65,12 @@ VALUES TRUE, 'The proof works exactly as for the category of finite sets.' ), +( + 'FinGrp', + 'effective congruences', + TRUE, + 'For a kernel pair $E$ of $h : X \to Z$ where $E$ and $X$ are finite groups, replacing $Z$ with the image of $h$ gives the same kernel pair.' +), ( 'FinGrp', 'normal', @@ -118,4 +124,4 @@ VALUES 'countable', FALSE, 'This is trivial.' -); \ No newline at end of file +); diff --git a/databases/catdat/data/003_category-property-assignments/FreeAb.sql b/databases/catdat/data/003_category-property-assignments/FreeAb.sql index 3be5d2a7..d8ba847c 100644 --- a/databases/catdat/data/003_category-property-assignments/FreeAb.sql +++ b/databases/catdat/data/003_category-property-assignments/FreeAb.sql @@ -61,6 +61,12 @@ VALUES (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\mathbf{Ab}$. Since $A \times_B A$ is free abelian, $f$ is also an coequalizer in $\mathbf{FreeAb}$.
(2) If $f : A \to B$ is a regular epimorphism in $\mathbf{FreeAb}$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective.' ), +( + 'FreeAb', + 'effective cocongruences', + TRUE, + 'Since $\mathbf{Ab}$ is abelian, it has effective cocongruences. Now, suppose a cocongruence $X \rightrightarrows E$ is the cokernel pair of $h : Z \to X$, where $X$ and $E$ are free abelian groups. If we find a surjective map $g : F \to Z$ where $F$ is a free abelian group, then $h \circ g$ has the same cokernel pair as $h$, and $h \circ g$ is a morphism in $\mathbf{FreeAb}$.' +), ( 'FreeAb', 'countable powers', @@ -84,4 +90,4 @@ VALUES 'sequential colimits', FALSE, 'See MO/509715.' -); \ No newline at end of file +); diff --git a/databases/catdat/data/003_category-property-assignments/Grp.sql b/databases/catdat/data/003_category-property-assignments/Grp.sql index 3f88bec9..1e0a8cbb 100644 --- a/databases/catdat/data/003_category-property-assignments/Grp.sql +++ b/databases/catdat/data/003_category-property-assignments/Grp.sql @@ -47,6 +47,12 @@ VALUES TRUE, 'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for groups.' ), +( + 'Grp', + 'effective cocongruences', + TRUE, + 'A proof can be found here.' +), ( 'Grp', 'normal', diff --git a/databases/catdat/data/003_category-property-assignments/Man.sql b/databases/catdat/data/003_category-property-assignments/Man.sql index 1fda6e42..2c974990 100644 --- a/databases/catdat/data/003_category-property-assignments/Man.sql +++ b/databases/catdat/data/003_category-property-assignments/Man.sql @@ -80,6 +80,12 @@ VALUES Because $r \circ (p \circ i_1) : X \to X$ is the identity, the image of $p \circ i_1$ is the equalizer of $\mathrm{id}_E$ and $(p \circ i_1) \circ r$, hence closed. Likewise, the image of $p \circ i_2$ is closed. Thus, the image of $p$, which is the union of these images, is closed.
Now, since the pushforward maps of tangent spaces compose to the identity, we see that $p$ must be a local immersion and $r$ must be a submersion. Also, since the fibers of $r$ have one or two points each, we see that the dimension of $E$ must locally be the same as the dimension of $X$. This implies that in fact $p$ and $r$ are local diffeomorphisms. Therefore, the cardinality of the fiber of $r$ is locally constant. Thus, if $U$ is the subset of $X$ where $r$ has fiber of a single point, with the subspace topology, then $U$ is a clopen submanifold of $X$ which serves as the equalizer of $p \circ i_1$ and $p \circ i_2$.' ), +( + 'Man', + 'effective cocongruences', + TRUE, + 'From the proof that $\mathbf{Man}$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows E$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : E \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $E$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.' +), ( 'Man', 'small', diff --git a/databases/catdat/data/003_category-property-assignments/Meas.sql b/databases/catdat/data/003_category-property-assignments/Meas.sql index 37c9e8f9..8331d58a 100644 --- a/databases/catdat/data/003_category-property-assignments/Meas.sql +++ b/databases/catdat/data/003_category-property-assignments/Meas.sql @@ -100,4 +100,10 @@ VALUES 'cofiltered-limit-stable epimorphisms', FALSE, 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Meas}$ which equips a set with the trivial $\sigma$-algebra.' +), +( + 'Meas', + 'effective cocongruences', + FALSE, + 'The proof is similar to the one for $\mathbf{Top}$: Use the trivial $\sigma$-algebra on a two-point space.' ); diff --git a/databases/catdat/data/003_category-property-assignments/Met.sql b/databases/catdat/data/003_category-property-assignments/Met.sql index 7f0cb1ce..06e14912 100644 --- a/databases/catdat/data/003_category-property-assignments/Met.sql +++ b/databases/catdat/data/003_category-property-assignments/Met.sql @@ -144,4 +144,10 @@ VALUES 'If $(N,z,s)$ is a natural numbers object in $\mathbf{Met}$, then $$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 +), +( + 'Met', + 'effective congruences', + FALSE, + 'Any kernel pair of $h : X \to Z$ in $\mathbf{Met}$ corresponds to a closed subset of $X\times X$. However, there are plenty of non-closed congruences, such as $\Delta \cup (\mathbb{Q} \times \mathbb{Q}) \subseteq \mathbb{R} \times \mathbb{R}$ with the subspace metric.' +); diff --git a/databases/catdat/data/003_category-property-assignments/PMet.sql b/databases/catdat/data/003_category-property-assignments/PMet.sql index b514daf8..d62762ac 100644 --- a/databases/catdat/data/003_category-property-assignments/PMet.sql +++ b/databases/catdat/data/003_category-property-assignments/PMet.sql @@ -138,4 +138,10 @@ VALUES 'If $(N,z,s)$ is a natural numbers object in $\mathbf{PMet}$, then $$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 pseudo-metric spaces does not exist, see MSE/1778408.' +), +( + 'PMet', + 'effective cocongruences', + FALSE, + 'The proof is similar to the one for $\mathbf{Top}$: Use the two-point space with the zero metric, which represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$.' ); diff --git a/databases/catdat/data/003_category-property-assignments/Prost.sql b/databases/catdat/data/003_category-property-assignments/Prost.sql index 4a2d9a52..9e0ebd2d 100644 --- a/databases/catdat/data/003_category-property-assignments/Prost.sql +++ b/databases/catdat/data/003_category-property-assignments/Prost.sql @@ -100,4 +100,10 @@ VALUES 'cofiltered-limit-stable epimorphisms', FALSE, 'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the functor $\mathbf{Set} \to \mathbf{Prost}$ that equips a set with the chaotic preorder.' +), +( + 'Prost', + 'effective cocongruences', + FALSE, + 'Consider the proset $E := \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a proset to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element proset with the trivial preorder.' ); diff --git a/databases/catdat/data/003_category-property-assignments/Rel.sql b/databases/catdat/data/003_category-property-assignments/Rel.sql index cf6e361d..1210ab25 100644 --- a/databases/catdat/data/003_category-property-assignments/Rel.sql +++ b/databases/catdat/data/003_category-property-assignments/Rel.sql @@ -71,6 +71,12 @@ VALUES TRUE, 'A proof can be found here.' ), +( + 'Rel', + 'effective congruences', + TRUE, + 'A proof can be found here.' +), ( 'Rel', 'preadditive', diff --git a/databases/catdat/data/003_category-property-assignments/Set_c.sql b/databases/catdat/data/003_category-property-assignments/Set_c.sql index bfe7298d..86b08391 100644 --- a/databases/catdat/data/003_category-property-assignments/Set_c.sql +++ b/databases/catdat/data/003_category-property-assignments/Set_c.sql @@ -77,6 +77,12 @@ VALUES TRUE, 'This is because $\{0,1\}$ is a subobject classifier in $\mathbf{Set}$, which is countable, and the monomorphisms coincide.' ), +( + 'Set_c', + 'effective congruences', + TRUE, + 'For a kernel pair $E$ of $h : X \to Z$ where $E$ and $X$ are countable, replacing $Z$ with the image of $h$ gives the same kernel pair.' +), ( 'Set_c', 'small', diff --git a/databases/catdat/data/003_category-property-assignments/Set_f.sql b/databases/catdat/data/003_category-property-assignments/Set_f.sql index e884cd5c..45407866 100644 --- a/databases/catdat/data/003_category-property-assignments/Set_f.sql +++ b/databases/catdat/data/003_category-property-assignments/Set_f.sql @@ -41,6 +41,18 @@ VALUES TRUE, 'A congruence on a set $X$ in $\mathbf{Set}_\mathrm{f}$ is the same as an equivalence relation $R$ on $X$ whose equivalence classes are finite. In that case, the usual quotient map $p : X \to X/R$ is finite-to-one. Moreover, if $h : X/R \to Y$ is a map such that $h \circ p : X \to Y$ is finite-to-one, then $h$ is finite-to-one as well because $h^*(\{y\}) \subseteq p^*((h \circ p)^*(\{y\}))$ for all $y \in Y$. Therefore, $p$ is also the quotient in $\mathbf{Set}_\mathrm{f}$.' ), +( + 'Set_f', + 'effective congruences', + TRUE, + 'If $E \rightrightarrows X$ is the kernel pair of $h : X \to Z$ in $\mathbf{Set}$ and both maps $E \to X$ are finite-to-one, then that means the equivalence classes of $E$ are finite. Thus, necessarily $h$ was finite-to-one also.' +), +( + 'Set_f', + 'effective cocongruences', + TRUE, + 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\mathbf{Set}_f$. Then it is a coreflexive corelation in $\mathbf{Set}$. Since $\mathbf{Set}$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$. If we replace $h$ with the inclusion map of its image, then this function is in $\mathbf{Set}_\mathrm{f}$ and gives the same cokernel pair.' +), ( 'Set_f', 'locally cartesian closed', @@ -132,4 +144,4 @@ VALUES FALSE, 'We will prove that the family of singleton sets $(1)_{n \in \mathbb{N}}$ has no multi-coproduct, generalizing the proof that the family does not have a coproduct given above. A cocone is just a map of sets $f : \mathbb{N} \to X$. A morphism from $f : \mathbb{N} \to X$ to $g : \mathbb{N} \to Y$ is a finite-to-one map $h : X \to Y$ with $g = h \circ f$. This describes the category of cocones, and we need to show that it has no multi-initial object. To this end, we claim that the connected component of the unique map $! : \mathbb{N} \to 1$ consists precisely of the maps $f : \mathbb{N} \to X$ with finite image. Once that is established, we can recycle the proof for missing coproducts since there we have only used finite codomains.
Let $g = h \circ f$ be as above. If $\mathrm{im}(f)$ is finite, then $\mathrm{im}(g) = h_*(\mathrm{im}(f))$ is finite as well. Conversely, if $\mathrm{im}(g)$ is finite, then $\mathrm{im}(f) \subseteq \bigcup_{y \in \mathrm{im}(g)} h^*(\{y\})$ is finite as well. This shows that the connected component of $!$ is contained in the collection of maps with finite image. Conversely, if $f$ has finite image, then there is a morphism from the corestriction $f'' : \mathbb{N} \to \mathrm{im}(f)$ to $f$, and also a morphism from $f''$ to $!$. This proves the remaining inclusion.' -); \ No newline at end of file +); diff --git a/databases/catdat/data/003_category-property-assignments/Set_pointed.sql b/databases/catdat/data/003_category-property-assignments/Set_pointed.sql index 15bec3c1..d5dba878 100644 --- a/databases/catdat/data/003_category-property-assignments/Set_pointed.sql +++ b/databases/catdat/data/003_category-property-assignments/Set_pointed.sql @@ -67,6 +67,13 @@ VALUES TRUE, '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.' ), +( + -- TODO: rework this when Barr-exact is added + 'Set*', + 'effective cocongruences', + TRUE, + 'We have that $\mathbf{Set}_*^{\mathrm{op}}$ is a slice category of $\mathbf{Set}^{\mathrm{op}}$, which in turn is monadic over $\mathbf{Set}$. Therefore, by combining results from Borceux and Bourn Appendix A and nLab, $\mathbf{Set}_*^{\mathrm{op}}$ is Barr-exact, and in particular it has effective congruences.' +), ( 'Set*', 'skeletal', diff --git a/databases/catdat/data/003_category-property-assignments/Setne.sql b/databases/catdat/data/003_category-property-assignments/Setne.sql index 6a4954f2..e348cb10 100644 --- a/databases/catdat/data/003_category-property-assignments/Setne.sql +++ b/databases/catdat/data/003_category-property-assignments/Setne.sql @@ -114,6 +114,12 @@ VALUES TRUE, 'This follows from this lemma applied to the forgetful functor to $\mathbf{Set}$.' ), +( + 'Setne', + 'effective congruences', + TRUE, + 'If a congruence $E \rightrightarrows X$ is the kernel pair of $h : X \to Z$, with both $E$ and $X$ non-empty, then certainly $Z$ must also be non-empty.' +), ( 'Setne', 'sequential limits', @@ -137,4 +143,11 @@ VALUES 'coquotients of cocongruences', FALSE, 'The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but they do not have an equalizer.' -) +), +( + 'Setne', + 'effective cocongruences', + FALSE, + 'The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square.' +); + diff --git a/databases/catdat/data/003_category-property-assignments/SetxSet.sql b/databases/catdat/data/003_category-property-assignments/SetxSet.sql index 78eb6657..56871c7c 100644 --- a/databases/catdat/data/003_category-property-assignments/SetxSet.sql +++ b/databases/catdat/data/003_category-property-assignments/SetxSet.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'Take the two-sorted algebraic theory with no operations and no equations.' ), +( + 'SetxSet', + 'effective cocongruences', + TRUE, + 'Suppose we have a cocongruence $X \rightrightarrows E$ in $\mathbf{Set} \times \mathbf{Set}$. Then each component is a cocongruence, so they are the kernel pairs of some maps $Z_1\to X_1$, $Z_2 \to X_2$. Then $E$ is the cokernel pair of $(Z_1, Z_2) \to (X_1, X_2)$.' +), ( 'SetxSet', 'skeletal', diff --git a/databases/catdat/data/003_category-property-assignments/Top.sql b/databases/catdat/data/003_category-property-assignments/Top.sql index dcd4464d..65beca91 100644 --- a/databases/catdat/data/003_category-property-assignments/Top.sql +++ b/databases/catdat/data/003_category-property-assignments/Top.sql @@ -130,4 +130,10 @@ VALUES 'cofiltered-limit-stable epimorphisms', FALSE, 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Top}$ which equips a set with the indiscrete topology.' +), +( + 'Top', + 'effective cocongruences', + FALSE, + 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' ); diff --git a/databases/catdat/data/003_category-property-assignments/Top_pointed.sql b/databases/catdat/data/003_category-property-assignments/Top_pointed.sql index 96599580..f4802d6a 100644 --- a/databases/catdat/data/003_category-property-assignments/Top_pointed.sql +++ b/databases/catdat/data/003_category-property-assignments/Top_pointed.sql @@ -168,7 +168,16 @@ VALUES 'cofiltered-limit-stable epimorphisms', FALSE, 'We already know that $\mathbf{Set}_*$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set}_* \to \mathbf{Top}_*$ that equips a pointed set with the indiscrete topology.' +), +( + 'Top*', + 'effective congruences', + FALSE, + 'Suppose that $\mathbf{Top}_*$ had effective congruences. Then for any congruence $E \rightrightarrows X$ in $\mathbf{Top}$, we can expand it to a congruence $E + \{*\} \rightrightarrows X + \{*\}$ in $\mathbf{Top}_*$. If $E + \{*\}$ is the kernel pair of $h : X + \{*\} \to Z$, then $E$ is the kernel pair of $h$ restricted to $X$. This contradicts the fact that $\mathbf{Top}$ does not have effective congruences.' +), +( + 'Top*', + 'effective cocongruences', + FALSE, + 'Consider the pointed topological space $I := \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are the two possible pointed functions. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $Z$ must be the singleton pointed space. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' ); - - - diff --git a/databases/catdat/data/003_category-property-assignments/Z.sql b/databases/catdat/data/003_category-property-assignments/Z.sql index dedd72fb..2d3ef0ba 100644 --- a/databases/catdat/data/003_category-property-assignments/Z.sql +++ b/databases/catdat/data/003_category-property-assignments/Z.sql @@ -53,6 +53,18 @@ VALUES TRUE, 'This follows immediately from the fact for $\mathbf{Set}$.' ), +( + 'Z', + 'effective congruences', + TRUE, + 'If we have a congruence $E \rightrightarrows X$ in $[\mathbf{CRing}, \mathbf{Set}]$, then each image at a commutative ring gives a congruence in $\mathbf{Set}$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$ whose kernel pair is $E$.' +), +( + 'Z', + 'effective cocongruences', + TRUE, + 'If we have a congruence $X\rightrightarrows E$ in $[\mathbf{CRing}, \mathbf{Set}]$, then each image at a commutative ring gives a cocongruence in $\mathbf{Set}$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$ whose cokernel pair is $E$.' +), ( 'Z', 'locally essentially small', @@ -100,4 +112,4 @@ VALUES 'cofiltered-limit-stable epimorphisms', FALSE, 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to [\mathbf{CRing}, \mathbf{Set}]$ that maps a set to its constant functor.' -); \ No newline at end of file +); diff --git a/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql b/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql index d54a854e..83b6b65a 100644 --- a/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql +++ b/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql @@ -37,8 +37,8 @@ VALUES ( 'reflexive_pair_trivial', '["left cancellative"]', - '["reflexive coequalizers", "coreflexive equalizers"]', - 'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.', + '["reflexive coequalizers", "coreflexive equalizers", "effective congruences", "effective cocongruences"]', + 'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of the identity morphism on the target, and the cokernel pair of the identity morphism on the source.', FALSE ), ( @@ -178,8 +178,8 @@ VALUES ( 'core-hin_quotients', '["core-thin"]', - '["quotients of congruences"]', - 'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\mathrm{id}_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\mathrm{id}_X$ is a coequalizer.', + '["quotients of congruences", "effective congruences"]', + 'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\mathrm{id}_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\mathrm{id}_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \mathrm{id}$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \mathrm{id}$ and $p_2 \circ r \circ p_1 = p_2 \circ \mathrm{id}$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \mathrm{id}$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\mathrm{id}_X$.', FALSE ), ( @@ -188,4 +188,4 @@ VALUES '["skeletal", "core-thin"]', 'This is trivial.', TRUE -); \ No newline at end of file +); diff --git a/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql b/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql index 24b71cdb..278436ba 100644 --- a/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql +++ b/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql @@ -27,6 +27,15 @@ VALUES 'This is trivial.', FALSE ), +( + 'preadditive_kernels_normal_imply_effective_congruences', + '["preadditive", "kernels", "normal"]', + '["effective congruences"]', + 'Let $f, g : E \rightrightarrows X$ be a congruence. Then let $E_0$ be the kernel of $g$. We see that $f$ restricted to $E_0$ is a monomorphism $E_0 \hookrightarrow X$. Let $f |_{E_0}$ be the kernel of a morphism $h : X \to Y$. We claim that $E$ is also the kernel pair of $h$.
+ To see this, suppose we have a pair of generalized elements $x_1, x_2 : T \rightrightarrows X$. Then the pair $x_1, x_2$ factors through $E$ if and only if $x_1 - x_2, 0$ does. This is equivalent to the condition that $x_1 - x_2$ factors through $E_0$. That in turn is equivalent to $h \circ (x_1 - x_2) = 0$, which is equivalent to $h \circ x_1 = h \circ x_2$.
+ In particular, applying the forward implications in the case $T := E, x_1 := f, x_2 := g$, we conclude that $h \circ f = h \circ g$, so we get the required commutative diagram. From there, the reverse implications show this diagram is a cartesian square.', + FALSE +), ( 'additive_definition', '["additive"]', @@ -110,4 +119,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/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql b/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql index e9555508..b801b7bc 100644 --- a/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql +++ b/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql @@ -223,10 +223,17 @@ VALUES 'This follows from one of equivalent formulations of multi-algebraic categories.', TRUE ), +( + 'multi-algebraic_implies_effective_congruences', + '["multi-algebraic"]', + '["effective congruences"]', + 'This is Thm. 4.0 in Yves Diers, Catégories Multialgébriques or its English translation.', + FALSE +), ( 'locally-finitely-multi-presentable_stable-monos', '["locally finitely multi-presentable"]', '["filtered-colimit-stable monomorphisms"]', 'Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (Adamek-Rosicky, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (Adamek-Rosicky, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.', FALSE -); \ No newline at end of file +); diff --git a/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql b/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql index 745b4f9b..0159f2ff 100644 --- a/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql +++ b/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql @@ -121,8 +121,8 @@ VALUES ( 'topos_consequence', '["elementary topos"]', - '["finitely cocomplete", "disjoint finite coproducts", "epi-regular"]', - 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8.', + '["finitely cocomplete", "disjoint finite coproducts", "epi-regular", "effective congruences"]', + 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8; and Johnstone, Part A, Proposition 2.4.1.', FALSE ), ( @@ -167,6 +167,29 @@ VALUES 'This is proven in Johnstone, A2.6.3 (for every quasitopos).', FALSE ), +( + 'regular_effective_congruences_implies_quotients', + '["regular", "effective congruences"]', + '["quotients of congruences"]', + 'We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient.', + FALSE +), +( + 'regular_epiregular_extensive_consequences', + '["regular", "epi-regular", "extensive"]', + '["effective cocongruences", "co-Malcev"]', + 'Suppose we have a coreflexive corelation on $X$, $X+X \overset{p}{\twoheadrightarrow} E \overset{r}{\twoheadrightarrow} X$. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \to E$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer of $p\circ p_1, p\circ p_2 : (X+X) \times (X+X) \to E$. By distributivity and extensitivity, it is sufficient to calculate the equalizer on each quadrant of $(X+X) \times (X+X)$. On the $(1,1)$ quadrant, this is the equalizer of $p\circ i_1\circ p_1, p\circ i_1\circ p_2$, which is isomorphic to $X$ since $p\circ i_1$ is a split monomorphism. On the $(1,2)$ quadrant, it is the equalizer of $p\circ i_1\circ p_1, p\circ i_2\circ p_2$. Since $r$ is a common section of $p\circ i_1$ and $p\circ i_2$, any generalized element of this equalizer has equal components; thus, the equalizer is isomorphic to the equalizer $Y$ of $p\circ i_1, p\circ i_2$. Similarly, on the $(2,1)$ quadrant, it is isomorphic to $Y$, and on the $(2,2)$ quadrant, it is isomorphic to $X$.
+ + Since the $X$ pieces are already equalized by the kernel pair of $p$, and the second $Y$ piece is redundant, we thus get that $p$ is the coequalizer of $i_1 \circ \mathrm{inc}_Y$ and $i_2 \circ \mathrm{inc}_Y$, which is equivalent to the cokernel pair of $\mathrm{inc}_Y$ and thus an effective cocongruence.', + FALSE +), +( + 'pretopos_balanced', + '["effective congruences", "extensive"]', + '["balanced"]', + 'Let $i : Y \to X$ be both a monomorphism and an epimorphism. Now define a congruence $f, g : X + Y + Y + X \rightrightarrows X+X$ acting as $i_1,i_1$ on the first copy of $X$; $i_1\circ i, i_2\circ i$ on the first copy of $Y$; $i_2\circ i, i_1\circ i$ on the second copy of $Y$; and $i_2\circ i_2$ on the second copy of $X$. We use extensitivity in showing that $f, g$ are jointly monomorphic, and again in proving transitivity. Now suppose this is the kernel pair of a morphism $h : X \to Z$. Then consider the map pair $i_2, i_1 : X \to X+X$. We must have $h \circ i_2 \circ i = h \circ i_1 \circ i$ since the pair of maps $i_2\circ i, i_1\circ i$ factor through $E$. Since $i$ is an epimorphism, that implies $h\circ i_2 = h\circ i_1$, so $i_2, i_1$ factor through $E$ as well. By disjointness of coproducts, we can conclude that $i_2, i_1$ factor uniquely through the second copy of $Y$. We thus get a morphism $X \to Y$ which is a left inverse of $i$, showing that $i$ must in fact be an isomorphism.', + FALSE +), ( 'lcc_implies_extensive', '["locally cartesian closed", "disjoint finite coproducts"]', @@ -222,4 +245,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/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index b511fc1b..efca47d0 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -104,6 +104,8 @@ "filtered-colimit-stable monomorphisms": true, "quotients of congruences": true, "coquotients of cocongruences": true, + "effective congruences": true, + "effective cocongruences": 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 44db92c4..6b976962 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -99,6 +99,8 @@ "filtered-colimit-stable monomorphisms": true, "quotients of congruences": true, "coquotients of cocongruences": true, + "effective congruences": true, + "effective cocongruences": 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 e70a439c..c95e68aa 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/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, + "effective congruences": false, + "effective cocongruences": false } diff --git a/static/pdf/.gitignore b/static/pdf/.gitignore new file mode 100644 index 00000000..372e1325 --- /dev/null +++ b/static/pdf/.gitignore @@ -0,0 +1,7 @@ +# Files from Latex Workshop +*.aux +*.fdb_latexmk +*.fls +*.log +*.synctex.gz +*.out \ No newline at end of file diff --git a/static/pdf/cocongruences_of_groups.pdf b/static/pdf/cocongruences_of_groups.pdf new file mode 100644 index 00000000..f5bdf0b6 Binary files /dev/null and b/static/pdf/cocongruences_of_groups.pdf differ diff --git a/static/pdf/cocongruences_of_groups.tex b/static/pdf/cocongruences_of_groups.tex new file mode 100644 index 00000000..c6957f45 --- /dev/null +++ b/static/pdf/cocongruences_of_groups.tex @@ -0,0 +1,108 @@ +\documentclass[a4paper,12pt,reqno]{amsart} +\usepackage[utf8]{inputenc} +\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry} +\usepackage{parskip} +\usepackage{tikz-cd} + +\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools} +\usepackage{hyperref} + +\theoremstyle{plain} +\newtheorem{prop}{Proposition} +\newtheorem{cor}[prop]{Corollary} + +\theoremstyle{definition} +\newtheorem{defi}[prop]{Definition} + +\DeclareMathOperator{\id}{id} +\DeclareMathOperator{\eq}{eq} +\DeclareMathOperator{\Grp}{\mathbf{Grp}} + +\newcommand{\C}{\mathcal{C}} + +\title{Cocongruences on groups are effective} +\author{Martin Brandenburg} +\date{\today} + +\begin{document} +\maketitle + +Our goal is to prove that every cocongruence in the category $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way. + +\begin{defi} +We shall say that a category $\C$ has \emph{good pushouts of monomorphisms} if it has pushouts of monomorphisms and if, for every diagram of monomorphisms +\[\begin{tikzcd} +B \ar{r} & B' \\ +A \ar{r} \ar{u} \ar{d} & A' \ar{u} \ar{d} \\ +C \ar{r} & C' +\end{tikzcd}\] +in which each square is a pullback, the induced morphism +\[B \sqcup_A C \to B' \sqcup_{A'} C'\] +is also a monomorphism. +\end{defi} + +\begin{prop} +The category $\Grp$ has good pushouts of monomorphisms. +\end{prop} + +\begin{proof} +Consider a diagram as above. We regard every monomorphism in it as an inclusion. Choose a system of representatives $S \subseteq B$ for the right $A$-cosets in $B$, meaning that the multiplication map $\cdot : A \times S \to B$ is bijective. Likewise, choose $T \subseteq C$ such that the multiplication map $\cdot : A \times T \to C$ is bijective. We may assume that $1 \in S$ and $1 \in T$. + +It is well known (see, for example, Serre's book \emph{Trees}, Ch.\ I, §1, Thm.\ 1) that every element of the amalgamated free product $B \sqcup_A C$ has a unique representation of the form +\[w = a \cdot x_1 \cdots x_n,\] +where $a \in A$, each $x_i$ lies either in $S \setminus \{1\}$ or in $T \setminus \{1\}$, and these choices alternate. + +The map +\[A \backslash B \to A' \backslash B', \, Ab \mapsto A'b\] +is injective. Indeed, if $b_1,b_2 \in B$ satisfy $A' b_1 = A' b_2$, then $b_1 b_2^{-1} \in A'$. Since $B \cap A' = A$, it follows that $b_1 b_2^{-1} \in A$, and hence $A b_1 = A b_2$. + +Therefore, we may extend $S$ to a system of representatives $S' \subseteq B'$ for the right $A'$-cosets in $B'$. Likewise, we may extend $T$ to a system of representatives $T' \subseteq C'$ for the right $A'$-cosets in $C'$. + +With respect to these systems, an element $w \in B \sqcup_A C$ written in normal form as above remains in normal form after being mapped to $B' \sqcup_{A'} C'$. This shows that the induced map is injective. +\end{proof} + +\begin{prop} +Let $\C$ be a balanced category with good pushouts of monomorphisms and equalizers of monomorphisms. Then every cocongruence in $\C$ is effective. +\end{prop} + +\begin{proof} +Let $X \in \C$ be an object, and let $i_1,i_2 : X \rightrightarrows Y$ be a cocongruence. Since it is coreflexive, there exists a morphism $r : Y \to X$ satisfying +\[r \circ i_1 = \id_X, \quad r \circ i_2 = \id_X.\] +In particular, $i_1$ and $i_2$ are monomorphisms. Since the cocongruence is cotransitive, there exists a morphism +\[c : Y \to Y \sqcup_{i_2,X,i_1} Y\] +satisfying +\[c \circ i_1 = u_1 \circ i_1, \quad c \circ i_2 = u_2 \circ i_2,\] +where $u_1,u_2 : Y \rightrightarrows Y \sqcup_{i_2,X,i_1} Y$ are the pushout inclusions satisfying $u_1 i_2 = u_2 i_1$. We will not use the fact that the cocongruence is cosymmetric; this will follow automatically. Define the monomorphism +\[E := \eq(i_1,i_2) \hookrightarrow X.\] + +Since $i_1$ and $i_2$ agree on $E$, there exists a unique morphism +\[\varphi : X \sqcup_E X \to Y\] +defined by $\varphi \circ j_1 = i_1$ and $\varphi \circ j_2 = i_2$, where $j_1,j_2 : X \rightrightarrows X \sqcup_E X$ are the two inclusions. + +We must show that $\varphi$ is an isomorphism. It is clearly an epimorphism, since $i_1$ and $i_2$ are jointly epimorphic by assumption. Since $\C$ is balanced, it therefore suffices to prove that $\varphi$ is a monomorphism. + +We will show that even the morphism +\[\gamma := c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y\] +is a monomorphism. It is characterized by +\[\gamma \circ j_1 = c \circ \varphi \circ j_1 = c \circ i_1 = u_1 \circ i_1,\] +\[\gamma \circ j_2 = c \circ \varphi \circ j_2 = c \circ i_2 = u_2 \circ i_2.\] + +In other words, $\gamma$ is induced by the diagram of monomorphisms +\[\begin{tikzcd} +X \ar{r}{i_1} & Y \\ +E \ar{r} \ar{u} \ar{d} & X \ar{u}[swap]{i_2} \ar{d}{i_1} \\ +X \ar{r}[swap]{i_2} & Y +\end{tikzcd}\] + +Since $\C$ has good pushouts of monomorphisms, it suffices to verify that both squares are pullbacks. Observe that the two squares are symmetric, so it is enough to consider one of them. To verify the universal property, let $a : T \to X$ and $b : T \to X$ be morphisms satisfying $i_1 \circ a = i_2 \circ b$. Applying $r : Y \to X$, we obtain +\[a = r \circ i_1 \circ a = r \circ i_2 \circ b = b.\] + +Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquely through $E \hookrightarrow X$. +\end{proof} + +\begin{cor} +Every cocongruence in the category $\Grp$ is effective. +\end{cor} + + +\end{document}