diff --git a/.cspell.json b/.cspell.json index e3a2b1cea..2d9cc8751 100644 --- a/.cspell.json +++ b/.cspell.json @@ -106,6 +106,7 @@ "comonadicity", "compactification", "compactifications", + "concretizable", "conormal", "copower", "copowers", diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml index 851eb7958..83387ceec 100644 --- a/database/data/categories/LRS_R.yaml +++ b/database/data/categories/LRS_R.yaml @@ -30,6 +30,20 @@ satisfied_properties: - property: well-copowered proof: This follows from the characterization of epimorphisms below. + - property: concretizable + proof: >- + Consider the functor $F : \LRS_R \to \Set \times \Set^{\op}$ defined on objects by + $$\textstyle F(X,\O_X) \coloneqq \bigl(|X|,\coprod_{U \subseteq X} |\O_X(U)|\bigr),$$ + where $U$ runs through the open subsets of $X$ and $|{-}|$ denotes the underlying set of a topological space or ring, respectively. If $(f,f^\sharp) : (X,\O_X) \to (Y,\O_Y)$ is a morphism of locally ringed spaces, then we get a map of sets $|f| : |X| \to |Y|$, and the ring homomorphisms $f^\sharp(V) : \O_Y(V) \to \O_X(f^*(V))$ for opens $V \subseteq Y$ induce a map of sets + $$\textstyle \alpha : \coprod_{V \subseteq Y} \O_Y(V) \to \coprod_{U \subseteq X} \O_X(U)$$ + defined by $\alpha \circ \iota_V = \iota_{f^*(V)} \circ f^\sharp(V)$. We let $F(f,f^\sharp) \coloneqq (|f|,\alpha)$. It is easy to verify that $F$ is a functor. + + To show that $F$ is faithful, assume that $(f,f^\sharp)$ and $(g,g^\sharp)$ are two morphisms with the same image under $F$. Then $|f| = |g|$, hence $f = g$. Also, we have + $$\iota_{f^*(V)} \circ f^\sharp(V) = \iota_{g^*(V)} \circ g^\sharp(V)$$ + for every open subset $V \subseteq Y$. Since $\iota_{f^*(V)} = \iota_{g^*(V)}$ is a monomorphism of sets, we conclude that $f^\sharp(V) = g^\sharp(V)$. Thus, $f^\sharp = g^\sharp$. We have shown $(f,f^\sharp) = (g,g^\sharp)$, as required. + + Since $\Set^{\op}$ is concretizable (say, via the contravariant power set functor), and $\Set \times \Set$ is also concretizable (because it is locally small and has a generating set), it follows that $\LRS_R$ is concretizable. + - property: infinitary extensive proof: >- The proof works for both ringed and locally ringed spaces and relies on the fact that $\Top$ is infinitary extensive. diff --git a/database/data/categories/Sch_R.yaml b/database/data/categories/Sch_R.yaml index aef7cd69e..7d60a8ee9 100644 --- a/database/data/categories/Sch_R.yaml +++ b/database/data/categories/Sch_R.yaml @@ -22,7 +22,7 @@ comments: satisfied_properties: - property: locally small - proof: There is a forgetful functor $\Sch_R \to \LRS_R$ and $\LRS_R$ is locally small. + proof: There is a forgetful functor $\Sch_R \to \LRS_R$ and $\LRS_R$ is locally small. - property: terminal object proof: The scheme $\Spec(R)$ is terminal. @@ -30,6 +30,9 @@ satisfied_properties: - 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. Alternatively, one can show that $\Sch_R$ is closed under pullbacks in the category $\LRS_R$, which has pullbacks. + - property: concretizable + proof: This is because $\LRS_R$ is concretizable. + - property: well-powered proof: See MO/160681. diff --git a/database/data/category-implications/size.yaml b/database/data/category-implications/size.yaml index 55d61f8f0..d549163c1 100644 --- a/database/data/category-implications/size.yaml +++ b/database/data/category-implications/size.yaml @@ -61,3 +61,18 @@ conclusions: - locally essentially small proof: This is trivial. + +- id: concretizable_is_locally_essentially_small + assumptions: + - concretizable + conclusions: + - locally essentially small + proof: 'If $U : \C \to \Set$ is a faithful functor, for every pair of objects $A,B$, the collection $\Hom(A,B)$ embeds into the set $\Hom(U(A),U(B))$, so that it is isomorphic to a set.' + +- id: generating_set_concrete + assumptions: + - generating set + - locally essentially small + conclusions: + - concretizable + proof: 'If $S$ is a generating set of a locally small category $\C$, then by definition the functor $(\Hom(G,-))_{G \in S} : \C \to \Set^S$ is faithful. Furthermore, the functor $\Set^S \to \Set$ mapping $X \mapsto \coprod_{G \in S} X_G$ is faithful. Their composition provides a faithful functor $\C \to \Set$.' diff --git a/database/data/category-properties/concretizable.yaml b/database/data/category-properties/concretizable.yaml new file mode 100644 index 000000000..251f621ee --- /dev/null +++ b/database/data/category-properties/concretizable.yaml @@ -0,0 +1,16 @@ +id: concretizable +relation: is +description: >- + A category $\C$ is concretizable when it admits a faithful functor + $$U : \C \to \Set.$$ + In this case, the pair $(\C,U)$ is called a concrete category. Thus, "concretizable" is a property, whereas "concrete" is additional structure. (Some authors use "concrete" for the property as well.) The property of being concretizable is self-dual since $\Set^{\op}$ is concretizable (for instance, via the contravariant power set functor). +nlab_link: https://ncatlab.org/nlab/show/concrete+category +dual: concretizable +invariant_under_equivalences: true + +related: + - generating set + - locally essentially small + +tags: + - size diff --git a/database/data/category-properties/generating set.yaml b/database/data/category-properties/generating set.yaml index 2658ce9c5..7f847d270 100644 --- a/database/data/category-properties/generating set.yaml +++ b/database/data/category-properties/generating set.yaml @@ -13,6 +13,7 @@ invariant_under_equivalences: true related: - generator - extremal generating set + - concretizable tags: - size diff --git a/database/data/category-properties/locally essentially small.yaml b/database/data/category-properties/locally essentially small.yaml index 9f1ae23aa..9cbc23ed0 100644 --- a/database/data/category-properties/locally essentially small.yaml +++ b/database/data/category-properties/locally essentially small.yaml @@ -1,6 +1,8 @@ id: locally essentially small relation: is -description: A category is locally essentially small when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is isomorphic to a set. (Here, we work with a set-theoretic foundation in which there are sets and collections. Categories are based on collections of objects and morphisms.) Equivalently, the category is equivalent to a locally small category. In contrast to being locally small, this condition is invariant under equivalences of categories. This is why we have added it to the database. For instance, every algebraic category is locally essentially small, but not necessarily locally small. This indicates that this is the "right" notion to work with. +description: >- + A category is locally essentially small when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is isomorphic to a set; see here for the set-theoretic foundation of category theory we are working with. + A category is locally essentially small if and only if it is equivalent to a locally small category. In contrast to being locally small, this condition is invariant under equivalences of categories. This is why we have added it to the database. For instance, every algebraic category is locally essentially small, but not necessarily locally small. This indicates that this is the "right" notion to work with. nlab_link: null dual: locally essentially small invariant_under_equivalences: true diff --git a/database/data/category-properties/locally small.yaml b/database/data/category-properties/locally small.yaml index b3dadc8be..ee222525b 100644 --- a/database/data/category-properties/locally small.yaml +++ b/database/data/category-properties/locally small.yaml @@ -1,6 +1,6 @@ id: locally small relation: is -description: A category is locally small when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is a set. Here, we work with a set-theoretic foundation in which there are sets and collections. Categories are based on collections of objects and morphisms. +description: A category is locally small when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is a set; see here for the set-theoretic foundation of category theory we are working with. nlab_link: https://ncatlab.org/nlab/show/locally+small+category dual: locally small invariant_under_equivalences: false diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index df68bb2c8..54cd258d6 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -125,6 +125,7 @@ "cokernel pairs": true, "equalizers of cokernel pairs": true, "coequalizers of kernel pairs": true, + "concretizable": true, "cartesian closed": false, "locally cartesian closed": false, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index e405c63d4..6a2502ea6 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -123,6 +123,7 @@ "cokernel pairs": true, "equalizers of cokernel pairs": true, "coequalizers of kernel pairs": true, + "concretizable": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index b5aefcc9f..50fc8175a 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -88,6 +88,7 @@ "cokernel pairs": true, "equalizers of cokernel pairs": true, "coequalizers of kernel pairs": true, + "concretizable": true, "abelian": false, "additive": false,