diff --git a/databases/catdat/data/categories/Ab_fg.yaml b/databases/catdat/data/categories/Ab_fg.yaml index eeb943ba8..ff8925c8e 100644 --- a/databases/catdat/data/categories/Ab_fg.yaml +++ b/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. diff --git a/databases/catdat/data/categories/B.yaml b/databases/catdat/data/categories/B.yaml index e0d106b3c..8134d5401 100644 --- a/databases/catdat/data/categories/B.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: inhabited reason: This is trivial. diff --git a/databases/catdat/data/categories/BG_c.yaml b/databases/catdat/data/categories/BG_c.yaml index 9f0f239d2..a1ddd7b77 100644 --- a/databases/catdat/data/categories/BG_c.yaml +++ b/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: {} diff --git a/databases/catdat/data/categories/BN.yaml b/databases/catdat/data/categories/BN.yaml index 8fd59d161..f5b7a565f 100644 --- a/databases/catdat/data/categories/BN.yaml +++ b/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. diff --git a/databases/catdat/data/categories/Delta.yaml b/databases/catdat/data/categories/Delta.yaml index edd8e79bd..255176041 100644 --- a/databases/catdat/data/categories/Delta.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: countable reason: This is obvious. diff --git a/databases/catdat/data/categories/FI.yaml b/databases/catdat/data/categories/FI.yaml index 462f6923d..4c29cba58 100644 --- a/databases/catdat/data/categories/FI.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: left cancellative reason: This is trivial. diff --git a/databases/catdat/data/categories/FS.yaml b/databases/catdat/data/categories/FS.yaml index a75438ef1..2405de448 100644 --- a/databases/catdat/data/categories/FS.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: essentially countable reason: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$. diff --git a/databases/catdat/data/categories/FinAb.yaml b/databases/catdat/data/categories/FinAb.yaml index cb5a0b1d2..defad2f8c 100644 --- a/databases/catdat/data/categories/FinAb.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: essentially countable reason: The underlying set of a finite structure can be chosen to be a subset of $\IN$. diff --git a/databases/catdat/data/categories/FinGrp.yaml b/databases/catdat/data/categories/FinGrp.yaml index c3a06c9e5..faf132eaa 100644 --- a/databases/catdat/data/categories/FinGrp.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: pointed reason: The trivial group is a zero object. check_redundancy: false diff --git a/databases/catdat/data/categories/FinOrd.yaml b/databases/catdat/data/categories/FinOrd.yaml index f44d7adfd..6cc7d2af0 100644 --- a/databases/catdat/data/categories/FinOrd.yaml +++ b/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 $\FinSet$ is locally finite. + - property_id: essentially countable reason: Every finite ordered set is isomorphic to $\{0 < \cdots < n-1 \}$ for some $n \in \IN$. diff --git a/databases/catdat/data/categories/FinSet.yaml b/databases/catdat/data/categories/FinSet.yaml index 5296b3f7a..7cccc389a 100644 --- a/databases/catdat/data/categories/FinSet.yaml +++ b/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$. diff --git a/databases/catdat/data/categories/Fld.yaml b/databases/catdat/data/categories/Fld.yaml index e2ecff42d..510f66810 100644 --- a/databases/catdat/data/categories/Fld.yaml +++ b/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$. diff --git a/databases/catdat/data/categories/Met.yaml b/databases/catdat/data/categories/Met.yaml index 3e14bb03e..3fbd3bf4d 100644 --- a/databases/catdat/data/categories/Met.yaml +++ b/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. diff --git a/databases/catdat/data/categories/PMet.yaml b/databases/catdat/data/categories/PMet.yaml index 3d68f363c..f409cd3a3 100644 --- a/databases/catdat/data/categories/PMet.yaml +++ b/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. diff --git a/databases/catdat/data/categories/Set_f.yaml b/databases/catdat/data/categories/Set_f.yaml index 4a3a49b1c..b9964b0db 100644 --- a/databases/catdat/data/categories/Set_f.yaml +++ b/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. diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 6c4bd148e..c01342b2d 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/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.' diff --git a/databases/catdat/data/category-implications/size.yaml b/databases/catdat/data/category-implications/size.yaml index f7fdec12b..3a3c66319 100644 --- a/databases/catdat/data/category-implications/size.yaml +++ b/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 diff --git a/databases/catdat/data/category-implications/thin.yaml b/databases/catdat/data/category-implications/thin.yaml index 47b161b90..f9050eb8b 100644 --- a/databases/catdat/data/category-implications/thin.yaml +++ b/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 diff --git a/databases/catdat/data/category-properties/essentially finite.yaml b/databases/catdat/data/category-properties/essentially finite.yaml index f125d698c..d7ed4a1d3 100644 --- a/databases/catdat/data/category-properties/essentially finite.yaml +++ b/databases/catdat/data/category-properties/essentially finite.yaml @@ -8,3 +8,4 @@ related_properties: - essentially countable - essentially small - finite + - locally finite diff --git a/databases/catdat/data/category-properties/finite.yaml b/databases/catdat/data/category-properties/finite.yaml index 1fda8664a..816f89224 100644 --- a/databases/catdat/data/category-properties/finite.yaml +++ b/databases/catdat/data/category-properties/finite.yaml @@ -8,4 +8,5 @@ invariant_under_equivalences: false related_properties: - countable - essentially finite + - locally finite - small diff --git a/databases/catdat/data/category-properties/locally finite.yaml b/databases/catdat/data/category-properties/locally finite.yaml new file mode 100644 index 000000000..09b693f7f --- /dev/null +++ b/databases/catdat/data/category-properties/locally finite.yaml @@ -0,0 +1,10 @@ +id: locally finite +relation: is +description: A category is locally finite or Hom-finite 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 diff --git a/databases/catdat/data/category-properties/thin.yaml b/databases/catdat/data/category-properties/thin.yaml index bcbe3dcad..d070c834d 100644 --- a/databases/catdat/data/category-properties/thin.yaml +++ b/databases/catdat/data/category-properties/thin.yaml @@ -8,3 +8,4 @@ invariant_under_equivalences: true related_properties: - core-thin - discrete + - locally finite diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index adf0df414..5727343b4 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/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 } diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 45f661464..5e68abb26 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/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 } diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index 93cc5571f..1f7143932 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/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 }