diff --git a/.cspell.json b/.cspell.json index 488347a3..02064e53 100644 --- a/.cspell.json +++ b/.cspell.json @@ -46,6 +46,7 @@ "brauer", "Bredon", "cancellative", + "Carboni", "cartesian", "Catabase", "catdat", @@ -77,6 +78,7 @@ "coequalizes", "coexact", "coexponentials", + "coextensivity", "cofiltered", "cofiltering", "cofinal", diff --git a/content/subcategories.md b/content/subcategories.md index 7cff07b2..fec810ac 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -83,7 +83,7 @@ _Proof._ The forgetful functor $\C / P \to \C$ is fully faithful; it has right a Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves pullbacks and coequalizers. If $\D$ is regular, then so is $\C$. ::: -_Proof._ Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullback in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram +_Proof._ Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullbacks in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram $$X \times_Y X \rightrightarrows X \to \im(f) \xrightarrow{i} Y$$ where $X \times_Y X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions, the image under $U$ is equivalent to the diagram in $\D$: $$UX \times_{UY} UX \rightrightarrows UX \to \im(Uf) \xrightarrow{Ui} UY$$ @@ -119,3 +119,9 @@ Any fully faithful functor reflects extremal generating sets (and therefore, by ::: _Proof:_ Under the given assumptions, we can factor $\C \to (\Set^+)^S$, $X \mapsto (\Hom_\C(G, X))_{G\in S}$, as being isomorphic to the composition of $U : \C \to D$ followed by $Y \mapsto (\Hom_\D(UG, Y))_{G\in S}$, using the assumption on $U$ to identify $\Hom_\D(UG, UX)$ with $\Hom_C(G, X)$ naturally in $X$. In this composition, the first is fully faithful and therefore also conservative; and the second is assumed to be faithful and conservative. Therefore, the composition is also faithful and conservative. $\square$ + +::: Lemma 11 +Let $U : \C \to \D$ be a faithful conservative functor (for example, a fully faithful functor). Assume that $\D$ is extensive, that $\C$ has finite coproducts and pullbacks along coproduct inclusions, and that $U$ preserves both. Then $\C$ is extensive. A similar statement holds for infinitary extensive (and countably extensive) categories, in which case we assume that $\C$ has all coproducts (resp. all countable coproducts) and that $U$ preserves these. +::: + +_Proof._ This is straight forward. We need to prove that finite coproducts are disjoint and stable under pullbacks in $\C$. If $A,B \in \C$, the coproduct inclusion $A \to A + B$ is a monomorphism: Since $U$ is faithful, it suffices to prove that its image under $U$ is a monomorphism. Since $U$ preserves finite coproducts, the image identifies with the coproduct inclusion $U(A) \to U(A) + U(B)$, which is a monomorphism since $\D$ is extensive. Moreover, the unique morphism $0 \to A \times_{A + B} B$ is an isomorphism: Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the unique morphism $0 \to U(A) \times_{U(A) + U(B)} U(B)$, which is an isomorphism since $\D$ is extensive. This proves that finite coproducts are disjoint in $\C$. To prove that they are stable under pullbacks, let $T \to A + B$ be any morphism in $\C$, and consider the pullbacks $T_A := T \times_{A + B} A$ and $T_B := T \times_{A + B} B$. We need to show that the canonical morphism $T_A + T_B \to T$ is an isomorphism. Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the canonical morphism $U(T)_{U(A)} + U(T)_{U(B)} \to U(T)$ induced by the morphism $U(T) \to U(A) + U(B)$ in $\D$, which is an isomorphism since $\D$ is extensive. $\square$ diff --git a/database/data/categories/CRing.yaml b/database/data/categories/CRing.yaml index cd2d74ed..4470485e 100644 --- a/database/data/categories/CRing.yaml +++ b/database/data/categories/CRing.yaml @@ -32,7 +32,21 @@ satisfied_properties: proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. - property: coextensive - proof: '[Sketch] A ring homomorphism $f : A \times B \to R$ yields the idempotent element $e \coloneqq f(1,0) \in R$, so that $R \cong eR \times (1-e)R$. Then $f$ decomposes into the ring homomorphisms $f_A : A \to eR$, $f_A(a) \coloneqq f(a,0)$ and $f_B : B \to (1-e)R$, $f_B(b) \coloneqq f(0,b)$.' + proof: >- + We already know that $\CRing$ has products and pushouts, since it is finitary algebraic. Concretely, the pushout of a span $A \leftarrow R \rightarrow B$ can be constructed as the tensor product $A \otimes_R B$ with the obvious multiplication. Finite products are disjoint because the projection $p_1 : A \times B \to A$ is clearly surjective, hence an epimorphism, and the tensor product $A \otimes_{p_1,A \times B,p_2} B = 0$ is the zero ring (the terminal object), since + $$a \otimes b = a \cdot p_1(1,0) \otimes b = a \otimes p_2(1,0) \cdot b = a \otimes 0 = 0.$$ + It remains to check that finite products are stable under pushouts. Let + $$f : A \times B \to T$$ + be a ring homomorphism, and consider the pushouts + $$\begin{align*} + T_A & := A \otimes_{p_1,A \times B,f} T \\ + T_B & := B \otimes_{p_2,A \times B,f} T. + \end{align*}$$ + We need to prove that the canonical homomorphism + $$T \to T_A \times T_B$$ + is an isomorphism. Since $p_1 : A \times B \to A$ is surjective with kernel $0 \times B = \langle (0,1) \rangle$, we have $T_A = T/\langle f(1,0)\rangle$, and likewise, $T_B = T/\langle f(0,1) \rangle$. The elements $f(1,0)$ and $f(0,1)$ are orthogonal idempotents in $T$. Therefore, the claim follows from the well-known result in commutative algebra that if $R$ is a commutative ring and $e \in R$ is an idempotent, then $R \to R/\langle e \rangle \times R/\langle 1-e \rangle$ is an isomorphism. One can also deduce this from the Chinese Remainder Theorem. + + An alternative proof, which we only sketch, uses the category of locally ringed spaces $\LRS$, which is infinitary extensive. It follows that the category of affine schemes is extensive by Lemma 11 here, and this category is anti-equivalent to $\CRing$. This argument is not circular since our proof of extensivity of $\LRS$ does not use coextensivity of $\CRing$. unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index ac10a69c..0ae8776a 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -27,15 +27,15 @@ satisfied_properties: - property: semi-strongly connected proof: Every non-empty category is weakly terminal (by using constant functors). - - property: infinitary extensive - proof: '[Sketch] This is straight forward from the fact that $\Set$ is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.' - - property: extremal generator proof: >- The walking morphism $I$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $I$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms. In fact, $I$ is an extremal generator: suppose $F : \C \to \D$ is a functor which induces a bijection $\Mor(\C) \to \Mor(\D)$. By considering the images of identity morphisms in $\C$, we see that $F$ is injective on objects; and then by considering the preimages of identity morphisms in $\D$, we see that $F$ is surjective on objects. By assumption, $F$ is also bijective on morphisms, so $F$ is an isomorphism of categories. + - property: infinitary extensive + proof: 'We have just seen that the walking morphism is an extremal generator, which means that the functor $\Mor : \Cat \to \Set$ is faithful and conservative. Moreover, $\Cat$ has coproducts and pullbacks, since it is locally finitely presentable. The functor $\Mor$ preserves coproducts by their concrete description and, being representable, also preserves pullbacks. Therefore, the claim follows from the extensivity of $\Set$ and Lemma 11 here.' + unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -94,7 +94,7 @@ special_objects: terminal object: description: trivial category coproducts: - description: disjoint unions + description: disjoint unions with no morphisms between objects in distinct summands products: description: direct products with pointwise operations diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index 380993bc..187dcf1c 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -53,7 +53,7 @@ satisfied_properties: with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c'' \in C$, by Urysohn''s lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c'') = 1$. Also, by Tietze''s extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c''))$, we conclude that $j(c) \ne j(c'')$. This shows that $j$ is injective, so it is a regular monomorphism.' - property: extensive - proof: This follows as for $\Top$ or $\Haus$ since finite coproducts in $\CompHaus$ are formed as disjoint union spaces with the disjoint union topology. + proof: This follows from Lemma 11 here since $\Top$ is infinitary extensive and its full subcategory $\CompHaus$ is closed under pullbacks and finite coproducts in $\Top$. - property: cofiltered-limit-stable epimorphisms proof: 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by lemma 1 here, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.' diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 193a2eb6..c9cd2cb2 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -14,7 +14,7 @@ related: - FS - Set - Set_c - - Set_f + - Set_ff satisfied_properties: - property: locally small diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index e27292b7..0ccd93d6 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -37,7 +37,7 @@ satisfied_properties: - property: regular proof: |- - This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the nLab it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup of $B$, hence free abelian, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms. + This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the nLab it suffices to prove that there are (reg epi, mono)-factorizations that are stable under pullbacks. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup of $B$, hence free abelian, and $A \to C$ is surjective. Clearly, surjective homomorphisms are stable under pullbacks. It remains to show that they coincide with the regular epimorphisms. (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\Ab$. Since $A \times_B A$ is free abelian (as a subgroup of $A \times A$), $f$ is also a coequalizer in $\FreeAb$. (2) If $f : A \to B$ is a regular epimorphism in $\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. diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 02687dc5..da67de5f 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -35,7 +35,7 @@ satisfied_properties: check_redundancy: false - property: infinitary extensive - proof: This follows exactly as for $\Top$ since Hausdorff spaces are closed under taking subspaces and coproducts in $\Top$. + proof: This follows from Lemma 11 here since $\Top$ is infinitary extensive and its full subcategory $\Haus$ is closed under pullbacks and coproducts in $\Top$. - property: well-powered proof: This is clear from the classification of monomorphisms as injective continuous maps. diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml index 65355a68..77e70a39 100644 --- a/database/data/categories/LRS_R.yaml +++ b/database/data/categories/LRS_R.yaml @@ -29,7 +29,20 @@ satisfied_properties: proof: This follows from the characterization of epimorphisms below. - property: infinitary extensive - proof: '[Sketch] Since $\Top$ is infinitary extensive, a morphism $f : Y \to \coprod_i X_i \eqqcolon X$ yields a decomposition $Y = \coprod_i Y_i$ (as topological spaces) with continuous maps $f_i : Y_i \to X_i$. Endow the open subset $Y_i \subseteq Y$ with the restricted sheaf. Then each $f_i$ becomes a morphism of locally ringed spaces, and $Y = \coprod_i Y_i$ holds as locally ringed spaces.' + proof: >- + The proof works for both ringed and locally ringed spaces and relies on the fact that $\Top$ is infinitary extensive. + + First, recall some basic facts about open embeddings (often called open immersions in the context of schemes). If $(X,\O_X)$ is a locally ringed space and $U \subseteq X$ is an open subset, then, letting $\O_U := (\O_X)|_U$, the pair $(U,\O_U)$ is again a locally ringed space. There is an inclusion morphism $(i,i^\sharp) : (U,\O_U) \to (X,\O_X)$, where $i$ is the inclusion map and $i^\sharp : \O_X \to i_* \O_U$ is defined via restriction maps. This is a monomorphism, and a morphism into $(X,\O_X)$ factors through it if and only if the image of its underlying map is contained in $U$. We will refer to any monomorphism isomorphic to one of this form as an open embedding. + + Pullbacks along open embeddings exist and are themselves open embeddings. Indeed, if $(f,f^\sharp) : (X,\O_X) \to (Y,\O_Y)$ is a morphism of locally ringed spaces and $V \subseteq Y$ is an open subset, then $f^*(V) \subseteq X$ is an open subset, and $(f^*(V),\O_{f^*(V)}) \hookrightarrow (X,\O_X)$ is the pullback of $(f,f^\sharp)$ along $(V,\O_V) \hookrightarrow (Y,\O_Y)$. + + Since $\LRS_R$ is cocomplete, coproducts exist. Concretely, the coproduct of a family of locally ringed spaces $(X_i,\O_{X_i})$ is the locally ringed space $(X,\O_X)$, where $X := \coprod_i X_i$ and $\O_X(U) := \prod_i \O_{X_i}(U \cap X_i)$. Notice that the coproduct inclusions are open embeddings. Hence, pullbacks along coproduct inclusions exist. + + That coproducts are disjoint in $\LRS_R$ follows from the corresponding property of $\Top$ together with the following observations. By the descriptions above, the forgetful functor $\LRS_R \to \Top$ preserves coproducts and pullbacks along open embeddings (although it does not preserve pullbacks in general), and the empty topological space admits a unique structure sheaf, up to isomorphism, making it into a locally ringed space. + + It remains to prove that coproducts are stable under pullbacks. To this end, let $(f,f^\sharp) : (T,\O_T) \to \coprod_i (X_i,\O_{X_i})$ be a morphism. Then $T_i := f^*(X_i) \subseteq T$ is an open subset, and for $i \neq j$ we have $T_i \cap T_j = \varnothing$ because $X_i \cap X_j = \varnothing$ in the coproduct. We must show that the canonical morphism $(g,g^\sharp) : \coprod_i (T_i,\O_{T_i}) \to (T,\O_T)$ is an isomorphism. The underlying continuous map $g$ is a homeomorphism because coproducts in $\Top$ are stable under pullbacks. It therefore remains to show that $g^\sharp : \O_T \to g_* \O$, where $\O$ denotes the structure sheaf of the coproduct, is an isomorphism. Equivalently, for every open subset $U \subseteq T$, we must show that the canonical ring homomorphism + $$\textstyle \O_T(U) \to \prod_{i \in I} \O_{T_i}(U \cap T_i) = \prod_{i \in I} \O_T(U \cap T_i)$$ + is an isomorphism. This is precisely the sheaf axiom applied to the open cover of $U$ by the pairwise disjoint open subsets $U \cap T_i$. unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index 5e4eeacd..7f9f6c25 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -19,6 +19,7 @@ satisfied_properties: proof: There is a forgetful functor $\Man \to \Set$ and $\Set$ is locally small. - property: finite products + # TODO: give a reference or explain this in more detail proof: In short, this follows from the corresponding statement for topological spaces and $\IR^n \times \IR^m \cong \IR^{n+m}$. check_redundancy: false @@ -28,12 +29,12 @@ satisfied_properties: - property: essentially small proof: 'This is a consequence of the Whitney embedding theorem. But there is also a more direct proof: Since a manifold is second-countable, it is Lindelöf (proof). In particular, there is a countable atlas. It is then completely determined by countable many open subsets of Euclidean spaces and the transition maps.' - - property: extensive - proof: '[Sketch] Since $\Top$ is infinitary extensive, a continuous map $f : M \to \coprod_i N_i$ corresponds to a decomposition $M = \coprod_i M_i$ (as topological spaces) with continuous maps $f_i : M_i \to N_i$. Endow the open subset $M_i \subseteq M$ with the smooth structure inherited from $M$. Now remark that $f$ is smooth iff each $f_i$ is smooth.' + - property: countable coproducts + proof: Take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) + check_redundancy: false - - property: countably distributive - # TODO: maybe add "countably extensive" to make this more conceptual - proof: To construct countable coproducts, take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) Now we need to check that the canonical smooth map $\coprod_i X \times Y_i \to X \times \coprod_i Y_i$ is a diffeomorphism (for countable families). It is a homeomorphism since $\Top$ is infinitary distributive. The inverse $X \times \coprod_i Y_i \to \coprod_i X \times Y_i$ is smooth since the domain is covered by the open subsets $X \times Y_i$ on which the map is clearly smooth. + - property: countably extensive + proof: 'This can be deduced from the countable extensivity of $\Top$ as follows. We already know that countable coproducts exist, and these are preserved by the forgetful functor to $\Top$. Since open embeddings pull back to open embeddings, and an open subset of a manifold carries a canonical manifold structure, it follows that $\Man$ has pullbacks along coproduct inclusions, and that the forgetful functor to $\Top$ preserves them. Since coproducts are disjoint in $\Top$ and the empty space has a unique manifold structure, it follows immediately that countable coproducts are also disjoint in $\Man$. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a countable family of manifolds, and let $f : T \to \coprod_{i \in I} X_i$ be a smooth map. Consider the pullbacks $T_i := f^*(X_i)$. These are precisely the preimages of the $X_i$ under $f$ and are open subsets of $T$. Since coproducts in $\Top$ are stable under pullbacks, the canonical smooth map $\coprod_{i \in I} T_i \to T$ is a homeomorphism. It is also a local diffeomorphism, since each $T_i \to T$ is an open embedding. Therefore, it is a diffeomorphism.' - property: Cauchy complete proof: See Theorem 2.1 at the nLab. diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index aa3256ba..045d1a7b 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -3,7 +3,7 @@ name: category of measurable spaces notation: $\Meas$ objects: measurable spaces morphisms: measurable maps -description: This is very similar to the category of topological spaces. Accordingly, limits and colimits can be constructed in the same way. +description: This category is similar to the category of topological spaces. For instance, limits and colimits can be constructed in the same way. However, a main difference is that this category is not infinitary distributive. nlab_link: https://ncatlab.org/nlab/show/Meas tags: @@ -37,8 +37,13 @@ satisfied_properties: - 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. - - 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.' + - property: countably extensive + proof: >- + This follows from the countable extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and that they are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets, with measurable subsets given by unions of measurable subsets of the summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique $\sigma$-algebra, it follows immediately that coproducts are disjoint in $\Meas$ as well. + + It remains to show that countable coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a countable family of measurable spaces and let $f : T \to \coprod_{i \in I} X_i$ be a measurable map. Consider the pullbacks $T_i := f^*(X_i)$. These are simply the preimages of $X_i$ under $f$, equipped with the $\sigma$-algebra induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical measurable map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it maps measurable sets to measurable sets. + + A measurable subset of $\coprod_{i \in I} T_i$ has the form $A = \coprod_{i \in I} (B_i \cap T_i)$, where each $B_i$ is a measurable subset of $T$. The image of $A$ in $T$ is $\bigcup_{i \in I} (B_i \cap T_i)$. Since this is a countable union, it suffices to show that each $B_i \cap T_i$ is measurable in $T$. This holds because $T_i$ is measurable in $T$ (since $X_i$ is measurable in the coproduct and $f$ is measurable) and $B_i$ is measurable in $T$ by assumption. - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. @@ -80,6 +85,18 @@ unsatisfied_properties: $$\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$$ for each $G \in S$, implying that $S$ cannot be an extremal generating set. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that $f$ factors through $(\kappa + 1, \M_\kappa')$. + - property: infinitary distributive + proof: >- + Let $X$ be a set of cardinality $> 2^{\aleph_0}$. We equip $X$ with the discrete $\sigma$-algebra. If $1$ denotes the singleton space, we therefore have $X \cong \coprod_{x \in X} 1$ in $\Meas$. However, we claim that the canonical bijective measurable map + $$\textstyle\coprod_{x,y \in X} 1 \to X \times X$$ + is not an isomorphism, i.e. that $X \times X$ does not carry the discrete $\sigma$-algebra. More precisely, we will show that the diagonal $\Delta \subseteq X \times X$ is not measurable. (This is probably standard, but we include the proof here for lack of a reference.) + + Assume that $\Delta \subseteq X \times X$ is measurable. Then (cf. MSE/61617) there is a countable family of rectangles $(A_n \times B_n)_{n \in \IN}$ such that $\Delta \in \sigma(\{A_n \times B_n : n \in \IN\})$. Consider the product of the characteristic functions + $$((\chi_{A_n})_n,(\chi_{B_n})_n) : X \to \{0,1\}^{\IN} \times \{0,1\}^{\IN}.$$ + Its kernel is an equivalence relation $\sim$ on $X$, namely, $x \sim y$ if and only if, for all $n$, we have $x \in A_n \iff y \in A_n$ and $x \in B_n \iff y \in B_n$. The set $X/{\sim}$ of equivalence classes embeds into $\{0,1\}^{\IN} \times \{0,1\}^{\IN}$ and therefore has at most $2^{\aleph_0}$ elements. By our assumption on $X$, the projection $X \to X/{\sim}$ cannot be injective. Thus, $\sim$ is not trivial. + + Next, consider the collection of all subsets $E \subseteq X \times X$ with the property that, whenever $x \sim y$, we have $(x,y) \in E \iff (x,x) \in E$. It is easily seen that this collection is a $\sigma$-algebra on $X \times X$. Moreover, it contains each rectangle $A_n \times B_n$. Therefore, it also contains the diagonal $\Delta$. But this means that $x \sim y$ implies $x=y$, i.e. that $\sim$ is trivial. This contradiction proves that the diagonal is not measurable. + special_objects: initial object: description: empty set with the unique $\sigma$-algebra diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index ac174589..4b457140 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -39,7 +39,7 @@ satisfied_properties: proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' - property: infinitary extensive - proof: This follows from the existence of coproducts and finite products, and from the fact that $\Top$ is infinitary extensive. + proof: This follows from Lemma 11 here since $\Top$ is infinitary extensive and its full subcategory $\Met_c$ of metrizable topological spaces is closed under pullbacks and coproducts in $\Top$. - property: effective cocongruences proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By MO/509548, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful and therefore reflects colimits, we conclude that $E$ is effective in $\Met_c$.' diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index af097ab0..10a7611a 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -27,7 +27,7 @@ satisfied_properties: proof: We can use the same proof as for $\Met$ since the equation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ also holds for for $r, s_i \in \IR \cup \{\infty\}$. - 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 $Y_i$ with the restricted metric. If $f$ is non-expansive, each $f_i$ is non-expansive, and for $x_i \in Y_i$ and $i \neq j$ we have $d_Y(x_i,x_j) \geq d_X(f(x_i),f(x_j)) = \infty$, so that $Y = \coprod_i Y_i$ holds as metric spaces.' + proof: 'This can be deduced from the infinitary extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets equipped with the metric that extends the given metrics and assigns distance $\infty$ to points in different summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique metric, it follows immediately that coproducts are disjoint in $\Met_\infty$ as well. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a family of metric spaces and let $f : T \to \coprod_{i \in I} X_i$ be a non-expansive map. Consider the pullbacks $T_i := f^*(X_i)$. These are just the preimages of $X_i$ under $f$, with the metric induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical non-expansive map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is isometric. Since each $T_i \to T$ is isometric, it suffices to prove that for $a \in T_i$ and $b \in T_j$, where $i \neq j$, we have $d_T(a,b) = \infty$. Indeed, since $f(a) \in X_i$ and $f(b) \in X_j$, we have $\infty = d_{\coprod_i X_i}(f(a),f(b)) \leq d_T(a,b)$.' - property: extremal generator proof: A similar proof to the one for $\Met$ shows that $[0, \infty]$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$, is an extremal generator for $\Met_{\infty}$. diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml index ccff1fea..c5d730c8 100644 --- a/database/data/categories/Mon.yaml +++ b/database/data/categories/Mon.yaml @@ -53,7 +53,7 @@ unsatisfied_properties: proof: If $M \to N$ is an epimorphism in $\Mon$ and $M$ is infinite, then $\card(N) \leq \card(M)$ (see MO/510431). This implies that in $\Mon$ the canonical homomorphism $\coprod_{n \geq 0} \IN \to \prod_{n \geq 0} \IN$ is not an epimorphism because its domain is countable and its codomain is uncountable. - property: coregular - proof: 'Consider the monoid $M \coloneqq \langle x_0, x_1, s : x_0 s = x_1 s = 1 \rangle$. Notice that every element in $M$ has a unique expression as $s^k \cdot u$ with $k \in \IN$ and $u \in \langle x_0,x_1 \rangle_M$. Moreover, the canonical homomorphism $\iota : \langle x_0, x_1 \rangle \to M$ (from the free monoid) is injective. We will prove that it is a regular monomorphism, which however is not pushout-stable. Consider $N \coloneqq \langle x_0, x_1, s_0, s_1 : x_i s_j = 1 \rangle$ and define $f_i : M \to N$ for $i=0,1$ by $f_i(x_j) = x_j$ and $f_i(s) = s_i$. Then $\iota$ is the equalizer of $f_0,f_1$. Now consider $g : \langle x_0,x_1 \rangle \to \langle y_0 \rangle$ defined by $g(x_0) = y_0$, $g(x_1) = 1$. The pushout of $\iota$ with $g$ is given by $\langle x_0, x_1, s, y_0 : x_0 s = x_1 s = 1 , \, x_0 = y_0, \, x_1 = 1 \rangle$, which simplifies to $\langle x_0, s : x_0 s = s = 1 \rangle$, which is trivial.' + proof: 'Consider the monoid $M \coloneqq \langle x_0, x_1, s : x_0 s = x_1 s = 1 \rangle$. Notice that every element in $M$ has a unique expression as $s^k \cdot u$ with $k \in \IN$ and $u \in \langle x_0,x_1 \rangle_M$. Moreover, the canonical homomorphism $\iota : \langle x_0, x_1 \rangle \to M$ (from the free monoid) is injective. We will prove that it is a regular monomorphism, which however is not stable under pushouts. Consider $N \coloneqq \langle x_0, x_1, s_0, s_1 : x_i s_j = 1 \rangle$ and define $f_i : M \to N$ for $i=0,1$ by $f_i(x_j) = x_j$ and $f_i(s) = s_i$. Then $\iota$ is the equalizer of $f_0,f_1$. Now consider $g : \langle x_0,x_1 \rangle \to \langle y_0 \rangle$ defined by $g(x_0) = y_0$, $g(x_1) = 1$. The pushout of $\iota$ with $g$ is given by $\langle x_0, x_1, s, y_0 : x_0 s = x_1 s = 1 , \, x_0 = y_0, \, x_1 = 1 \rangle$, which simplifies to $\langle x_0, s : x_0 s = s = 1 \rangle$, which is trivial.' - property: regular subobject classifier proof: 'Assume that $\Omega$ is a regular subobject classifier. Since the trivial monoid is a zero object, every regular submonoid $U \subseteq M$ of any monoid $M$ would have the form $\{m \in M : h(m) = 1 \}$ for some homomorphism $M \to \Omega$. Now take any monoid $M$ with zero that has two different homomorphisms with zero $f,g : M \rightrightarrows N$ (for example, let $M = N = \{0\} \cup \{x^n : n \geq 0\}$ be the free monoid with zero on one generator, $f(x) = 0$,and $g(x) = x$). Take their equalizer $U \subseteq M$, and choose a homomorphism $h : M \to \Omega$ with $U = \{m \in M : h(m) = 1\}$. Since $0 \in U$, we have $h(0)=1$. But then for all $m \in M$ we have $h(m) = h(m) h(0) = h(m 0) = h(0) = 1$, i.e. $U = M$, which yields the contradiction $f = g$.' diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index cf87efac..90fe7af4 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -28,7 +28,7 @@ satisfied_properties: proof: Every non-empty poset is weakly terminal (by using constant maps). - property: infinitary extensive - proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as posets, and each $f_i$ is order-preserving.' + proof: This follows from Lemma 11 here since $\PreOrd$ is infinitary extensive and its full subcategory $\Pos$ is closed under pullbacks and coproducts in $\PreOrd$. - property: coregular proof: See MSE/5130295. diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 7799b52b..985cfaa8 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -27,7 +27,7 @@ satisfied_properties: proof: Every non-empty preordered set is weakly terminal (by using constant maps). - property: infinitary extensive - proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as preordered sets, and each $f_i$ is order-preserving.' + proof: 'This can be deduced from the infinitary extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets equipped with the evident partial order that leaves the distinct summands incomparable. Since coproducts are disjoint in $\Set$ and the empty set has a unique preorder, it follows immediately that coproducts are disjoint in $\PreOrd$ as well. It remains to show that coproducts are stable under pullbacks. Let $(P_i)_{i \in I}$ be a family of preordered sets and let $f : T \to \coprod_{i \in I} P_i$ be an order-preserving map. Consider the pullbacks $T_i := f^*(P_i)$. These are just the preimages of $P_i$ under $f$, with the partial order induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical order-preserving map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is order-reflecting. Since each $T_i \to T$ is order-reflecting, this amounts to proving that, for $x \in T_i$ and $y \in T_j$ with $i \neq j$, we never have $x \leq y$ in $T$. But such a relation would imply $f(x) \leq f(y)$ in $\coprod_{i \in I} P_i$, where $f(x) \in P_i$ and $f(y) \in P_j$, which contradicts the concrete description of the coproduct.' - property: coregular proof: See MSE/5130295. diff --git a/database/data/categories/Sch_R.yaml b/database/data/categories/Sch_R.yaml index 7269a7dd..cc842277 100644 --- a/database/data/categories/Sch_R.yaml +++ b/database/data/categories/Sch_R.yaml @@ -26,13 +26,13 @@ satisfied_properties: proof: The scheme $\Spec(R)$ is terminal. - property: pullbacks - proof: This is the well-known construction of the fiber product of schemes, see e.g. EGA I, Chap. I, Thm. 3.2.1. + proof: This is the well-known construction of the fiber product of schemes, see e.g. EGA I, Chap. I, Thm. 3.2.1. Alternatively, one can show that $\Sch_R$ is closed under pullbacks in the category $\LRS_R$, which has pullbacks. - property: well-powered proof: See MO/160681. - property: infinitary extensive - proof: One uses the same proof as for locally ringed spaces, using that open subspaces of schemes are also schemes. + proof: This follows from Lemma 11 here since $\LRS_R$ is infinitary extensive and its full subcategory $\Sch_R$ is closed under pullbacks and coproducts in $\LRS_R$. unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 32ac39f3..1368ab0c 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -14,7 +14,7 @@ related: - FinSet - Set_* - Set_c - - Set_f + - Set_ff - SetxSet - Setne - Set_arrow diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index 68501ef3..51cac78e 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -41,20 +41,17 @@ satisfied_properties: - property: semi-strongly connected proof: This is because the larger category $\Set$ has this property. - - property: extensive - proof: The same proof as for $\Set$ applies. Actually, the category is "countably extensive". - - - property: countably distributive - proof: By elementary set theory, a countable (disjoint) union of countable sets is again countable. Hence, countable coproducts exist in $\Set_\c$, and we already saw that finite products exist. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts. + - property: countably extensive + proof: This follows from Lemma 11 here since $\Set$ is countably extensive (even infinitary extensive) and its full subcategory $\Set_\c$ is closed under pullbacks and countable coproducts in $\Set$. - property: effective congruences proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.' - property: regular - proof: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. + proof: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullbacks since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. - property: coregular - proof: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushout since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide. + proof: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushouts since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide. unsatisfied_properties: - property: small diff --git a/database/data/categories/Set_f.yaml b/database/data/categories/Set_f.yaml deleted file mode 100644 index 3e709a78..00000000 --- a/database/data/categories/Set_f.yaml +++ /dev/null @@ -1,96 +0,0 @@ -id: Set_f -name: category of sets with finite-to-one maps -notation: $\Set_\f$ -objects: sets -morphisms: 'maps $f : X \to Y$ with the property that for every $y \in Y$ the fiber $f^*(\{y\})$ is a finite set' -description: In this variant of $\Set$ we only consider maps with finite fibers, which are commonly called finite-to-one. Equivalently, every preimage of a finite set is again finite, and this description makes it obvious that composition is well-defined. -nlab_link: null - -tags: - - set theory - -related: - - FinSet - - Set - -satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\Set_\f \to \Set$ and $\Set$ is locally small. - - - property: extremal generator - proof: The singleton set (which is not terminal) is an extremal generator as it represents the forgetful functor $\Set_\f \to \Set$ which is faithful and conservative. - - - property: semi-strongly connected - proof: From set theory it is known that for all sets $X,Y$ there is an injective map $X \to Y$ or an injective map $Y \to X$, and injective maps are finite-to-one. - - - property: extensive - proof: 'We first show that finite coproducts exist. The empty set is clearly initial. The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite. Hence, finite coproducts exist. A map $A \to X + Y$ yields a decomposition $A = A_X + A_Y$ with maps $A_X \to X$, $A_Y \to Y$ (since $\Set$ is extensive). Here, $A \to X + Y$ is finite-to-one iff $A_X \to X$ and $A_Y \to Y$ are finite-to-one.' - - - property: equalizers - proof: 'Equalizers can be constructed as in $\Set$ because of the following trivial observation: if $f : X \to Y$ is a finite-to-one map and $E \subseteq Y$ is a subset with $f(X) \subseteq E$, then the induced map $f^E : X \to E$ is also finite-to-one.' - - - property: epi-regular - proof: 'If $f : X \to Y$ is an epimorphism in $\Set_\f$, i.e. a surjective finite-to-one map, it is a coequalizer of the two maps $p_1, p_2 : X \times_Y Y \rightrightarrows Y$ in $\Set$. These maps are finite-to-one since $p_i^*(\{y\}) \cong f^*(\{y\})$ for $i=1,2$, and their coequalizer is also $f$ in $\Set_\f$: It suffices to observe that if $h : Y \to T$ is a map such that $h \circ f$ is finite-to-one, then $h$ is finite-to-one as well. In fact, surjectivity of $f$ implies $h^*(\{t\}) = f_*((h \circ f)^*(\{t\}))$ for $t \in T$.' - - - property: well-copowered - proof: This is clear since the epimorphisms are surjective. - - - property: quotients of congruences - proof: 'A congruence on a set $X$ in $\Set_\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 $\Set_\f$.' - - - property: effective congruences - proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\f$. From the proof on quotients of congruences in $\Set_\f$, we have a quotient map $p : X \to X/E$ in $\Set_\f$, and $E$ is the kernel pair of $p$ in $\Set$. It remains to see that $E$ is also the kernel pair of $p$ in $\Set_f$. Thus, suppose we have $x_1, x_2 : T \rightrightarrows X$ with $p \circ x_1 = p \circ x_2$. Then there is a unique $e : T \to E$ in $\Set$ with $x_1 = f\circ e$ and $x_2 = g\circ e$. Since $f\circ e$ is finite-to-one, we must have $e$ is finite-to-one as well.' - - - property: effective cocongruences - proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' - - - property: locally cartesian closed - proof: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\f / X \simeq \FinSet^X$. This category is cartesian closed since $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. - - - property: ℵ₁-accessible - proof: 'We first show that $\aleph_1$-directed colimits exist and are preserved by the forgetful functor to $\Set$. Let $(X_i)_{i \in I}$ be a diagram in $\Set_\f$ indexed by a $\aleph_1$-directed poset $I$. Let $(u_i : X_i \to X)$ be the colimit in $\Set$. Each map $u_i$ is finite-to-one: Otherwise, some fiber $u_i^*(\{x\}) \subseteq X_i$ contains infinitely many elements $a_1,a_2,\dotsc$. For every $n \geq 1$ we find $i_n \geq i$ such that $a_1,a_n$ have the same image in $X_{i_n}$. Let $i_\infty \in I$ be an upper bound of all $i_n$. Then all $a_n$ have the same image in $X_{i_\infty}$. This is a contradiction since $X_i \to X_{i_\infty}$ is finite-to-one. Now if $f : X \to Y$ is a map such that each $f \circ u_i$ is finite-to-one, then $f$ is finite-to-one as well: If a fiber $f^*(\{y\})$ contains infinitely many distinct elements $x_1,x_2,\dotsc$, there is some index $i$ such that all have a preimage in $X_i$, but then $(f \circ u_i)^*(\{y\})$ would be infinite. This concludes the proof that $\aleph_1$-directed colimits exist. In $\Set$, every set $X$ is the $\aleph_1$-directed colimit of its countable subsets. This remains true in $\Set_\f$ because a map $X \to Y$ is finite-to-one as long as each restriction to a countable subset of $X$ is finite-to-one. Moreover, every countable set is $\aleph_1$-presentable in $\Set$, but also in $\Set_\f$.' - - - property: ℵ₁-cofiltered limits - proof: 'We derive this from the fact that $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$. Let $D : \I \to \Set_\f$ be an $\aleph_1$-cofiltered diagram. Let $(p_i : L \to D(i))_{i \in \I}$ be the limit cone in $\Set$. Each $p_i$ is finite-to-one, because the fiber over $d \in D(i)$ is the limit of the $\aleph_1$-cofiltered diagram $\tilde{D} : I/i \to \FinSet$ which maps $j \to i$ to $D(j \to i)^*(\{d\})$. To verify the universal property, let $(f_i : T \to D(i))_{i \in \I}$ be a cone in $\Set_\f$. There is a unique map $f : T \to L$ such that $p_i f = f_i$ for every $i \in \I$, and it remains to prove that $f$ is finite-to-one. Choose any $i \in \I$. Then for every $x \in L$ we have $f^*(\{x\}) \subseteq f_i^*(\{p_i(x)\})$, and the latter set is finite.' - -unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: locally finite - proof: If $X$ is an infinite set, there are infinitely many maps $1 \to X$. They are injective and hence finite-to-one. - - - property: strongly connected - proof: Already $\Set$ is not strongly connected. - - - property: binary powers - proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\f$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetry, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' - - - property: countable copowers - proof: 'Assume that the copower $X \coloneqq \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' - - - property: filtered - proof: 'Consider the maps $f,g : \IN \rightrightarrows \IN$ defined by $f(x)=x$ and $g(x)=2x$. They are injective, hence finite-to-one. If a map $h : \IN \to X$ coequalizes them, we have $h(x)=h(2x)$, in particular $h(1)=h(2^n)$ for all $n \in \IN$. Thus, $h$ is not finite-to-one.' - - - property: sequential limits - proof: Consider the set $[n] \coloneqq \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\f$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$. - - - property: cogenerating set - proof: 'Suppose that $S$ is a set of objects of $\Set_\f$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$ giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : 1 \rightrightarrows \kappa$.' - -special_objects: - initial object: - description: empty set - coproducts: - description: '[finite case] disjoint union' - -special_morphisms: - isomorphisms: - description: bijective maps - proof: This is easy. - monomorphisms: - description: injective maps - proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the singleton), hence preserves monomorphisms. - epimorphisms: - description: surjective maps with finite fibers - proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml new file mode 100644 index 00000000..3163cb59 --- /dev/null +++ b/database/data/categories/Set_ff.yaml @@ -0,0 +1,100 @@ +id: Set_ff +name: category of sets with finite-to-one maps +notation: $\Set_\ff$ +objects: sets +morphisms: 'maps $f : X \to Y$ with the property that for every $y \in Y$ the fiber $f^*(\{y\})$ is a finite set' +description: In this variant of $\Set$ we only consider maps with finite fibers, which are commonly called finite-to-one. Equivalently, every preimage of a finite set is again finite, and this description makes it obvious that composition is well-defined. +nlab_link: null + +tags: + - set theory + +related: + - FinSet + - Set + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\Set_\ff \to \Set$ and $\Set$ is locally small. + + - property: extremal generator + proof: The singleton set (which is not terminal) is an extremal generator as it represents the forgetful functor $\Set_\ff \to \Set$ which is faithful and conservative. + + - property: semi-strongly connected + proof: From set theory it is known that for all sets $X,Y$ there is an injective map $X \to Y$ or an injective map $Y \to X$, and injective maps are finite-to-one. + + - property: equalizers + proof: 'Equalizers can be constructed as in $\Set$ because of the following trivial observation: if $f : X \to Y$ is a finite-to-one map and $E \subseteq Y$ is a subset with $f(X) \subseteq E$, then the induced map $f^E : X \to E$ is also finite-to-one.' + + - property: locally cartesian closed + proof: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\ff / X \simeq \FinSet^X$. This category is cartesian closed since $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. + + - property: finite coproducts + proof: 'The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite.' + check_redundancy: false + + - property: extensive + proof: We have already seen that finite coproducts exist in $\Set_\ff$, and pullbacks exist since the category is locally cartesian closed, although a direct argument is also possible. The forgetful functor $\Set_\ff \to \Set$ preserves finite coproducts and pullbacks, and is clearly faithful and conservative (but not full). Therefore, the claim follows from the extensivity of $\Set$ and Lemma 11 here. + + - property: epi-regular + proof: 'If $f : X \to Y$ is an epimorphism in $\Set_\ff$, i.e. a surjective finite-to-one map, it is a coequalizer of the two maps $p_1, p_2 : X \times_Y Y \rightrightarrows Y$ in $\Set$. These maps are finite-to-one since $p_i^*(\{y\}) \cong f^*(\{y\})$ for $i=1,2$, and their coequalizer is also $f$ in $\Set_\ff$: It suffices to observe that if $h : Y \to T$ is a map such that $h \circ f$ is finite-to-one, then $h$ is finite-to-one as well. In fact, surjectivity of $f$ implies $h^*(\{t\}) = f_*((h \circ f)^*(\{t\}))$ for $t \in T$.' + + - property: well-copowered + proof: This is clear since the epimorphisms are surjective. + + - property: quotients of congruences + proof: 'A congruence on a set $X$ in $\Set_\ff$ 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 $\Set_\ff$.' + + - property: effective congruences + proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\ff$. From the proof on quotients of congruences in $\Set_\ff$, we have a quotient map $p : X \to X/E$ in $\Set_\ff$, and $E$ is the kernel pair of $p$ in $\Set$. It remains to see that $E$ is also the kernel pair of $p$ in $\Set_\ff$. Thus, suppose we have $x_1, x_2 : T \rightrightarrows X$ with $p \circ x_1 = p \circ x_2$. Then there is a unique $e : T \to E$ in $\Set$ with $x_1 = f\circ e$ and $x_2 = g\circ e$. Since $f\circ e$ is finite-to-one, we must have $e$ is finite-to-one as well.' + + - property: effective cocongruences + proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_\ff$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\ff$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' + + - property: ℵ₁-accessible + proof: 'We first show that $\aleph_1$-directed colimits exist and are preserved by the forgetful functor to $\Set$. Let $(X_i)_{i \in I}$ be a diagram in $\Set_\ff$ indexed by a $\aleph_1$-directed poset $I$. Let $(u_i : X_i \to X)$ be the colimit in $\Set$. Each map $u_i$ is finite-to-one: Otherwise, some fiber $u_i^*(\{x\}) \subseteq X_i$ contains infinitely many elements $a_1,a_2,\dotsc$. For every $n \geq 1$ we find $i_n \geq i$ such that $a_1,a_n$ have the same image in $X_{i_n}$. Let $i_\infty \in I$ be an upper bound of all $i_n$. Then all $a_n$ have the same image in $X_{i_\infty}$. This is a contradiction since $X_i \to X_{i_\infty}$ is finite-to-one. Now if $f : X \to Y$ is a map such that each $f \circ u_i$ is finite-to-one, then $f$ is finite-to-one as well: If a fiber $f^*(\{y\})$ contains infinitely many distinct elements $x_1,x_2,\dotsc$, there is some index $i$ such that all have a preimage in $X_i$, but then $(f \circ u_i)^*(\{y\})$ would be infinite. This concludes the proof that $\aleph_1$-directed colimits exist. In $\Set$, every set $X$ is the $\aleph_1$-directed colimit of its countable subsets. This remains true in $\Set_\ff$ because a map $X \to Y$ is finite-to-one as long as each restriction to a countable subset of $X$ is finite-to-one. Moreover, every countable set is $\aleph_1$-presentable in $\Set$, but also in $\Set_\ff$.' + + - property: ℵ₁-cofiltered limits + proof: 'We derive this from the fact that $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$. Let $D : \I \to \Set_\ff$ be an $\aleph_1$-cofiltered diagram. Let $(p_i : L \to D(i))_{i \in \I}$ be the limit cone in $\Set$. Each $p_i$ is finite-to-one, because the fiber over $d \in D(i)$ is the limit of the $\aleph_1$-cofiltered diagram $\tilde{D} : I/i \to \FinSet$ which maps $j \to i$ to $D(j \to i)^*(\{d\})$. To verify the universal property, let $(f_i : T \to D(i))_{i \in \I}$ be a cone in $\Set_\ff$. There is a unique map $f : T \to L$ such that $p_i f = f_i$ for every $i \in \I$, and it remains to prove that $f$ is finite-to-one. Choose any $i \in \I$. Then for every $x \in L$ we have $f^*(\{x\}) \subseteq f_i^*(\{p_i(x)\})$, and the latter set is finite.' + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: locally finite + proof: If $X$ is an infinite set, there are infinitely many maps $1 \to X$. They are injective and hence finite-to-one. + + - property: strongly connected + proof: Already $\Set$ is not strongly connected. + + - property: binary powers + proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\ff$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetry, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' + + - property: countable copowers + proof: 'Assume that the copower $X \coloneqq \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' + + - property: filtered + proof: 'Consider the maps $f,g : \IN \rightrightarrows \IN$ defined by $f(x)=x$ and $g(x)=2x$. They are injective, hence finite-to-one. If a map $h : \IN \to X$ coequalizes them, we have $h(x)=h(2x)$, in particular $h(1)=h(2^n)$ for all $n \in \IN$. Thus, $h$ is not finite-to-one.' + + - property: sequential limits + proof: Consider the set $[n] \coloneqq \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\ff$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$. + + - property: cogenerating set + proof: 'Suppose that $S$ is a set of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$ giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : 1 \rightrightarrows \kappa$.' + +special_objects: + initial object: + description: empty set + coproducts: + description: '[finite case] disjoint union' + +special_morphisms: + isomorphisms: + description: bijective maps + proof: This is easy. + monomorphisms: + description: injective maps + proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the singleton), hence preserves monomorphisms. + epimorphisms: + description: surjective maps with finite fibers + proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.' diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index a48168fe..010e2fbc 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -39,7 +39,7 @@ satisfied_properties: proof: The one-point space is a generator since it represents the forgetful functor $\Top \to \Set$. - property: infinitary extensive - proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the subspace topology. If $f$ is continuous, each $Y_i = f^*(X_i)$ is open in $Y$, so that $Y = \coprod_i Y_i$ holds as topological spaces, and each $f_i$ is continuous.' + proof: 'This can be deduced from the infinitary extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets whose open subsets are unions of open subsets of the summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique topology, it follows immediately that coproducts are disjoint in $\Top$ as well. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a family of topological spaces and let $f : T \to \coprod_{i \in I} X_i$ be a continuous map. Consider the pullbacks $T_i := f^*(X_i)$. These are just the preimages of $X_i$ under $f$, with the topology induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical continuous map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is an open map. By the concrete description of open subsets in the disjoint union, it suffices to prove that each $T_i \to T$ is an open map. But this is the inclusion of a subspace, which is open since $X_i$ is open in $\coprod_{i \in I} X_i$.' - property: regular subobject classifier proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$. diff --git a/database/data/category-implications/additive.yaml b/database/data/category-implications/additive.yaml index df5ceafc..136b5e40 100644 --- a/database/data/category-implications/additive.yaml +++ b/database/data/category-implications/additive.yaml @@ -52,7 +52,7 @@ - abelian conclusions: - regular - proof: In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see Mac Lane, Ch. VIII. + proof: In an abelian category, every epimorphism is regular, and epimorphisms are stable under pullbacks, see Mac Lane, Ch. VIII. is_equivalence: false - id: grothendieck_abelian_definition diff --git a/database/data/category-implications/distributivity.yaml b/database/data/category-implications/distributivity.yaml index a2303dee..bbba6a4e 100644 --- a/database/data/category-implications/distributivity.yaml +++ b/database/data/category-implications/distributivity.yaml @@ -48,7 +48,7 @@ - distributive conclusions: - strict initial object - proof: See the nLab or Prop. 3.4 in Introduction to extensive and distributive categories. + proof: See the nLab or Prop. 3.4 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. is_equivalence: false - id: distributive_criterion diff --git a/database/data/category-implications/extensive.yaml b/database/data/category-implications/extensive.yaml index 96e12333..d44b6b32 100644 --- a/database/data/category-implications/extensive.yaml +++ b/database/data/category-implications/extensive.yaml @@ -8,6 +8,14 @@ proof: This holds by definition. is_equivalence: false +- id: countably_extensive_assumption + assumptions: + - countably extensive + conclusions: + - countable coproducts + proof: This holds by definition. + is_equivalence: false + - id: infinitary_extensive_assumption assumptions: - infinitary extensive @@ -16,9 +24,17 @@ proof: This holds by definition. is_equivalence: false -- id: infinitary_extensive_finitary +- id: infinitary_extensive_countable assumptions: - infinitary extensive + conclusions: + - countably extensive + proof: This is obvious. + is_equivalence: false + +- id: countably_extensive_finitary + assumptions: + - countably extensive conclusions: - extensive proof: This is obvious. @@ -30,7 +46,7 @@ conclusions: - disjoint finite coproducts - strict initial object - proof: These are Prop. 2.6 and 2.8 in Introduction to extensive and distributive categories. + proof: These are Prop. 2.6 and 2.8 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. is_equivalence: false - id: extensive_distributivity @@ -39,7 +55,7 @@ - finite products conclusions: - distributive - proof: This is Prop. 4.5 in Introduction to extensive and distributive categories. + proof: This is Prop. 4.5 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. is_equivalence: false - id: infinitary_extensive_distributivity @@ -48,7 +64,16 @@ - finite products conclusions: - infinitary distributive - proof: One can adjust the proof of Prop. 4.5 in Introduction to extensive and distributive categories (which deals with the finite case). + proof: One can adjust the proof of Prop. 4.5 in Introduction to extensive and distributive categories by Carboni-Lack-Walters (which deals with the finite case). + is_equivalence: false + +- id: countably_extensive_distributivity + assumptions: + - countably extensive + - finite products + conclusions: + - countably distributive + proof: One can adjust the proof of Prop. 4.5 in Introduction to extensive and distributive categories by Carboni-Lack-Walters (which deals with the finite case). is_equivalence: false - id: lcc_implies_extensive diff --git a/database/data/category-properties/coextensive.yaml b/database/data/category-properties/coextensive.yaml index 81b0b543..ca5390b7 100644 --- a/database/data/category-properties/coextensive.yaml +++ b/database/data/category-properties/coextensive.yaml @@ -1,14 +1,15 @@ id: coextensive relation: is -description: A category $\C$ is coextensive when it has finite products and for all objects $A,B \in \C$ the product functor $A/\C \times B/\C \to (A \times B)/\C$ is an equivalence of categories. The prototypical example is the category of commutative rings. +description: A category $\C$ is coextensive when it has finite products and for all objects $A,B \in \C$ the product functor $A/\C \times B/\C \to (A \times B)/\C$ is an equivalence of categories. Equivalently (by using the characterization of extensive categories), pushouts along binary product projections exist, binary products are disjoint, and binary products are stable under pushouts. The prototypical example is the category of commutative rings. nlab_link: null dual: extensive invariant_under_equivalences: true related: - disjoint finite products - - finite products + - codistributive - infinitary coextensive + - countably coextensive tags: - limit–colimit interaction diff --git a/database/data/category-properties/countably coextensive.yaml b/database/data/category-properties/countably coextensive.yaml new file mode 100644 index 00000000..1d617242 --- /dev/null +++ b/database/data/category-properties/countably coextensive.yaml @@ -0,0 +1,22 @@ +id: countably coextensive +relation: is +description: >- + A category $\C$ is countably coextensive if it has countable products and, for every countable family of objects $(A_i)_{i \in I}$, the product functor + $$\textstyle \prod_{i \in I} (A_i/\C) \to (\coprod_{i \in I} A_i) / \C,$$ + which maps a family of morphisms $(A_i \to X_i)_{i \in I}$ to their product $\prod_{i \in I} A_i \to \prod_{i \in I} X_i$, is an equivalence of categories. Equivalently (by using the characterization of countably extensive categories), pushouts along product projections exist, countable products are disjoint, and countable products are stable under pushouts. + + The only difference between this property and the property of being infinitary coextensive is that we restrict ourselves to countable families. + +nlab_link: null +dual: countably extensive +invariant_under_equivalences: true + +related: + - disjoint products + - countable products + - countably codistributive + - coextensive + - infinitary coextensive + +tags: + - limit–colimit interaction diff --git a/database/data/category-properties/countably extensive.yaml b/database/data/category-properties/countably extensive.yaml new file mode 100644 index 00000000..c352dab6 --- /dev/null +++ b/database/data/category-properties/countably extensive.yaml @@ -0,0 +1,22 @@ +id: countably extensive +relation: is +description: >- + A category $\C$ is countably extensive if it has countable coproducts and, for every countable family of objects $(A_i)_{i \in I}$, the coproduct functor + $$\textstyle \prod_{i \in I} (\C/A_i) \to \C/(\coprod_{i \in I} A_i),$$ + which maps a family of morphisms $(X_i \to A_i)_{i \in I}$ to their coproduct $\coprod_{i \in I} X_i \to \coprod_{i \in I} A_i$, is an equivalence of categories. Equivalently, pullbacks along coproduct inclusions exist, countable coproducts are disjoint, and countable coproducts are stable under pullbacks. For a proof of this equivalent characterization, see Section 2 of Introduction to extensive and distributive categories by Carboni, Lack, and Walters. This covers the finite case, but the countable case is similar. + + The only difference between this property and the property of being infinitary extensive is that we restrict ourselves to countable families. A typical example of a countably extensive category which is not infinitary extensive is the category of measurable spaces. + +nlab_link: null +dual: countably coextensive +invariant_under_equivalences: true + +related: + - disjoint coproducts + - countable coproducts + - countably distributive + - extensive + - infinitary extensive + +tags: + - limit–colimit interaction diff --git a/database/data/category-properties/extensive.yaml b/database/data/category-properties/extensive.yaml index 64243e66..ac9e0eb8 100644 --- a/database/data/category-properties/extensive.yaml +++ b/database/data/category-properties/extensive.yaml @@ -1,14 +1,25 @@ id: extensive relation: is -description: A category $\C$ is extensive when it has finite coproducts and for all objects $A,B \in \C$ the coproduct functor $\C/A \times \C/B \to \C/(A+B)$ is an equivalence of categories. Equivalently, pullbacks of finite coproduct inclusions along arbitrary morphisms exist and finite coproducts are disjoint and stable under pullback. +description: >- + A category $\C$ is extensive when it has finite coproducts (denoted $+$) and for all objects $A,B \in \C$ the coproduct functor + $$\C/A \times \C/B \to \C/(A+B),$$ + which maps $(X \to A, Y \to B)$ to $(X+Y \to A+B)$, is an equivalence of categories. This is equivalent to the following three conditions: +
    +
  1. Pullbacks along binary coproduct inclusions exist, i.e. for every morphism $T \to A + B$, the pullback $T \times_{A + B} A$ exists.
    2. +
  2. Binary coproducts are disjoint: The coproduct inclusions $A \rightarrow A + B \leftarrow B$ are monomorphisms, and their pullback $A \times_{A + B} B$ is the initial object $0$.
    3. +
  3. Binary coproducts are stable under pullbacks: For every morphism $T \to A + B$, if we define the pullbacks $T_A := T \times_{A + B} A$ and $T_B := T \times_{A + B} B$, then the canonical morphism $T_A + T_B \to T$ is an isomorphism.
    4. +
+ For a proof of this equivalent characterization, see Section 2 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. + nlab_link: https://ncatlab.org/nlab/show/extensive+category dual: coextensive invariant_under_equivalences: true related: - disjoint finite coproducts - - finite coproducts + - distributive - infinitary extensive + - countably extensive - pretopos tags: diff --git a/database/data/category-properties/infinitary coextensive.yaml b/database/data/category-properties/infinitary coextensive.yaml index 57a2cd59..dfa623d5 100644 --- a/database/data/category-properties/infinitary coextensive.yaml +++ b/database/data/category-properties/infinitary coextensive.yaml @@ -1,7 +1,7 @@ id: infinitary coextensive relation: is description: |- - A category $\C$ is infinitary coextensive when it has products and for all families of objects $(A_i)_{i \in I}$ the product functor $\prod_{i \in I} A_i / \C/A_i \to \prod_{i \in I} A_i / \C$ is an equivalence of categories. + A category $\C$ is infinitary coextensive when it has products and for all families of objects $(A_i)_{i \in I}$ the product functor $\prod_{i \in I} (A_i / \C) \to (\prod_{i \in I} A_i) / \C$ is an equivalence of categories. Equivalently (by using the characterization of infinitary extensive categories), pushouts along product projections exist, products are disjoint, and products are stable under pushouts. This terminology does not seem to be common, but we have added it as a dual for the more commonly known property of being infinitary extensive. nlab_link: null dual: infinitary extensive @@ -10,7 +10,8 @@ invariant_under_equivalences: true related: - coextensive - disjoint products - - products + - infinitary codistributive + - countably coextensive tags: - limit–colimit interaction diff --git a/database/data/category-properties/infinitary extensive.yaml b/database/data/category-properties/infinitary extensive.yaml index c2966d04..624fac18 100644 --- a/database/data/category-properties/infinitary extensive.yaml +++ b/database/data/category-properties/infinitary extensive.yaml @@ -1,14 +1,25 @@ id: infinitary extensive relation: is -description: A category $\C$ is infinitary extensive when it has coproducts and for all families of objects $(A_i)_{i \in I}$ the coproduct functor $\prod_{i \in I} \C/A_i \to \C/(\coprod_{i \in I} A_i)$ is an equivalence of categories. Equivalently, pullbacks of coproduct inclusions along arbitrary morphisms exist and coproducts are disjoint and stable under pullback. +description: >- + A category $\C$ is infinitary extensive when it has coproducts and for all families of objects $(A_i)_{i \in I}$ the coproduct functor + $$\textstyle \prod_{i \in I} (\C/A_i) \to \C/(\coprod_{i \in I} A_i),$$ + that maps a family of morphisms $(X_i \to A_i)_{i \in I}$ to their coproduct $\coprod_{i \in I} X_i \to \coprod_{i \in I} A_i$, is an equivalence of categories. This is equivalent to the following three conditions: +
    +
  1. Pullbacks along coproduct inclusions exist, i.e. for every morphism $T \to \coprod_{i \in I} A_i$ and every $i \in I$ the pullback $T \times_{\coprod_{i \in I} A_i} A_i$ exists.
    2. +
  2. Coproducts are disjoint: Each coproduct inclusion $A_i \to \coprod_{i \in I} A_i$ is a monomorphism, and for $i \neq j$ the pullback $A_i \times_{\coprod_{i \in I} A_i} A_j$ is the initial object $0$.
    3. +
  3. Coproducts are stable under pullbacks: For every morphism $T \to \coprod_{i \in I} A_i$, if we define the pullbacks $T_i := T \times_{\coprod_{i \in I} A_i} A_i$ for $i \in I$, then the canonical morphism $\coprod_{i \in I} T_i \to T$ is an isomorphism.
    4. +
+ For a proof of this equivalent characterization, see Section 2 in Introduction to extensive and distributive categories by Carboni-Lack-Walters; this covers the finite case, but the infinite case is similar. + nlab_link: https://ncatlab.org/nlab/show/extensive+category dual: infinitary coextensive invariant_under_equivalences: true related: - - coproducts - disjoint coproducts + - infinitary distributive - extensive + - countably extensive tags: - limit–colimit interaction diff --git a/database/data/macros.yaml b/database/data/macros.yaml index bcb0b582..bd497850 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -32,7 +32,7 @@ # abbreviations \op: \mathrm{op} \c: \mathrm{c} -\f: \mathrm{f} +\ff: \mathrm{ff} \fg: \mathrm{fg} \fp: \mathrm{fp} \ab: \mathrm{ab} diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 4d8ef7c2..07401a34 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -147,8 +147,10 @@ "codistributive": false, "infinitary codistributive": false, "extensive": false, + "countably extensive": false, "infinitary extensive": false, "coextensive": false, + "countably coextensive": false, "infinitary coextensive": false, "regular subobject classifier": false, "direct": false, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index 5ceebb92..5ceee3db 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -60,6 +60,7 @@ "regular": true, "coregular": true, "extensive": true, + "countably extensive": true, "infinitary extensive": true, "co-Malcev": true, "locally strongly finitely presentable": true, @@ -146,6 +147,7 @@ "disjoint finite products": false, "disjoint products": false, "coextensive": false, + "countably coextensive": false, "infinitary coextensive": false, "unital": false, "counital": false, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index f66e00c9..8e7eabc8 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -46,6 +46,7 @@ "wide pushouts": true, "coregular": true, "extensive": true, + "countably extensive": true, "infinitary extensive": true, "regular subobject classifier": true, "coreflexive equalizers": true, @@ -125,6 +126,7 @@ "disjoint finite products": false, "disjoint products": false, "coextensive": false, + "countably coextensive": false, "infinitary coextensive": false, "co-Malcev": false, "unital": false,