diff --git a/.claude/skills/check-proofs/SKILL.md b/.claude/skills/check-proofs/SKILL.md index ba0249ede..339b0139a 100644 --- a/.claude/skills/check-proofs/SKILL.md +++ b/.claude/skills/check-proofs/SKILL.md @@ -30,6 +30,7 @@ All other argument text is additional context; consider it without narrowing the 4. Use relevant repository context when a proof depends on a local definition or referenced CatDat entry. Keep the assessment grounded in available sources; flag context that cannot be checked. - Prefer reading a known source file directly, especially when a CatDat link or entry ID identifies it. For content links, check the matching Markdown file under `content/`; for data entries, locate the YAML source under the appropriate `database/data/` directory (use Glob with the entry's ID as filename). Do not rely on generated files under `build/`. - When the path is unknown, Grep only the relevant source directory (`content/` or `database/data/`) for one short, distinctive plain-text term or the entry's ID. Avoid long LaTeX expressions, complex regular expressions, and queries combining many alternatives. + - Use the size notions (small, essentially small, locally small, ...) as defined in `content/foundations.md`. In particular, an essentially small _collection_ (such as a (co)generating collection) is one that is isomorphic to a set; do not confuse it with an essentially small _category_, which is equivalent to a small category. - Treat a search with no matches as inconclusive, not as evidence that the reference is absent. Check the intended source path, then retry with a simpler term or exact filename. Only report that context is unavailable after these checks fail. 5. This is a read-only review. Do not edit files, apply fixes, or invoke database update workflows. Do not propose rewritten proofs unless the user separately asks. diff --git a/content/Grp_total_explicit_proof.md b/content/Grp_total_explicit_proof.md index 1d8aedf4d..110c8f14f 100644 --- a/content/Grp_total_explicit_proof.md +++ b/content/Grp_total_explicit_proof.md @@ -7,39 +7,41 @@ description: An explicit construction of the left adjoint to the covariant Yoned The definition of a [total](/category-property/total) category is very abstract; furthermore, it is not immediately clear how it is possible for _any_ category which is not essentially small to satisfy the definition, much less a wide variety of the algebraic and topological categories which are considered in practice. Thus, to illustrate the definition, we give an explicit construction of the functor $$L : [\Grp^{\op},\Set] \to \Grp$$ -that is left adjoint to the Yoneda embedding $y : \Grp \hookrightarrow [\Grp^{\op},\Set]$. +that is left adjoint to the Yoneda embedding $y : \Grp \hookrightarrow [\Grp^{\op},\Set]$ and therefore witnesses that $\Grp$ is total. Fix a functor $T : \Grp^{\op} \to \Set$. To construct the group $L(T)$, we will make use of the usual cogroup structure on $\IZ$ in $\Grp$, which includes - the comultiplication homomorphism $\mu : \IZ \to \IZ * \IZ'$, $1 \mapsto 1 \cdot 1'$ (where $\IZ'$ denotes a copy of $\IZ$), - the coidentity homomorphism $\varepsilon : \IZ \to 0$, -- the coinverse homomorphism $\iota : \IZ \to \IZ$. +- the coinverse homomorphism $\sigma : \IZ \to \IZ$. -Also, let $i_1,i_2 : \IZ \rightrightarrows \IZ * \IZ'$ denote the coprojections. We define the group $L(T)$ as the group generated by elements $e(x)$, one for each element $x \in T(\IZ)$, subject to the following relations: +Also, let $\iota_1, \iota_2 : \IZ \rightrightarrows \IZ * \IZ'$ denote the coprojections. We define the group $L(T)$ as the group generated by elements $e(x)$, one for each element $x \in T(\IZ)$, subject to the following relations: -- $e(T\mu(x)) = e(Ti_1(x)) \cdot e(Ti_2(x))$ for each $x \in T(\IZ * \IZ')$, -- $e(T\varepsilon(x)) = 1$ for each $x \in T0$, -- $e(T\iota(x)) = e(x)^{-1}$ for each $x \in T\IZ$. +- $e(T(\mu)(x)) = e(T(\iota_1)(x)) \cdot e(T(\iota_2)(x))$ for each $x \in T(\IZ * \IZ')$, +- $e(T(\varepsilon)(x)) = 1$ for each $x \in T(0)$, +- $e(T(\sigma)(x)) = e(x)^{-1}$ for each $x \in T(\IZ)$. -We first need to define a natural transformation $\eta_T : T \to \Hom({-}, L(T))$. For each group $H$ we define the function $\eta_T(H) : TH \to \Hom(H, L(T))$ by sending $x \in TH$ to $h \mapsto e(Th(x))$, where we abuse notation to identify $h \in H$ with the corresponding morphism $\IZ \to H$ mapping $1 \mapsto h$, so that $Th : TH \to T\IZ$. To see that this defines a group homomorphism from $H$ to $L(T)$, note that for $h, h' \in H$ we have three commutative diagrams of the form +We first need to define a natural transformation +$$\eta_T : T \to \Hom({-}, L(T)).$$ +For each group $H$ we define the function $\eta_T(H) : T(H) \to \Hom(H, L(T))$ by sending $x \in T(H)$ to the map +$$H \to L(T), \quad h \mapsto e(T(\widetilde{h})(x)),$$ +where $\widetilde{h} : \IZ \to H$ denotes the homomorphism mapping $1 \mapsto h$, so that $T(\widetilde{h}) : T(H) \to T(\IZ)$. To see that this defines a group homomorphism from $H$ to $L(T)$, for $h,h' \in H$ we define the homomorphism $[h,h'] : \IZ * \IZ' \to H$ by $[h,h'] \circ \iota_1 = \widetilde{h}$ and $[h,h'] \circ \iota_2 = \widetilde{h'}$. Note that $[h,h'] \circ \mu = \widetilde{hh'}$. Hence, $$ -\begin{CD} -T(H) @> = >> T(H)\\ -@V T(hh') VV @VVV\\ -T(\IZ * \IZ') @>>> T(\IZ) -\end{CD} +\begin{align*} +e(T(\widetilde{hh'})(x)) &= e(T(\mu)(T([h,h'])(x))) \\ +& = e(T(\iota_1)(T([h,h'])(x))) \cdot e(T(\iota_2)(T([h,h'])(x))) \\ +& = e(T(\widetilde{h})(x)) \cdot e(T(\widetilde{h'})(x)), +\end{align*} $$ -where on the bottom we use $T\mu, Ti_1, Ti_2$, and on the right we use $h h', h, h'$. Applying this to $x\in TH$, we get $T(h h')(x)$, $Th(x)$, and $Th'(x)$, respectively. Thus, the relation $e(T\mu(y)) = e(Ti_1(y)) \cdot e(Ti_2(y))$ with $y \coloneqq T(h h')(x)$ implies -$$e(T(hh')(x)) = e(Th(x)) \cdot e(Th'(x)),$$ -as required. Similar proofs show that the map $H \to L(T)$ respects inverses and the identity. We leave it as an exercise for the reader to show this is natural in $H$. +as required. Similar proofs show that the map $H \to L(T)$ respects inverses and the identity. We leave it as an exercise to verify that $\eta_T(H)$ is natural in $H$. We now need to show that for each group $G$ and natural transformation $\alpha : T \to y_G$, there exists a unique group homomorphism $\varphi : L(T) \to G$ such that $$\alpha = y_{\varphi} \circ \eta_T : T \to \Hom({-}, L(T)) \to \Hom({-}, G).$$ -We start with uniqueness: suppose $x \in T\IZ$. Then by hypothesis, -$$\alpha_{\IZ} = (y_{\varphi})_{\IZ} \circ (\eta_T)_{\IZ} : T\IZ \to \Hom(\IZ, L(T)) \to \Hom(\IZ, G).$$ -For each $x \in T\IZ$, the first step on the right-hand side maps $x \mapsto (1 \mapsto e(x))$, and the second step then maps this to $1 \mapsto \varphi(e(x))$. Therefore, +We start with uniqueness: suppose that $\varphi$ is such a homomorphism. Then, in particular, +$$\alpha_{\IZ} = (y_{\varphi})_{\IZ} \circ (\eta_T)_{\IZ} : T(\IZ) \to \Hom(\IZ, L(T)) \to \Hom(\IZ, G).$$ +For each $x \in T(\IZ)$, the first step on the right-hand side maps $x \mapsto (1 \mapsto e(x))$, and the second step then maps this to $1 \mapsto \varphi(e(x))$. Therefore, $$\varphi(e(x)) = \alpha_{\IZ}(x)(1)$$ for each $x$, which establishes the uniqueness of $\varphi$. @@ -47,22 +49,22 @@ For the existence part, the first step is to show there is a group homomorphism $$ \begin{CD} -T(\IZ * \IZ') @> \alpha_{\IZ * \IZ'} >> \Hom(\IZ * \IZ', G) @> \simeq >> UG \times UG\\ +T(\IZ * \IZ') @> \alpha_{\IZ * \IZ'} >> \Hom(\IZ * \IZ', G) @> \simeq >> U(G) \times U(G)\\ @VVV @VVV @VVV\\ -T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G) @> \simeq >> UG +T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G) @> \simeq >> U(G) \end{CD} $$ -applying naturality to $\mu, i_1, i_2 : \IZ \to \IZ * \IZ'$. On the right-hand side, we get multiplication, first projection, and second projection, respectively. From this, we conclude that the images of $e(T\mu(x))$ and $e(Ti_1(x)) \cdot e(Ti_2(x))$ in $UG$ agree for any element $x \in T(\IZ * \IZ')$. Similar proofs show that the other relations are also satisfied. +by applying naturality to $\mu, \iota_1, \iota_2 : \IZ \to \IZ * \IZ'$, where $U : \Grp \to \Set$ denotes the forgetful functor. On the right-hand side, we get multiplication, first projection, and second projection, respectively. From this, we conclude that the images of $e(T(\mu)(x))$ and $e(T(\iota_1)(x)) \cdot e(T(\iota_2)(x))$ in $U(G)$ agree for any element $x \in T(\IZ * \IZ')$. Similar proofs show that the other relations are also satisfied. -Finally, we need to show $\alpha = y_{\varphi} \circ \eta_T$, i.e. $\alpha_H = (y_{\varphi})_H \circ (\eta_T)_H$ for each group $H$. By definition, for each $x \in TH$, the first step gives the homomorphism $h \mapsto e(Th(x))$; then the second step is formed by composition with $\varphi$. By the specification of $\varphi$, this gives the homomorphism $h \mapsto \alpha_{\IZ}(Th(x))(1)$. However, by the assumption that $\alpha$ is a natural transformation, for each $h \in H$ we have a commutative diagram +Finally, we need to show $\alpha = y_{\varphi} \circ \eta_T$, i.e. $\alpha_H = (y_{\varphi})_H \circ (\eta_T)_H$ for each group $H$. By definition, for each $x \in T(H)$, the first step gives the homomorphism $h \mapsto e(T(\widetilde{h})(x))$; then the second step is formed by composition with $\varphi$. By the specification of $\varphi$, this gives the homomorphism $h \mapsto \alpha_{\IZ}(T(\widetilde{h})(x))(1)$. However, by the assumption that $\alpha$ is a natural transformation, for each $h \in H$ we have a commutative diagram $$ \begin{CD} -TH @> \alpha_H >> \Hom(H, G) \\ -@V Th VV @VV {-} \circ h V \\ -T\IZ @> \alpha_{\IZ} >> \Hom(\IZ, G). +T(H) @> \alpha_H >> \Hom(H, G) \\ +@V T(\widetilde{h}) VV @VV {-} \circ \widetilde{h} V \\ +T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G). \end{CD} $$ -Applying this to $x \in TH$ gives exactly that $\alpha_{\IZ}(Th(x))(1) = \alpha_H(x)(h)$. $\square$ +Applying this to $x \in T(H)$ gives exactly that $\alpha_{\IZ}(T(\widetilde{h})(x))(1) = \alpha_H(x)(h)$. $\square$ diff --git a/content/cocongruences_of_groups.md b/content/cocongruences_of_groups.md index 5bf9f650f..eb86f6bc1 100644 --- a/content/cocongruences_of_groups.md +++ b/content/cocongruences_of_groups.md @@ -1,11 +1,11 @@ --- -title: Cocongruences on groups are effective +title: Cocongruences of groups are effective description: This result will be proved more generally for categories in which pushouts and monomorphisms interact in a suitable way. --- -# Cocongruences on groups are effective +# Cocongruences of groups are effective -Our goal is to prove that every cocongruence in $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way. +Our goal is to prove that every cocongruence (see definition [here](/category-property/coquotients_of_cocongruences)) in $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way. We shall say that a category $\C$ has _good pushouts of monomorphisms_ if it has pushouts of monomorphisms and if, for every diagram of monomorphisms @@ -105,3 +105,7 @@ Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquel ::: Corollary 3 Every cocongruence in the category $\Grp$ is effective. ::: + +::: Proof +We know that $\Grp$ is balanced (since it is mono-regular, see [here](/category/Grp) for the proofs) and has equalizers. Moreover, it has good pushouts of monomorphisms by Proposition 1. Thus, the claim follows from Proposition 2. +::: diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md index 2dfa1973e..7160ffbe5 100644 --- a/content/congruences_in_rel.md +++ b/content/congruences_in_rel.md @@ -83,7 +83,7 @@ We can also conclude that $E$ is the kernel pair of this quotient, by the genera ::: Lemma Suppose we have a congruence $f, g : E \rightrightarrows X$ with a contractible coequalizer $$ E \, \overset{f}{\underset{g}{\rightrightarrows}} \, X \overset{e}{\rightarrow} Q $$ -with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e. we have a cartesian square +with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e. we have a pullback square $$ \begin{CD} diff --git a/content/constant_morphisms.md b/content/constant_morphisms.md index 6ffee55b0..ce391670b 100644 --- a/content/constant_morphisms.md +++ b/content/constant_morphisms.md @@ -5,8 +5,10 @@ description: We prove some results that help determine whether a morphism in a c # Results on constant morphisms +Recall that a map of sets $f : X \to Y$ is called constant if $f(x_1)=f(x_2)$ for all $x_1,x_2 \in X$. There is also another definition, which requires $f$ to factor through a singleton set, but we will not use it here. Hence, the unique map $\varnothing \to \varnothing$ is regarded as constant. + ::: Lemma 1 -A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map in the usual sense. +A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map. ::: ::: Proof diff --git a/content/effective-congruence-quotients.md b/content/effective-congruence-quotients.md index 897a6dfcc..5e21d597a 100644 --- a/content/effective-congruence-quotients.md +++ b/content/effective-congruence-quotients.md @@ -1,21 +1,25 @@ --- -title: Quotients of effective congruences are strict quotients -description: Quotients by effective congruences are characterized via a pullback +title: Quotients of effective congruences +description: If an effective congruence has a quotient, it is the kernel pair of this quotient. --- -# Quotients of effective congruences are strict quotients +# Quotients of effective congruences + +Recall that a congruence $E \rightrightarrows X$ is called effective if it is the kernel pair of some morphism with domain $X$. The next result shows that, in many situations, this morphism can be chosen canonically, namely as the quotient of the congruence, provided that it exists. ::: Lemma -Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square -$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E. \end{CD}$$ +An effective congruence whose coequalizer exists is the kernel pair of its coequalizer. More precisely, let $f,g : E \rightrightarrows X$ be an effective congruence. If $f,g$ have a coequalizer $p : X \to X/E$, then $f,g$ is the kernel pair of $p$. That is, the square +$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E \end{CD}$$ +is a pullback. ::: ::: Proof -Suppose we have $h : X \to Z$ so that we have a cartesian square -$$\begin{CD} E @> f >> X \\ @V g VV @VV h V \\ X @>> h > Z. \end{CD}$$ -Then by the universal property of the coequalizer, there is a unique morphism +Let $h : X \to Z$ be a morphism such that $f,g$ is the kernel pair of $h$. By the universal property of the coequalizer, there is a unique morphism $$\bar h : X/E \to Z$$ -such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then -$$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$ -so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic. +such that $h = \bar h \circ p$. Now suppose we have morphisms $a, b : T \rightrightarrows X$ such that $p \circ a = p \circ b$. Then +$$h \circ a = \bar h \circ p \circ a = \bar h \circ p \circ b = h \circ b.$$ +Since $f,g$ is the kernel pair of $h$, this means that the pair $a, b$ factors uniquely through the pair $f,g$. ::: + +This result is similar to the [lemma](/content/regular-epis-kernel-pairs) that a regular monomorphism is the equalizer of its cokernel pair, provided that the cokernel pair exists. + diff --git a/content/foundations.md b/content/foundations.md index 45139a357..7c32eeabe 100644 --- a/content/foundations.md +++ b/content/foundations.md @@ -97,7 +97,9 @@ If $\C, \D$ are categories, we can therefore construct the functor category $[\C It is better to state explicitly when the assumption of being locally small is needed. -Equivalences of categories are defined [as usual](https://en.wikipedia.org/wiki/Equivalence_of_categories). A category is _essentially small_ if it is equivalent to a small category. A collection $X$ is essentially small if and only if the associated discrete category $X_{\disc}$ (which has only identity morphisms) is essentially small. In this sense, the two notions are compatible. +Equivalences of categories are defined [as usual](https://en.wikipedia.org/wiki/Equivalence_of_categories). A category is _essentially small_ if it is equivalent to a small category. A collection $S$ is essentially small if and only if the associated discrete category $S_{\disc}$ (which has only identity morphisms) is essentially small. In this sense, the two notions are compatible. + +However, a collection of objects $S \subseteq \Ob(\C)$ of a category $\C$ must not be identified with the full subcategory of $\C$ spanned by $S$: they are different kinds of objects, and their notions of being essentially small differ. For example, the collection of all singletons in $\Set$ is not essentially small, since it is isomorphic to the collection of all sets, whereas the full subcategory of $\Set$ spanned by the singletons is essentially small, since it is equivalent to the trivial category $\1$. For instance, a [generating collection](/category-property/generating_collection) is required to be essentially small as a collection, i.e., isomorphic to a set. ## Representable functors diff --git a/content/missing_cogenerating_collections.md b/content/missing_cogenerating_collections.md index f17e0d41d..2d7d16593 100644 --- a/content/missing_cogenerating_collections.md +++ b/content/missing_cogenerating_collections.md @@ -6,7 +6,7 @@ description: A generalization of the proof that the category of commutative ring # Missing cogenerating collections ::: Lemma -Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: +Let $\C$ be a category and $U: \C \to \Set$ be a functor. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: 1. For any $X \in \F$ and any non-terminal $Y \in \C$, for every morphism $f: X \to Y$ its underlying map $U(f) : U(X) \to U(Y)$ is injective. 2. For every infinite cardinal number $\kappa$, there exists an object $X \in \F$ such that $\card(U(X)) \geq \kappa$ and such that $X$ has a non-identity endomorphism. @@ -15,5 +15,5 @@ Then $\C$ does not have a cogenerating collection. ::: ::: Proof -Assume that there is a cogenerating collection $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction. +Assume that there is a cogenerating collection $S$. In particular, $S$ is essentially small. By assumption (2) applied to a cardinal $\kappa > \sup \{\card(U(Y)) : Y \in S\}$, there is an object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$ for all $Y \in S$ and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction. ::: diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md index 1e8c0b29d..f6a817092 100644 --- a/content/natural_numbers_objects.md +++ b/content/natural_numbers_objects.md @@ -114,13 +114,16 @@ is an isomorphism. This is the precise connection to countable distributivity. Let $F : \C \to \D$ be left adjoint to $G : \D \to \C$. Assume that $1_{\C}$ is a terminal object of $\C$ such that $1_{\D} \coloneqq F(1_{\C})$ is a terminal object of $\D$. Then $F$ preserves natural numbers objects. That is, if $(N,z,s)$ is a natural numbers object in $\C$, then its image $(F(N),F(z),F(s))$ is a natural numbers object in $\D$. ::: +A direct proof is possible, but we give a proof that reduces the lemma to the well-known fact that left adjoints preserve initial objects. + ::: Proof For a category $\C$ with a terminal object $1_{\C}$, let $R(\C)$ denote the category of diagrams $$1_{\C} \xrightarrow{x_0} X \xrightarrow{r} X$$ -in $\C$. A natural numbers object in $\C$ is precisely an initial object of $R(\C)$. Suppose that $H : \C \to \D$ is a functor between categories with terminal objects that preserves terminal objects. Then $H$ induces a functor $R(H) : R(\C) \to R(\D)$ that maps +in $\C$. A morphism $(X,x_0,r) \to (Y,y_0,s)$ in $R(\C)$ is a morphism $f : X \to Y$ such that $f \circ x_0 = y_0$ and $s \circ f = f \circ r$. A natural numbers object in $\C$ is precisely an initial object of $R(\C)$. Suppose that $H : \C \to \D$ is a functor between categories with terminal objects that preserves terminal objects, and let $u : 1_{\D} \to H(1_{\C})$ be the unique isomorphism. Then $H$ induces a functor $R(H) : R(\C) \to R(\D)$ that maps $$1_{\C} \xrightarrow{x_0} X \xrightarrow{r} X$$ -to its image -$$1_{\D} \cong H(1_{\C}) \xrightarrow{H(x_0)} H(X) \xrightarrow{H(r)} H(X).$$ +to +$$1_{\D} \xrightarrow{H(x_0) \circ u} H(X) \xrightarrow{H(r)} H(X)$$ +and a morphism $f$ to $H(f)$. In the situation of the lemma, we therefore have two functors @@ -131,13 +134,19 @@ R(G) & : R(\D) \to R(\C). \end{align*} $$ -Notice that $G$ preserves terminal objects since it is a right adjoint. +Notice that $G$ preserves terminal objects since it is a right adjoint. Since $1_{\D} = F(1_{\C})$, the isomorphism $u$ for $F$ is the identity, so that $R(F)(X,x_0,r) = (F(X),F(x_0),F(r))$. The isomorphism $u : 1_{\C} \to G(1_{\D}) = G(F(1_{\C}))$ for $G$ is the unit $\eta_{1_{\C}}$, because both are morphisms into the terminal object $G(1_{\D})$. Hence, +$$R(G)(Y,y_0,s) = (G(Y), G(y_0) \circ \eta_{1_{\C}}, G(s)).$$ -We claim that $R(F)$ is left adjoint to $R(G)$. Indeed, for objects $(X,x_0,r) \in R(\C)$ and $(Y,y_0,s) \in R(\D)$, a morphism $R(F)(X,x_0,r) \to (Y,y_0,s)$ is the same as a morphism $f : F(X) \to Y$ such that +We claim that $R(F)$ is left adjoint to $R(G)$. Let +$$\varphi : \Hom(F(X),Y) \to \Hom(X,G(Y)), \quad f \mapsto G(f) \circ \eta_X$$ +denote the natural bijection of the adjunction $F \dashv G$. Now let $(X,x_0,r) \in R(\C)$ and $(Y,y_0,s) \in R(\D)$. A morphism $R(F)(X,x_0,r) \to (Y,y_0,s)$ is a morphism $f : F(X) \to Y$ such that $$f \circ F(x_0) = y_0, \quad s \circ f = f \circ F(r).$$ -Under the adjunction $F \dashv G$, it corresponds to a morphism $\widetilde{f} : X \to G(Y)$ such that -$$\widetilde{f} \circ x_0 = G(y_0), \quad G(s) \circ \widetilde{f} = \widetilde{f} \circ r.$$ -This is precisely a morphism $(X,x_0,r) \to R(G)(Y,y_0,s)$. +Since $\varphi$ is bijective, the first equation is equivalent to $\varphi(f \circ F(x_0)) = \varphi(y_0)$. By naturality of $\varphi$ in the first argument, the left-hand side is $\varphi(f) \circ x_0$, and by definition of $\varphi$, the right-hand side is $G(y_0) \circ \eta_{1_{\C}}$. So the first equation means +$$\varphi(f) \circ x_0 = G(y_0) \circ \eta_{1_{\C}}.$$ +Similarly, the second equation is equivalent to $\varphi(s \circ f) = \varphi(f \circ F(r))$, which by naturality of $\varphi$ in the second and in the first argument means +$$G(s) \circ \varphi(f) = \varphi(f) \circ r.$$ +These two equations say precisely that $\varphi(f)$ is a morphism $(X,x_0,r) \to R(G)(Y,y_0,s)$. Thus, $\varphi$ restricts to a natural bijection +$$\Hom\bigl(R(F)(X,x_0,r),(Y,y_0,s)\bigr) \cong \Hom\bigl((X,x_0,r),R(G)(Y,y_0,s)\bigr).$$ Since $R(F)$ is a left adjoint, it preserves initial objects. This is precisely the statement that $F$ preserves natural numbers objects. ::: diff --git a/content/preadditive_structure_unique.md b/content/preadditive_structure_unique.md index 647ed1ea0..e55944d1c 100644 --- a/content/preadditive_structure_unique.md +++ b/content/preadditive_structure_unique.md @@ -5,22 +5,40 @@ description: In the presence of finite products, a preadditive structure on a gi # Uniqueness of preadditive structures -::: Lemma -Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products and finite coproducts. Then for all objects $X,Y$ the canonical morphism -$$\alpha : X \oplus Y \to X \times Y$$ -is an isomorphism. Moreover, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum +::: Lemma 1 +Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products. Then finite coproducts exist as well. +::: + +::: Proof +The terminal object $1$ is also an initial object, because for all objects $A$ there is the zero morphism $0_{1,A} : 1 \to A$, and it is uniquely determined because any morphism $f : 1 \to A$ satisfies +$$f = f \circ \id_1 = f \circ 0_{1,1} = 0_{1,A}.$$ +It remains to construct binary coproducts. Actually, their underlying objects coincide with binary products. Let $A,B$ be objects. We define the morphism $i_1 : A \to A \times B$ by $p_1 \circ i_1 = \id_A$ and $p_2 \circ i_1 = 0_{A,B}$. Similarly, we define the morphism $i_2 : B \to A \times B$ by $p_1 \circ i_2 = 0_{B,A}$ and $p_2 \circ i_2 = \id_B$. We claim that +$$A \xrightarrow{i_1} A \times B \xleftarrow{i_2} B$$ +is a binary coproduct. First, notice that +$$i_1 \circ p_1 + i_2 \circ p_2 = \id_{A \times B}$$ +holds in $\End(A \times B)$. In fact, if we compose the left-hand side with $p_1$, we get +$$p_1 \circ i_1 \circ p_1 + p_1 \circ i_2 \circ p_2 = \id_A \circ p_1 + 0_{B,A} \circ p_2 = p_1,$$ +and a similar calculation works for $p_2$. Now let $f : A \to T$ and $g : B \to T$ be morphisms. We want to show that there exists a unique $h : A \times B \to T$ with $h \circ i_1 = f$ and $h \circ i_2 = g$. To show uniqueness, notice that +$$h = h \circ (i_1 \circ p_1 + i_2 \circ p_2) = f \circ p_1 + g \circ p_2.$$ +Conversely, if we define $h : A \times B \to T$ via $h \coloneqq f \circ p_1 + g \circ p_2$, then +$$h \circ i_1 = f \circ p_1 \circ i_1 + g \circ p_2 \circ i_1 = f \circ \id_A + g \circ 0_{A,B} = f,$$ +and similarly $h \circ i_2 = g$. +::: + +::: Lemma 2 +Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products, hence with finite coproducts by Lemma 1. Then for all objects $X,Y$ the canonical morphism $\alpha : X \oplus Y \to X \times Y$ is an isomorphism. Moreover, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum $$f+g : A \to B$$ -is the composite of $(f,g) : A \to B \times B$, the inverse $\alpha^{-1} : B \oplus B \to B \times B$, and the codiagonal $\nabla : B \oplus B \to B$. +is the composite of $(f,g) : A \to B \times B$, the inverse $\alpha^{-1} : B \times B \to B \oplus B$, and the codiagonal $\nabla : B \oplus B \to B$. ::: ::: Proof -The morphism $\alpha : X \oplus Y \to X \times Y$ is defined by the equations +In any category with zero morphisms, the morphism $\alpha : X \oplus Y \to X \times Y$ is defined by the equations $$p_1 \circ \alpha \circ i_1 = \id_X, \quad p_2 \circ \alpha \circ i_2 = \id_Y,$$ -$$p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0.$$ -It does not depend on the choice of preadditive structure since zero morphisms are unique. It is an isomorphism: Define +$$p_2 \circ \alpha \circ i_1 = 0_{X,Y}, \quad p_1 \circ \alpha \circ i_2 = 0_{Y,X}.$$ +It does not depend on the choice of preadditive structure since zero morphisms are unique. We now check that it is an isomorphism. (This is already contained in the proof of Lemma 1, since there we have constructed binary coproducts in such a way that $\alpha$ is even the identity, but we repeat the proof here, since we need the inverse morphism anyway.) Define $$\beta \coloneqq i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y.$$ Then $\alpha \circ \beta = \id_{X \times Y}$ because -$$p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \id_X \circ p_1 + 0 \circ p_2 = p_1$$ +$$p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \id_X \circ p_1 + 0_{Y,X} \circ p_2 = p_1$$ and likewise $p_2 \circ \alpha \circ \beta = p_2$. We also have $\beta \circ \alpha = \id_{X \oplus Y}$ with a very similar calculation that shows $\beta \circ \alpha \circ i_1 = i_1$ and $\beta \circ \alpha \circ i_2 = i_2$. Therefore, for morphisms $f,g : A \rightrightarrows B$ the composite $A \to B$ in the claim is equal to $$ diff --git a/content/subcategories.md b/content/subcategories.md index 43182e86f..7c0066b5a 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -48,6 +48,7 @@ $$ \end{align*} $$ +It is routine to check that the composite is the natural morphism. ::: ::: Lemma 4 diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 5e6db445c..2c3fbc9bb 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -72,6 +72,7 @@ conclusions: - effective congruences - quotients of congruences + # TODO: rename congruences consistently to q_1, q_2 (and cocongruences to j_1, j_2) proof: '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 $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \id$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \id$ and $p_2 \circ r \circ p_1 = p_2 \circ \id$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \id$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\id_X$.' - id: preadditive_kernels_normal_imply_effective_congruences @@ -86,7 +87,7 @@ To see this, suppose we have a pair of generalized elements $x_1, x_2 \in X(T)$. Then we have $$\begin{align*} (x_1,x_2) \in E & \iff (x_1 - x_2,0) \in E \\ & \iff x_1 - x_2 \in E_0 \\ & \iff h(x_1 - x_2) = 0 \\ & \iff h(x_1) = h(x_2). \end{align*}$$ - In particular, applying the forward implications in the case $T \coloneqq E$, $x_1 \coloneqq f$, $x_2 \coloneqq 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. + In particular, applying the forward implications in the case $T \coloneqq E$, $x_1 \coloneqq f$, $x_2 \coloneqq 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 pullback square. - id: additive_effective_congruences_imply_normal assumptions: diff --git a/database/data/category-properties/additive.yaml b/database/data/category-properties/additive.yaml index cbd8c7427..f72a37d60 100644 --- a/database/data/category-properties/additive.yaml +++ b/database/data/category-properties/additive.yaml @@ -1,6 +1,6 @@ id: additive relation: is -description: A category is additive if it is preadditive and has finite products (equivalently, finite coproducts). Note that in the context of finite products, the preadditive structure is unique. +description: A category is additive if it is preadditive and has finite products. It then also has finite coproducts (see Lemma 1 here), which explains why this property is self-dual. Moreover, the preadditive structure is uniquely determined (see Lemma 2 here). nlab_link: https://ncatlab.org/nlab/show/additive+category dual: additive invariant_under_equivalences: true diff --git a/database/data/category-properties/coquotients of cocongruences.yaml b/database/data/category-properties/coquotients of cocongruences.yaml index d9179b910..460cb25f1 100644 --- a/database/data/category-properties/coquotients of cocongruences.yaml +++ b/database/data/category-properties/coquotients of cocongruences.yaml @@ -1,6 +1,19 @@ id: coquotients of cocongruences relation: has -description: 'A cocongruence (or internal equivalence corelation) on an object $X$ of a category is a parallel pair $i_1, i_2 : X \rightrightarrows E$ which is jointly epimorphic, and such that for every object $T$, the image of $({-} \circ i_1, {-} \circ i_2) : \Hom(E, T) \to \Hom(X, T)^2$ is an equivalence relation. The category has coquotients of cocongruences if for each such cocongruence, there exists an equalizer of $i_1$ and $i_2$. Note that in the case of a category with binary copowers, the corresponding quotients of $X + X$ are also commonly referred to as cocongruences, or as internal equivalence corelations.' +description: >- + A cocongruence (or internal equivalence corelation) on an object $X$ of a category is a parallel pair $j_1, j_2 : X \rightrightarrows E$ which is jointly epimorphic, and such that for every object $T$, the image of $({-} \circ j_1, {-} \circ j_2) : \Hom(E, T) \to \Hom(X, T)^2$ is an equivalence relation. If pushouts exist (or at least the pushout displayed below), the latter condition is equivalent to the existence of morphisms + $$\begin{align*} + r & : E \to X & \quad \text{(coreflexivity)} \\ + s & : E \to E & \quad \text{(cosymmetry)} \\ + t & : E \to E \sqcup_{j_2,X,j_1} E & \quad \text{(cotransitivity)} + \end{align*}$$ + satisfying the following equations: + $$\begin{align*} + r \circ j_1 & = \id_X & r \circ j_2 & = \id_X \\ + s \circ j_1 & = j_2 & s \circ j_2 & = j_1 \\ + t \circ j_1 & = \iota_1 \circ j_1 & t \circ j_2 & = \iota_2 \circ j_2 + \end{align*}$$ + In particular, $j_1,j_2$ is a coreflexive pair. A coquotient of $j_1,j_2$ is an equalizer of $j_1,j_2$. We say that a category has coquotients of cocongruences if every cocongruence has a coquotient. Note that in the case of a category with binary copowers, the corresponding quotient objects $X + X \twoheadrightarrow E$ are also commonly referred to as cocongruences, or as internal equivalence corelations. nlab_link: null dual: quotients of congruences invariant_under_equivalences: true diff --git a/database/data/category-properties/effective cocongruences.yaml b/database/data/category-properties/effective cocongruences.yaml index 6c053dd70..bb4bbf21d 100644 --- a/database/data/category-properties/effective cocongruences.yaml +++ b/database/data/category-properties/effective cocongruences.yaml @@ -1,8 +1,8 @@ id: effective cocongruences relation: has description: >- - 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 @VV f V \\ X @>> g > E. \end{CD}$$ + A cocongruence $j_1,j_2 : 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 pushout square + $$\begin{CD} Y @> h >> X \\ @V h VV @VV j_1 V \\ X @>> j_2 > E. \end{CD}$$ A category has effective cocongruences if every cocongruence in the category is effective. nlab_link: null dual: effective congruences diff --git a/database/data/category-properties/effective congruences.yaml b/database/data/category-properties/effective congruences.yaml index b572cb05d..c8143edf4 100644 --- a/database/data/category-properties/effective congruences.yaml +++ b/database/data/category-properties/effective congruences.yaml @@ -1,8 +1,8 @@ id: effective congruences relation: has description: >- - 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 @VV h V \\ X @>> h > Y. \end{CD}$$ + A congruence $q_1, q_2 : 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 pullback square + $$\begin{CD} E @> q_1 >> X \\ @V q_2 VV @VV h V \\ X @>> h > Y. \end{CD}$$ A category has effective congruences if every congruence in the category is effective. nlab_link: https://ncatlab.org/nlab/show/congruence dual: effective cocongruences diff --git a/database/data/category-properties/preadditive.yaml b/database/data/category-properties/preadditive.yaml index c06e176e4..a98d58119 100644 --- a/database/data/category-properties/preadditive.yaml +++ b/database/data/category-properties/preadditive.yaml @@ -6,7 +6,7 @@ description: >- f \circ (g + h) &= f \circ g + f \circ h \\ (f + g) \circ h &= f \circ h + g \circ h. \end{align*}$$ - Note that being preadditive is an extra structure. The property here merely says that a preadditive structure exists. Furthermore, since categories are not assumed to be locally small (see Foundations), the abelian group $\Hom(A,B)$ is not necessarily a set. In contrast, a locally small preadditive category is precisely an $(\Ab,\otimes)$-enriched category. + Note that being preadditive is an extra structure. The property here merely says that a preadditive structure exists. Furthermore, since categories are not assumed to be locally small (see Foundations), the collection $\Hom(A,B)$ with abelian group structure is not necessarily a set. In contrast, a locally small preadditive category is precisely an $(\Ab,\otimes)$-enriched category. nlab_link: https://ncatlab.org/nlab/show/Ab-enriched+category dual: preadditive invariant_under_equivalences: true diff --git a/database/data/category-properties/quotients of congruences.yaml b/database/data/category-properties/quotients of congruences.yaml index 8d2225fec..cfef33f56 100644 --- a/database/data/category-properties/quotients of congruences.yaml +++ b/database/data/category-properties/quotients of congruences.yaml @@ -1,6 +1,19 @@ id: quotients of congruences relation: has -description: 'A congruence (or internal equivalence relation) on an object $X$ of a category is a parallel pair $p_1, p_2 : E \rightrightarrows X$ which is jointly monomorphic, and such that for every object $T$, the image of $(p_1 \circ {-}, p_2 \circ {-}) : \Hom(T, E) \to \Hom(T, X)^2$ is an equivalence relation. The category has quotients of congruences if for each such congruence, there exists a coequalizer of $p_1$ and $p_2$. Note that in the case of a category with binary powers, the corresponding subobjects of $X \times X$ are also commonly referred to as congruences, or as internal equivalence relations.' +description: >- + A congruence (or internal equivalence relation) on an object $X$ of a category is a parallel pair $q_1, q_2 : E \rightrightarrows X$ which is jointly monomorphic, and such that for every object $T$, the image of $(q_1 \circ {-}, q_2 \circ {-}) : \Hom(T, E) \to \Hom(T, X)^2$ is an equivalence relation. If pullbacks exist (or at least the pullback displayed below), the latter condition is equivalent to the existence of morphisms + $$\begin{align*} + r & : X \to E & \quad \text{(reflexivity)} \\ + s & : E \to E & \quad \text{(symmetry)} \\ + t & : E \times_{q_2,X,q_1} E \to E & \quad \text{(transitivity)} + \end{align*}$$ + satisfying the following equations: + $$\begin{align*} + q_1 \circ r & = \id_X & q_2 \circ r & = \id_X \\ + q_1 \circ s & = q_2 & q_2 \circ s & = q_1 \\ + q_1 \circ t & = q_1 \circ p_1 & q_2 \circ t & = q_2 \circ p_2 + \end{align*}$$ + In particular, $q_1,q_2$ is a reflexive pair. A quotient of $q_1,q_2$ is a coequalizer of $q_1,q_2$. We say that a category has quotients of congruences if every congruence has a quotient. Note that in the case of a category with binary powers, the corresponding subobjects $E \hookrightarrow X \times X$ are also commonly referred to as congruences, or as internal equivalence relations. nlab_link: https://ncatlab.org/nlab/show/congruence dual: coquotients of cocongruences invariant_under_equivalences: true diff --git a/database/data/morphisms/empty-map.yaml b/database/data/morphisms/empty-map.yaml index 57b514199..aace5b77e 100644 --- a/database/data/morphisms/empty-map.yaml +++ b/database/data/morphisms/empty-map.yaml @@ -18,7 +18,7 @@ satisfied_properties: proof: It is vacuously injective. - property: constant - proof: The map is clearly constant, and by Lemma 1 here this means that the morphism in $\Set$ is constant. + proof: The map is vacuously constant, and by Lemma 1 here this means that the morphism in $\Set$ is constant. - property: coconstant proof: This is because $\varnothing$ is initial; see also the dual of Lemma 4 here.