Add new property: locally finite

databases/catdat/data/categories/Ab_fg.yaml

@@ -33,6 +33,9 @@ unsatisfied_properties:
   - property_id: small
     reason: Even the collection of trivial groups is not small.
 
+  - property_id: locally finite
+    reason: The group $\Hom(\IZ,\IZ) \cong \IZ$ is not finite.
+
   - property_id: skeletal
     reason: This is trivial.
 

databases/catdat/data/categories/B.yaml

@@ -18,6 +18,9 @@ satisfied_properties:
   - property_id: locally small
     reason: There is a forgetful functor $\IB \to \Set$ and $\Set$ is locally small.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\IB \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: inhabited
     reason: This is trivial.
 

databases/catdat/data/categories/BG_c.yaml

@@ -35,7 +35,7 @@ satisfied_properties:
     reason: This is because $G$ is countable.
 
 unsatisfied_properties:
-  - property_id: essentially finite
+  - property_id: locally finite
     reason: This is because we choose $G$ to be infinite.
 
 special_objects: {}

databases/catdat/data/categories/BN.yaml

@@ -44,6 +44,9 @@ unsatisfied_properties:
   - property_id: one-way
     reason: This is trivial.
 
+  - property_id: locally finite
+    reason: This is trivial.
+
   - property_id: sequential limits
     reason: Assume that the sequence $\cdots \xrightarrow{1}  \bullet \xrightarrow{1} \bullet \xrightarrow{1} \bullet$ has a limit. This is a (universal) sequence of natural numbers $n_0,n_1,\dotsc$ satisfying $n_i = n_{i+1} + 1$. But then $n_i = n_0 - i$, and in particular $n_{n_0 + 1} = - 1$, a contradiction.
 

databases/catdat/data/categories/Delta.yaml

@@ -21,6 +21,9 @@ satisfied_properties:
   - property_id: small
     reason: This is trivial.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\Delta \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: countable
     reason: This is obvious.
 

databases/catdat/data/categories/FI.yaml

@@ -19,6 +19,9 @@ satisfied_properties:
   - property_id: locally small
     reason: There is a forgetful functor $\FI \to \Set$ and $\Set$ is locally small.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\FI \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: left cancellative
     reason: This is trivial.
 

databases/catdat/data/categories/FS.yaml

@@ -19,6 +19,9 @@ satisfied_properties:
   - property_id: locally small
     reason: There is a forgetful functor $\FS \to \Set$ and $\Set$ is locally small.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\FS \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: essentially countable
     reason: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$.
 

databases/catdat/data/categories/FinAb.yaml

@@ -19,6 +19,9 @@ satisfied_properties:
   - property_id: locally small
     reason: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\FinAb \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: essentially countable
     reason: The underlying set of a finite structure can be chosen to be a subset of $\IN$.
 

databases/catdat/data/categories/FinGrp.yaml

@@ -18,6 +18,9 @@ satisfied_properties:
   - property_id: locally small
     reason: It is a full subcategory of $\Grp$, which is locally small.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\FinGrp \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: pointed
     reason: The trivial group is a zero object.
     check_redundancy: false

databases/catdat/data/categories/FinOrd.yaml

@@ -19,6 +19,9 @@ satisfied_properties:
   - property_id: locally small
     reason: There is a forgetful functor $\FinOrd \to \Set$ and $\Set$ is locally small.
 
+  - property_id: locally finite
+    reason: There is a faithful functor $\FinOrd \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+
   - property_id: essentially countable
     reason: Every finite ordered set is isomorphic to $\{0 < \cdots < n-1 \}$ for some $n \in \IN$.
 

databases/catdat/data/categories/FinSet.yaml

@@ -23,6 +23,9 @@ satisfied_properties:
   - property_id: locally small
     reason: There is a forgetful functor $\FinSet \to \Set$ and $\Set$ is locally small.
 
+  - property_id: locally finite
+    reason: This is trivial.
+
   - property_id: essentially countable
     reason: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$.
 

databases/catdat/data/categories/Fld.yaml

@@ -35,6 +35,9 @@ unsatisfied_properties:
   - property_id: skeletal
     reason: This is trivial.
 
+  - property_id: locally finite
+    reason: There are infinitely many homomorphisms $\IQ(X) \to \IQ(X)$, $X \mapsto X^k$.
+
   - property_id: connected
     reason: A field of characteristic $0$ cannot be connected with a field of characteristic $p > 0$. in fact, the connected components of $\Fld$ are the subcategories $\Fld_p$ of fields of characteristic $p$, where $p$ is a prime or $0$.
 

databases/catdat/data/categories/Met.yaml

@@ -68,6 +68,9 @@ unsatisfied_properties:
   - property_id: essentially small
     reason: This is trivial.
 
+  - property_id: locally finite
+    reason: This is obvious.
+
   - property_id: strict terminal object
     reason: This is trivial.
 

databases/catdat/data/categories/PMet.yaml

@@ -63,6 +63,9 @@ unsatisfied_properties:
   - property_id: essentially small
     reason: This is trivial.
 
+  - property_id: locally finite
+    reason: This is obvious.
+
   - property_id: strict terminal object
     reason: This is trivial.
 

databases/catdat/data/categories/Set_f.yaml

@@ -60,6 +60,9 @@ unsatisfied_properties:
   - property_id: essentially small
     reason: This is obvious.
 
+  - property_id: locally finite
+    reason: If $X$ is an infinite set, there are infinitely many maps $1 \to X$. They are injective and hence finite-to-one.
+
   - property_id: strongly connected
     reason: Already $\Set$ is not strongly connected.
 

databases/catdat/data/categories/Sp.yaml

@@ -27,6 +27,9 @@ unsatisfied_properties:
   - property_id: skeletal
     reason: This is trivial.
 
+  - property_id: locally finite
+    reason: If $1$ denotes the terminal species, there are infinitely many morphisms $1 \to 1 \sqcup 1$ since they correspond to functions $\IN \to \{1,2\}$.
+
   - property_id: locally small
     reason: 'Disclaimer: This result and its proof are not relevant for category theory and are also depending on the concrete model of set theory. That this category is locally essentially small is only what matters. Now, consider the terminal species $F=G=1$. Then $\Hom(F,G)$ has just a single element, namely the natural transformation $\alpha$ that sends every finite set $X$ to the unique map $\alpha_X : 1 \to 1$. Formally, $\alpha$ is a map, modelled as a set of ordered pairs $(X,\id_1)$, where $X$ is a finite set. Hence, $\alpha$ is not a set (since finite sets do not form a set), and therefore $\Hom(F,G) = \{\alpha\}$ is also not a set.'
 

databases/catdat/data/category-implications/size.yaml

@@ -34,6 +34,7 @@
     - essentially finite
   conclusions:
     - essentially countable
+    - locally finite
   reason: This is trivial.
   is_equivalence: false
 
@@ -60,3 +61,11 @@
     - locally essentially small
   reason: This is trivial.
   is_equivalence: false
+
+- id: locally_finite_consequence
+  assumptions:
+    - locally finite
+  conclusions:
+    - locally essentially small
+  reason: This is trivial.
+  is_equivalence: false

databases/catdat/data/category-implications/thin.yaml

@@ -5,7 +5,7 @@
     - thin
   conclusions:
     - generating set
-    - locally essentially small
+    - locally finite
     - one-way
     - equalizers
     - left cancellative
@@ -30,6 +30,15 @@
   reason: 'Let $X$ be any object. The swap $\tau : X \times X \to X \times X$ is an automorphism, hence equal to the identity. It follows that the projections $p_1,p_2 : X \times X \rightrightarrows X$ are the same. And this means that every two morphisms $Y \rightrightarrows X$ are the same.'
   is_equivalence: false
 
+- id: thin_via_locally-finite
+  assumptions:
+    - locally finite
+    - countable powers
+  conclusions:
+    - thin
+  reason: If $A,B$ are objects, we have a bijection $\Hom(A,B)^{\IN} \cong \Hom(A,B^{\IN})$. By assumption, this set is finite. Hence, $\Hom(A,B)$ has at most one element.
+  is_equivalence: false
+
 - id: thin_groupoids
   assumptions:
     - core-thin

databases/catdat/data/category-properties/essentially finite.yaml

@@ -8,3 +8,4 @@ related_properties:
   - essentially countable
   - essentially small
   - finite
+  - locally finite

databases/catdat/data/category-properties/finite.yaml

@@ -8,4 +8,5 @@ invariant_under_equivalences: false
 related_properties:
   - countable
   - essentially finite
+  - locally finite
   - small

databases/catdat/data/category-properties/locally finite.yaml

@@ -0,0 +1,10 @@
+id: locally finite
+relation: is
+description: A category is <i>locally finite</i> or <i>Hom-finite</i> when for all objects $A,B$ the collection $\Hom(A,B)$ is finite. (We do not assume that this collection is an actual set. Therefore, this property is invariant under equivalences of categories.)
+nlab_link: https://ncatlab.org/nlab/show/locally+finite+category
+dual_property_id: locally finite
+invariant_under_equivalences: true
+
+related_properties:
+  - finite
+  - thin

databases/catdat/data/category-properties/thin.yaml

@@ -8,3 +8,4 @@ invariant_under_equivalences: true
 related_properties:
   - core-thin
   - discrete
+  - locally finite

databases/catdat/scripts/expected-data/Ab.json

@@ -157,5 +157,6 @@
 	"gaunt": false,
 	"core-thin": false,
 	"subobject-trivial": false,
-	"quotient-trivial": false
+	"quotient-trivial": false,
+	"locally finite": false
 }

databases/catdat/scripts/expected-data/Set.json

@@ -157,5 +157,6 @@
 	"gaunt": false,
 	"core-thin": false,
 	"subobject-trivial": false,
-	"quotient-trivial": false
+	"quotient-trivial": false,
+	"locally finite": false
 }

databases/catdat/scripts/expected-data/Top.json

@@ -157,5 +157,6 @@
 	"subobject-trivial": false,
 	"quotient-trivial": false,
 	"effective congruences": false,
-	"effective cocongruences": false
+	"effective cocongruences": false,
+	"locally finite": false
 }