Add concretizable categories

.cspell.json

@@ -106,6 +106,7 @@
 		"comonadicity",
 		"compactification",
 		"compactifications",
+		"concretizable",
 		"conormal",
 		"copower",
 		"copowers",

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 <a href="/category/Set_op">$\Set^{\op}$</a> is concretizable (say, via the contravariant power set functor), and <a href="/category/SetxSet">$\Set \times \Set$</a> 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 <a href="/category/Top">$\Top$</a> is infinitary extensive.

database/data/categories/Sch_R.yaml

@@ -22,14 +22,17 @@ 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 <a href="/category/LRS_R">$\LRS_R$</a> is locally small.
 
   - property: terminal object
     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. Alternatively, one can show that $\Sch_R$ is closed under pullbacks in the category <a href="/category/LRS_R">$\LRS_R$</a>, which has pullbacks.
 
+  - property: concretizable
+    proof: This is because <a href="/category/LRS_R">$\LRS_R$</a> is concretizable.
+
   - property: well-powered
     proof: See <a href="https://mathoverflow.net/questions/160681" target="_blank">MO/160681</a>.
 

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$.'

database/data/category-properties/concretizable.yaml

@@ -0,0 +1,16 @@
+id: concretizable
+relation: is
+description: >-
+  A category $\C$ is <i>concretizable</i> when it admits a faithful functor
+  $$U : \C \to \Set.$$
+  In this case, the pair $(\C,U)$ is called a <i>concrete category</i>. 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 <a href="/functor/power_set_contravariant">contravariant power set functor</a>).
+nlab_link: https://ncatlab.org/nlab/show/concrete+category
+dual: concretizable
+invariant_under_equivalences: true
+
+related:
+  - generating set
+  - locally essentially small
+
+tags:
+  - size

database/data/category-properties/generating set.yaml

@@ -13,6 +13,7 @@ invariant_under_equivalences: true
 related:
   - generator
   - extremal generating set
+  - concretizable
 
 tags:
   - size

database/data/category-properties/locally essentially small.yaml

@@ -1,6 +1,8 @@
 id: locally essentially small
 relation: is
-description: A category is <i>locally essentially small</i> 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 <i>locally essentially small</i> when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is isomorphic to a set; see <a href="/content/foundations">here</a> 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

database/data/category-properties/locally small.yaml

@@ -1,6 +1,6 @@
 id: locally small
 relation: is
-description: A category is <i>locally small</i> 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 <i>locally small</i> when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is a set; see <a href="/content/foundations">here</a> 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

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,

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,

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,