Complete topos implies cocomplete

database/data/categories/FinSet.yaml

@@ -35,9 +35,6 @@ satisfied_properties:
   - property: extremal generator
     proof: The one-point set is an extremal generator even in <a href="/category/Set">$\Set$</a>. Now apply Lemma 10 <a href="/content/subcategories">here</a>.
 
-  - property: extremal cogenerator
-    proof: The two-element set is an extremal cogenerator even in <a href="/category/Set">$\Set$</a>. Now apply Lemma 10 <a href="/content/subcategories">here</a>.
-
   - property: semi-strongly connected
     proof: Every non-empty finite set is weakly terminal (by using constant maps).
 

database/data/categories/Z-FinSet.yaml

@@ -51,12 +51,6 @@ unsatisfied_properties:
   - property: countable
     proof: For every set $X$ this category contains the terminal object $(\{X\},\id)$.
 
-  - property: generator
-    proof: >-
-      Assume that $(G,\gamma)$ is a generator of $\IZ{-}\FinSet$. Then $G$ cannot be empty, since otherwise $\IZ{-}\FinSet$ would be thin, which is absurd. Choose an element $g \in G$. Since $\gamma$ is a permutation of a finite set, there is some $n \geq 2$ with $\gamma^n(g)=g$.
-
-      Choose a natural number $m \geq 2$ that does not divide $n$ (for example, $m=n+1$), and consider the finite set $X = \{0,1,\dotsc,m-1\}$ equipped with the permutation $\sigma$ defined by $\sigma(x) = (x+1) \bmod m$. Since $(X,\sigma)$ has a non-trivial endomorphism, for example $\sigma$, and $(G,\gamma)$ is a generator, there is a morphism $(G,\gamma) \to (X,\sigma)$. If $x \in X$ denotes the image of $g \in G$, we conclude that $\sigma^n(x)=x$. By construction of $\sigma$, this implies $m \mid n$, which contradicts our assumption on $m$.
-
   - property: cogenerator
     proof: >-
       Assume that $(Q,\rho)$ is a cogenerator of $\IZ{-}\FinSet$. Choose $k \geq 1$ with $\rho^k = \id_Q$. Now consider the finite set $X = \{0,1,\dotsc,2k-1\}$ equipped with the permutation $\sigma$ defined by $\sigma(x) = (x+1) \bmod 2k$. The object $(X,\sigma)$ has a non-trivial endomorphism $g$ defined by $g(x) = (x+k) \bmod 2k$, i.e. $g = \sigma^k$. Since $(Q,\rho)$ is a cogenerator, there is a morphism $f : (X,\sigma) \to (Q,\rho)$ with $f \circ g \neq f$. But since $f$ is a morphism, we have

database/data/category-implications/topos.yaml

@@ -36,6 +36,130 @@
     - coregular
   proof: This is proven in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant">Johnstone</a>, A2.6.3.
 
+# ---- consequences of the monadicity of the power object functor P : T^op -> T ----
+
+- id: topos_monadic_over_itself
+  assumptions:
+    - elementary topos
+    - complete
+  conclusions:
+    - cocomplete
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_powers
+  assumptions:
+    - elementary topos
+    - powers
+  conclusions:
+    - copowers
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_countable_powers
+  assumptions:
+    - elementary topos
+    - countable powers
+  conclusions:
+    - countable copowers
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_aleph2_powers
+  assumptions:
+    - elementary topos
+    - ℵ₂-small powers
+  conclusions:
+    - ℵ₂-small copowers
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_products
+  assumptions:
+    - elementary topos
+    - products
+  conclusions:
+    - coproducts
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_countable_products
+  assumptions:
+    - elementary topos
+    - countable products
+  conclusions:
+    - countable coproducts
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_aleph2_products
+  assumptions:
+    - elementary topos
+    - ℵ₂-small products
+  conclusions:
+    - ℵ₂-small coproducts
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_sequential
+  assumptions:
+    - elementary topos
+    - sequential limits
+  conclusions:
+    - sequential colimits
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_sifted
+  assumptions:
+    - elementary topos
+    - cosifted limits
+  conclusions:
+    - sifted colimits
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_filtered
+  assumptions:
+    - elementary topos
+    - cofiltered limits
+  conclusions:
+    - filtered colimits
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_aleph1_filtered
+  assumptions:
+    - elementary topos
+    - ℵ₁-cofiltered limits
+  conclusions:
+    - ℵ₁-filtered colimits
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_connected
+  assumptions:
+    - elementary topos
+    - connected limits
+  conclusions:
+    - connected colimits
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_monadic_over_itself_wide_pullbacks
+  assumptions:
+    - elementary topos
+    - wide pullbacks
+  conclusions:
+    - wide pushouts
+  proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).'
+
+- id: topos_generator_implies_cogenerator
+  assumptions:
+    - elementary topos
+    - generator
+  conclusions:
+    - cogenerator
+  proof: 'For an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is right adjoint to $P^{\op} : \T \to \T^{\op}$ and moreover is faithful. The first statement is part of the proof that $P$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 <a href="/content/subcategories">here</a>, if $G$ is a generator of $\T$, then $PG$ is a cogenerator.'
+
+- id: topos_generating_collection_implies_cogenerating_collection
+  assumptions:
+    - elementary topos
+    - generating collection
+  conclusions:
+    - cogenerating collection
+  proof: 'For an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is right adjoint to $P^{\op} : \T \to \T^{\op}$ and moreover is faithful. The first statement is part of the proof that $P$ is monadic (<a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 <a href="/content/subcategories">here</a>, if $F$ is a generating collection of $\T$, then $P_*(F)$ is a cogenerating collection.'
+
+# ---- end of consequences of the monadicity of P ----
+
 - id: grothendieck_topos_definition
   assumptions:
     - Grothendieck topos