diff --git a/content/Grp_total_explicit_proof.md b/content/Grp_total_explicit_proof.md new file mode 100644 index 00000000..2149442f --- /dev/null +++ b/content/Grp_total_explicit_proof.md @@ -0,0 +1,37 @@ +--- +title: Explicit Proof that the Category of Groups is Total +description: An explicit construction of the left adjoint to the covariant Yoneda embedding on the category of groups +author: Daniel Schepler +--- + +## Explicit Proof that the Category of Groups is Total + +We will fix a functor $T : \Grp^{\op} \to \Set$. Based on this, we need to construct a group $L(T)$. The construction will work as follows: we start with a set of generators $e_x$, one for each element $x \in T\IZ$. Now let $\mu : \IZ \to \IZ * \IZ'$ be the comultiplication homomorphism, $1 \mapsto 1 \cdot 1'$, and $i_1, i_2 : \IZ \rightrightarrows \IZ * \IZ'$ the two coprojections. We now add a relation $e_{T\mu(x)} = e_{Ti_1(x)} \cdot e_{Ti_2(x)}$ for each element $x \in T(\IZ * \IZ')$. Similarly, letting $\iota : \IZ \to \IZ$ be the coinverse homomorphism, we add a relation $e_{T\iota(x)} = e_x^{-1}$ for each element $x \in T\IZ$; and letting $\varepsilon : \IZ \to 0$ be the coidentity homomorphism, we add a relation $e_{T\varepsilon(x)} = 1$ for each element $x \in T0$. + +We first need to define the natural transformation $\eta_T : T \to \Hom({-}, L(T))$. To start, for each group $H$ we need a function $TH \to \Hom(H, L(T))$. We will define this function to send $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$, 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 +$$\begin{CD} +T(H) @> = >> T(H)\\ +@V T(h * h') VV @VVV\\ +T(\IZ * \IZ') @>>> T(\IZ) +\end{CD}$$ +where on the bottom we use $T\mu, Ti_1, Ti_2$. Applying this to $x\in TH$, we get $Th(x)$, $Th'(x)$, and $T(h h')(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)} e_{Th'(x)},$$ +as required. Similar proofs show that the map $H \to G$ respects inverses and the identity. We leave it as an exercise for the reader to show this 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} \circ (\eta_T)_{\alpha} : 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$. + +For the existence part, the first step is to show there is a gruop homomorphism $L(T) \to G$ with the images of $e_x$ required by the previous part, i.e. $e_x \mapsto \alpha_{\IZ}(x)(1)$. To prove this, we need to check that the relations in $L(T)$ are collapsed in $G$. Now, for each $x \in T(\IZ * \IZ')$, we have three commutative diagrams of the form +$$\begin{CD} +T(\IZ * \IZ') @> \alpha_{\IZ * \IZ'} >> \Hom(\IZ * \IZ', G) @> \simeq >> UG \times UG\\ +@VVV @VVV @VVV\\ +T(\IZ) @> \alpha_{\IZ} >> \Hom(\IZ, G) @> \simeq >> UG +\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 collapsed. + +Finally, we need to show $\alpha = y_{\varphi} \circ \eta_T$. It suffices to show $\alpha_H = (y_{\varphi})_H \circ (\eta_T)_H : TH \to \Hom(H, L(T)) \to \Hom(H, G)$ 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 homorphism $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 +$$\begin{CD} +TH @> \alpha_H >> \Hom(H, G) \\ +@V Th VV @VV {-} \circ 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$ diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md index a59d81f7..a397ba6b 100644 --- a/content/missing_cogenerator.md +++ b/content/missing_cogenerator.md @@ -13,8 +13,18 @@ Let $\C$ be a pointed category with a faithful functor $U: \C \to \Set$. Assume 1. For any $X \in \F$ and any $Y \in \C$, every non-zero morphism $f: X \to Y$ is injective on underlying sets. 2. For every $Y \in \C$ there is some object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$. -Then $\C$ does not have a cogenerator. +Then $\C$ does not have a cogenerator. Moreover, $\C$ is not cototal. ::: _Proof._ -Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. $\square$ +Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. + +Now assume that $\C$ is cocotal. Using the axiom of choice, we may assume that for each small cardinal $\kappa$, there is at most one element $X \in \F$ such that $\card(U(X)) = \kappa$. We define a functor $T : \C \to \Set$ which is morally defined by $T(Y) \coloneqq \prod_{X \in \F} \Hom(X, Y)$. In this product, we know that $\Hom(X, Y) = \{ 0 \}$ whenever $\card(U(X)) > \card(U(Y))$, so every term except for a small number is a singleton and does not change the product. Thus, we may define +$$T(Y) \coloneqq \prod_{X \in \F : \card(U(X)) \le \card(U(Y))} \Hom(X, Y),$$ +and define the functor structure by extending tuples with zero morphisms as necessary. + +Now, if $L : [\C, \Set] \to \C^{\op}$ is the left adjoint of the contravariant Yoneda embedding $y : \C^{op} \to [\C, \Set]$, then we have a bijection +$$\Hom_{\C}(X, L(T)) \simeq \Hom(T, \Hom(X, {-}))$$ +for each object $X$ of $\C$. Now let $X_0$ be an element of $\F$ such that $\card(U(X_0)) > \card(U(L(T)))$. Then we can define two natural transformations $T \to \Hom({-}, X_0)$: one is the constant zero map; and the other is selection of the $X$ component, i.e. given an element of $TY = \prod_{X\in F : \card(U(X)) \le \card(U(Y))} \Hom(X, Y)$ we select the $X$ component if $\card(U(X)) \le \card(U(Y))$, or set the result to the zero morphism if $\card(U(X)) > \card(U(Y))$. Note these two natural transformations are unequal, since for example we can define an element of $T(X_0)$ which is $\id_{X_0}$ on the $X_0$ component and zero on the other components, and the two transformations map this element to $\id_{X_0} \ne 0$. + +Therefore, by the above bijection, $\Hom_{\C}(X_0, L(T))$ has at least two elements, out of which at least one must be non-zero and therefore injective on underlying sets. This contradicts the assumption that $\card(U(X_0)) > \card(U(L(T))$. $\square$ diff --git a/databases/catdat/data/categories/Alg(R).yaml b/databases/catdat/data/categories/Alg(R).yaml index 96fc09ad..2cf70975 100644 --- a/databases/catdat/data/categories/Alg(R).yaml +++ b/databases/catdat/data/categories/Alg(R).yaml @@ -43,6 +43,9 @@ unsatisfied_properties: - property: cogenerating set proof: 'We apply this lemma to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' + - property: cototal + proof: Essentially the same proof as for $\CAlg(R)$ works here. + - property: codistributive proof: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see MSE/625874 for their description) and $A$ is an $R$-algebra, the canonical morphism $A \sqcup R^2 \to (A \sqcup R)^2 = A^2$ is usually no isomorphism. For example, for $A = R[X]$ the coproduct on the LHS is not commutative, it has the algebra presentation $\langle X,E : E^2=E \rangle$.' diff --git a/databases/catdat/data/categories/CAlg(R).yaml b/databases/catdat/data/categories/CAlg(R).yaml index 0244eb45..9a8fad0d 100644 --- a/databases/catdat/data/categories/CAlg(R).yaml +++ b/databases/catdat/data/categories/CAlg(R).yaml @@ -19,7 +19,7 @@ satisfied_properties: proof: There is a forgetful functor $\CAlg(R) \to \Set$ and $\Set$ is locally small. - property: finitary algebraic - proof: Take the algebraic theory of a commutative ring. + proof: Take the algebraic theory of a commutative $R$-algebra. - property: strict terminal object proof: 'If $f : 0 \to R$ is a homomorphism, then $R$ satisfies $1=f(1)=f(0)=0$, so that $R=0$.' @@ -41,6 +41,9 @@ unsatisfied_properties: - property: cogenerating set proof: 'We apply this lemma to the collection of commutative $R$-algebras which are fields: If $F$ is a commutative $R$-algebra that is also a field and $A$ is a non-trivial commutative $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' + - property: cototal + proof: 'Let $\F$ be the family of commutative $R$-algebras of the form $R \times k$ where $k$ is an infinite field including a quotient field of $R$. Then for any commutative $R$-algebra $A$, we have a distinguished morphism $R \times k \to A$ consisting of the projection to $R$ followed by the unique morphism $R \to A$. Moreover, if we have any morphism $\varphi : R \times k \to A$ which is not equal to the distinguished morphism, that implies that $\varphi(0, 1) \ne 0$, so the rng homomorphism $k \to R \times k \to A$ is injective, implying $\card(U(A)) \ge \card(U(k))$. From here, an argument similar to the one here gives a contradiction, using the distinguished morphisms in place of zero morphisms.' + - property: countably codistributive proof: 'The canonical homomorphism $A \otimes_R R^{\IN} \to A^{\IN}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A \coloneqq K[X]$ and consider the sequence $(X^n)_{n} \in A^{\IN}$.' diff --git a/databases/catdat/data/categories/CRing.yaml b/databases/catdat/data/categories/CRing.yaml index d95061e9..b90c6bc4 100644 --- a/databases/catdat/data/categories/CRing.yaml +++ b/databases/catdat/data/categories/CRing.yaml @@ -47,6 +47,9 @@ unsatisfied_properties: - property: cogenerating set proof: 'We apply this lemma to the collection of fields: If $F$ is a field and $R$ is a non-trivial commutative ring, any ring homomorphism $F \to R$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' + - property: cototal + proof: 'This is a special case of the proof for $\CAlg(R)$ with $R = \IZ$.' + - property: countably codistributive proof: 'The canonical homomorphism $\IQ \otimes \IZ^{\IN} \to (\IQ \otimes \IZ)^{\IN} = \IQ^{\IN}$ is not an isomorphism: its image consists of those sequences of rational numbers whose denominators can be bounded.' diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index 80e08f45..702677bb 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -40,9 +40,6 @@ unsatisfied_properties: - property: balanced proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism which is not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. - - property: cogenerating set - proof: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in $\Mon$, which we know does not exist.' - - property: regular proof: See Example 3.14 at the nLab. @@ -85,6 +82,16 @@ unsatisfied_properties: $$\Sub_{\reg}(\{ 0 \to 1 \to 2 \}) \to \Sub_{\reg}(\{ 0 \to 1 \}) \times_{\Sub_{\reg}(\{1\})} \Sub_{\reg}(\{ 1 \to 2 \})$$ is not injective. Therefore, $\Sub_{\reg} : \Cat^{\op} \to \Set^+$ does not preserve pullbacks, so it cannot be representable. + - property: cototal + proof: >- + For each infinite cardinal $\kappa$, choose a simple group $S_\kappa$ of cardinality $\kappa$ with at least $\kappa$ distinct automorphisms (for example the group of permutations of $\kappa$ of finite support which are even). We will define a functor $T : \Cat \to \Set$ which morally will send a category $\C$ to the collection-sized wide pullback of $[B S_\kappa, \C] \to [1, \C]$. Namely, if $\kappa$ is greater than the cardinality of any endomorphism monoid of an object of $\C$, then the image in $[1, \C]$ uniquely determines a functor in $[B S_\kappa, \C]$. Thus, we can restrict to the corresponding pullback with $\kappa$ restricted to be at most $\max(\aleph_0, \lambda)$ where $\lambda$ is the supremum of the cardinalities of endomorphism monoids; and this also forms a pullback of the full collection-sized diagram. + + Now assume $\Cat$ is cototal with $L : [\Cat, \Set] \to \Cat^{\op}$ a left adjoint to the contravariant Yoneda embedding. Then for each infinite cardinal $\kappa$, we would have a bijection + $$[B S_\kappa, L(T)] \simeq \Hom(T, [B S_\kappa, -]).$$ + On the other hand, we have at least $\kappa$ distinct morphisms $T \to [B S_\kappa, -]$: for each automorphism $\pi$ of $S_\kappa$, we can take the natural transformation which selects the $\kappa$ component of the limit, and then composes with $B \pi$. To see these are distinct, apply them to the element of $T(B S_\kappa)$ which is the identity on the $\kappa$ component and $B(0)$ on the $\lambda$ component for $\lambda \ne \kappa$. + + However, if $\kappa$ is greater than the cardinality of any endomorphism monoid of $L(T)$, then any functor $B S_\kappa \to L(T)$ must act on the morphisms of $B S_\kappa$ by sending each to the identity morphism on the image object. Therefore, $\card([B S_\kappa, L(T)]) \le \card(\Ob(L(T)))$. Thus, if we also choose $\kappa > \card(\Ob(L(T)))$, then we get a contradiction. + special_objects: initial object: description: empty category diff --git a/databases/catdat/data/categories/Grp.yaml b/databases/catdat/data/categories/Grp.yaml index 1b541e60..190d37b7 100644 --- a/databases/catdat/data/categories/Grp.yaml +++ b/databases/catdat/data/categories/Grp.yaml @@ -39,6 +39,10 @@ satisfied_properties: - property: effective cocongruences proof: A proof can be found here. + - property: total + proof: This follows formally from the fact that $\Grp$ is finitary algebraic and therefore locally presentable. For a more explicit proof, see here. + check_redundancy: false + unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -46,7 +50,7 @@ unsatisfied_properties: - property: normal proof: Every non-normal subgroup (such as $C_2 \hookrightarrow S_3$) provides a counterexample. - - property: cogenerator + - property: cototal proof: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism from a simple group to a group must be injective, and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' - property: coregular diff --git a/databases/catdat/data/categories/Haus.yaml b/databases/catdat/data/categories/Haus.yaml index 81bcd23e..6ed88783 100644 --- a/databases/catdat/data/categories/Haus.yaml +++ b/databases/catdat/data/categories/Haus.yaml @@ -26,9 +26,11 @@ satisfied_properties: - property: equalizers proof: This follows from the corresponding fact for $\Top$ since subspaces of Hausdorff spaces are again Hausdorff. + check_redundancy: false - property: products proof: This follows from the corresponding fact for $\Top$ since products of Hausdorff spaces are again Hausdorff. + check_redundancy: false - property: cocomplete proof: This follows since $\Haus$ is a reflective subcategory of $\Top$, which is cocomplete. For the reflector, see e.g. the nLab. Explicitly, we construct the colimit of Hausdorff spaces by applying the reflector to the colimit of the underlying topological spaces. diff --git a/databases/catdat/data/categories/LRS_R.yaml b/databases/catdat/data/categories/LRS_R.yaml index 9bb3f576..76955462 100644 --- a/databases/catdat/data/categories/LRS_R.yaml +++ b/databases/catdat/data/categories/LRS_R.yaml @@ -53,6 +53,9 @@ unsatisfied_properties: Alternatively, using the usual adjunction between affine schemes and locally ringed spaces (EGA I (1971), Ch. 1, Prop. 1.6.3), a generating set in $\LRS_R$ would induce a generating set in the category of affine $R$-schemes, which contradicts the fact that $\CAlg(R)$ does not have a cogenerating set. + - property: total + proof: 'The adjunction between the global sections functor and the $\Spec$ functor (EGA I (1971), Ch. 1, Prop. 1.6.3) makes $\CAlg(R)^{\op}$ into a reflective subcategory of $\LRS_R$. Therefore, if $LRS_R$ were total, then \CAlg(R) would be cototal, which we know is not the case.' + - property: cartesian closed proof: This is Corollary 4(a) here. check_redundancy: false diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index d7ce5a65..e5aafc47 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -36,9 +36,11 @@ satisfied_properties: - property: complete proof: Take the limit of the underlying sets and take the smallest $\sigma$-algebra making all projections measurable. + check_redundancy: false - property: cocomplete proof: Take the colimit of the underlying sets and take the largest $\sigma$-algebra making all inclusions measurable. That is, a set is measurable iff its preimage under each inclusion is measurable. + check_redundancy: false - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.' diff --git a/databases/catdat/data/categories/Mon.yaml b/databases/catdat/data/categories/Mon.yaml index 10474de5..2d198115 100644 --- a/databases/catdat/data/categories/Mon.yaml +++ b/databases/catdat/data/categories/Mon.yaml @@ -39,7 +39,7 @@ unsatisfied_properties: - property: Malcev proof: 'Consider the submonoid $\{(a,b) : a \leq b \}$ of $\IN^2$.' - - property: cogenerator + - property: cototal proof: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism $G \to M$ from a simple group $G$ to a monoid $M$ must be injective (as it corestricts to a homomorphism of groups $G \to M^{\times}$), and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' - property: counital diff --git a/databases/catdat/data/categories/On.yaml b/databases/catdat/data/categories/On.yaml index 5f67174e..1e16de13 100644 --- a/databases/catdat/data/categories/On.yaml +++ b/databases/catdat/data/categories/On.yaml @@ -45,6 +45,7 @@ unsatisfied_properties: - property: well-copowered proof: The "quotients" of $0$ are all ordinals. + check_redundancy: false - property: inverse proof: Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$. diff --git a/databases/catdat/data/categories/Ring.yaml b/databases/catdat/data/categories/Ring.yaml index 0e2a6342..6167ca97 100644 --- a/databases/catdat/data/categories/Ring.yaml +++ b/databases/catdat/data/categories/Ring.yaml @@ -46,6 +46,9 @@ unsatisfied_properties: - property: cogenerating set proof: 'We apply this lemma to the collection of fields: If $F$ is a field and $R$ is a non-trivial ring, any ring homomorphism $F \to R$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' + - property: cototal + proof: 'This is a special case of the proof for $\Alg(R)$ with $R = \IZ$.' + - property: codistributive proof: 'If $\sqcup$ denotes the coproduct of rings (see MSE/625874 for their description) and $R$ is a ring, the canonical morphism $R \sqcup \IZ^2 \to (R \sqcup \IZ)^2 = R^2$ is usually no isomorphism. For example, for $R = \IZ[X]$ the coproduct on the LHS is not commutative, it has the ring presentation $\langle X,E : E^2=E \rangle$.' diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index d491880c..75ba1d64 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -36,7 +36,7 @@ unsatisfied_properties: - property: balanced proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. (The proof can be reduced to the unital case.) - - property: cogenerator + - property: cototal proof: 'We apply this lemma to the collection of fields: Any non-zero rng homomorphism from a field to a rng must be injective, and for every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$.' - property: counital diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index c6a2b274..b739aaa3 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -21,6 +21,7 @@ satisfied_properties: - property: complete proof: Take the limit of the underlying sets and endow it with the coarsest topology making all projections continuous. + check_redundancy: false - property: cocomplete proof: Take the colimit of the underlying sets and endow it with the finest topology making all inclusions continuous. diff --git a/databases/catdat/data/category-implications/accessible.yaml b/databases/catdat/data/category-implications/accessible.yaml index 94033586..c26fdb79 100644 --- a/databases/catdat/data/category-implications/accessible.yaml +++ b/databases/catdat/data/category-implications/accessible.yaml @@ -28,6 +28,14 @@ proof: This follows from one of equivalent formulations of locally presentable categories. is_equivalence: true +- id: locally_presentable_consequence + assumptions: + - locally presentable + conclusions: + - total + proof: ... + is_equivalence: false + - id: locally_finitely_presentable_consequence assumptions: - locally finitely presentable diff --git a/databases/catdat/data/category-implications/total.yaml b/databases/catdat/data/category-implications/total.yaml new file mode 100644 index 00000000..3eafb7b0 --- /dev/null +++ b/databases/catdat/data/category-implications/total.yaml @@ -0,0 +1,28 @@ +# results on total and cototal categories + +- id: total_definition + assumptions: + - total + conclusions: + - locally essentially small + proof: This is true by definition. + is_equivalence: false + +- id: total_consequences + assumptions: + - total + conclusions: + - complete + - cocomplete + proof: 'If a category $\C$ is total, then $\C$ is a reflective subcategory of the presheaf category $[\C^{\op}, \Set]$ where the latter is cocomplete. As for completeness: suppose $(X_i)_{i\in \I}$ is a limit diagram in $\C$, and consider the functor $T$ which sends an object $U$ to the set of cones $U \to X_i$. Then $L(T)$ is a limit of $X_i$. To see this, first of all for each $i$ we have a morphism $T \to \Hom({-}, X_i)$ which selects the $i$ component of the cone; this corresponds to a morphism $L(T) \to X_i$. Similarly, for each $f : i \to j$ in $\I$ we have a morphism from the $i$ component functor to the $j$ component functor, so naturality of the adjunction implies that we get the required compatibility conditions for a cone $L(T) \to X_i$. Conversely, the identity morphism $\id : L(T) \to L(T)$ corresponds to a morphism $T \to \Hom({-}, L(T))$, so for any cone $U \to X_i$ we have a corresponding element of $T(U)$, which maps to a morphism in $\Hom(U, L(T))$.' + is_equivalence: false + +- id: cocomplete_well-copowered_generator_implies_total + assumptions: + - cocomplete + - well-copowered + - generator + conclusions: + - total + proof: ... + is_equivalence: false diff --git a/databases/catdat/data/category-properties/cototal.yaml b/databases/catdat/data/category-properties/cototal.yaml new file mode 100644 index 00000000..445c5d38 --- /dev/null +++ b/databases/catdat/data/category-properties/cototal.yaml @@ -0,0 +1,11 @@ +id: cototal +relation: is +description: 'A category $\C$ is cototal when its dual category is total, i.e. it is locally essentially small and the contravariant Yoneda embedding $y : \C \to [\C^{\op}, \Set]$ has a left adjoint.' +nlab_link: https://ncatlab.org/nlab/show/total+category +dual_property: total +invariant_under_equivalences: true + +related_properties: + - cocomplete + - complete + - locally copresentable diff --git a/databases/catdat/data/category-properties/locally copresentable.yaml b/databases/catdat/data/category-properties/locally copresentable.yaml index 12563b17..27865e35 100644 --- a/databases/catdat/data/category-properties/locally copresentable.yaml +++ b/databases/catdat/data/category-properties/locally copresentable.yaml @@ -7,3 +7,4 @@ invariant_under_equivalences: true related_properties: - coaccessible - complete + - cototal diff --git a/databases/catdat/data/category-properties/locally presentable.yaml b/databases/catdat/data/category-properties/locally presentable.yaml index 53c681d2..37683d54 100644 --- a/databases/catdat/data/category-properties/locally presentable.yaml +++ b/databases/catdat/data/category-properties/locally presentable.yaml @@ -17,6 +17,7 @@ invariant_under_equivalences: true related_properties: - accessible - cocomplete + - total - locally finitely presentable - locally multi-presentable - locally poly-presentable diff --git a/databases/catdat/data/category-properties/total.yaml b/databases/catdat/data/category-properties/total.yaml new file mode 100644 index 00000000..9d3266c1 --- /dev/null +++ b/databases/catdat/data/category-properties/total.yaml @@ -0,0 +1,11 @@ +id: total +relation: is +description: 'A category $\C$ is total when it is locally essentially small and the covariant Yoneda embedding $y : \C^{\op} \to [\C, \Set]$ has a left adjoint. (For a concrete example of how this left adjoint might look, see here.)' +nlab_link: https://ncatlab.org/nlab/show/total+category +dual_property: cototal +invariant_under_equivalences: true + +related_properties: + - cocomplete + - complete + - locally presentable diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 8e906067..1900d983 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -116,6 +116,8 @@ "ℵ₂-small coproducts": true, "ℵ₂-small powers": true, "ℵ₂-small copowers": true, + "total": true, + "cototal": 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 5596e679..763b547d 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -112,6 +112,8 @@ "ℵ₂-small powers": true, "ℵ₂-small copowers": true, "pretopos": true, + "total": true, + "cototal": 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 8da72ea9..91d7b725 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -80,6 +80,8 @@ "ℵ₂-small coproducts": true, "ℵ₂-small powers": true, "ℵ₂-small copowers": true, + "total": true, + "cototal": true, "abelian": false, "additive": false,