diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 3035325aa..6e7a3ab77 100644 --- a/database/data/categories/FinSet.yaml +++ b/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 $\Set$. Now apply Lemma 10 here. - - property: extremal cogenerator - proof: The two-element set is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here. - - property: semi-strongly connected proof: Every non-empty finite set is weakly terminal (by using constant maps). diff --git a/database/data/categories/Z-FinSet.yaml b/database/data/categories/Z-FinSet.yaml index c43978841..a2921ad67 100644 --- a/database/data/categories/Z-FinSet.yaml +++ b/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 diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index 821a0cb21..728cb291f 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -36,6 +36,130 @@ - coregular proof: This is proven in Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 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 (Johnstone, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 here, 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 (Johnstone, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 here, 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