diff --git a/.cspell.json b/.cspell.json index 2e78761b..680f8ff9 100644 --- a/.cspell.json +++ b/.cspell.json @@ -16,7 +16,8 @@ "mdash", "comphaus", "esbuild", - "coloneqq" + "coloneqq", + "FiltVect" ], "words": [ "abelian", @@ -136,6 +137,7 @@ "extensivity", "extremal", "fieldification", + "filtrations", "finitary", "foundedness", "Freyd", diff --git a/databases/catdat/data/categories/Ab_fg.yaml b/databases/catdat/data/categories/Ab_fg.yaml index d9f65472..bfc7e3bc 100644 --- a/databases/catdat/data/categories/Ab_fg.yaml +++ b/databases/catdat/data/categories/Ab_fg.yaml @@ -12,6 +12,7 @@ tags: related_categories: - Ab - FinAb + - FinVect_c satisfied_properties: - property: locally small @@ -27,7 +28,7 @@ satisfied_properties: proof: Every finitely generated abelian group is isomorphic to a group of the form $\IZ^n / U$, where $n \in \IN$ and $U$ is a subgroup of $\IZ^n$. Since $\IZ^n$ is Noetherian as a $\IZ$-module, $U$ is finitely generated, hence the category $\Ab_\fg$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \IZ^n / U$ and $B \cong \IZ^m / T$, the hom-set $\Hom(A,B)$ is countable. Indeed, precomposition with the quotient map yields an injection $\Hom(A,B) \hookrightarrow \Hom(\IZ^n, B) \cong B^n$, and $B^n$ is countable. - property: ℵ₁-accessible - proof: The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\Ab_{\fg}$ has $\aleph_1$-filtered colimits. Since $\Ab_{\fg}$ is essentially small, there is a set $G$ such that every f.g. abelian group is isomorphic to one in $G$. So trivially it is also a $\aleph_1$-filtered colimit of such objects (take the constant diagram). Finally, every object is $\Ab_{\fg} = \Ab_{\fp}$ is finitely presentable in $\Ab$ and hence also in $\Ab_{\fg}$, a fortiori $\aleph_1$-presentable. + proof: The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\Ab_{\fg}$ has $\aleph_1$-filtered colimits. Since $\Ab_{\fg}$ is essentially small, there is a set $G$ such that every f.g. abelian group is isomorphic to one in $G$. So trivially it is also a $\aleph_1$-filtered colimit of such objects (take the constant diagram). Finally, every object is $\Ab_{\fg} = \Ab_{\fp}$ is finitely presentable in $\Ab$ and hence also in $\Ab_{\fg}$, a fortiori $\aleph_1$-presentable. - property: ℵ₁-cofiltered limits proof: A proof can be found here. diff --git a/databases/catdat/data/categories/BG_c.yaml b/databases/catdat/data/categories/BG_c.yaml index 09cf7148..8b75162c 100644 --- a/databases/catdat/data/categories/BG_c.yaml +++ b/databases/catdat/data/categories/BG_c.yaml @@ -13,6 +13,7 @@ tags: related_categories: - BG_f + - BG_u - BN satisfied_properties: diff --git a/databases/catdat/data/categories/BG_f.yaml b/databases/catdat/data/categories/BG_f.yaml index d1bcf885..5c66ae2f 100644 --- a/databases/catdat/data/categories/BG_f.yaml +++ b/databases/catdat/data/categories/BG_f.yaml @@ -14,6 +14,7 @@ tags: related_categories: - BG_c + - BG_u - BN satisfied_properties: diff --git a/databases/catdat/data/categories/BG_u.yaml b/databases/catdat/data/categories/BG_u.yaml new file mode 100644 index 00000000..74967878 --- /dev/null +++ b/databases/catdat/data/categories/BG_u.yaml @@ -0,0 +1,59 @@ +id: BG_u +name: delooping of an infinite uncountable group +notation: $BG$ +objects: a single object +morphisms: the elements of an infinite uncountable group $G$ +description: Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. In this example, we consider the case of an uncountable group $G$ (such as $G = \IR$). +nlab_link: https://ncatlab.org/nlab/show/delooping + +tags: + - algebra + - category theory + - single object + +related_categories: + - BG_f + - BG_c + - BN + +satisfied_properties: + - property: small + proof: This is trivial. + + - property: groupoid + proof: This is trivial. + + - property: connected + proof: This is trivial. + + - property: skeletal + proof: There is just one object. + + - property: generator + proof: The unique object is a generator for trivial reasons. + +unsatisfied_properties: + - property: locally finite + proof: This is because we choose $G$ to be infinite. + + - property: essentially countable + proof: This is because we choose $G$ to be uncountable. + +special_objects: {} + +special_morphisms: + isomorphisms: + description: every morphism + proof: It is a groupoid. + monomorphisms: + description: every morphism + proof: This is trivial. + epimorphisms: + description: every morphism + proof: This holds because it is a groupoid. + regular monomorphisms: + description: same as monomorphisms + proof: This is because the category is mono-regular. + regular epimorphisms: + description: same as isomorphisms + proof: This is because the category is left cancellative. diff --git a/databases/catdat/data/categories/FiltVect.yaml b/databases/catdat/data/categories/FiltVect.yaml new file mode 100644 index 00000000..a9c2bde2 --- /dev/null +++ b/databases/catdat/data/categories/FiltVect.yaml @@ -0,0 +1,119 @@ +id: FiltVect +name: category of filtered vector spaces +notation: $\FiltVect_K$ +objects: >- + A filtered vector space over a field $K$ consists of a vector space $V$ over $K$ together with an $\IZ$-indexed sequence of subspaces $F^n(V) \subseteq V$ satisfying $F^{n+1}(V) \subseteq F^n(V)$ for all $n \in \IZ$. + $$\cdots \subseteq F^1(V) \subseteq F^0(V) \subseteq F^{-1}(V) \subseteq \cdots \subseteq V$$ +morphisms: 'A morphism $(V,F) \to (W,G)$ is a linear map $f : V \to W$ satisfying $f_*(F^n(V)) \subseteq G^n(W)$ for all $n \in \IZ$. We call such morphisms filtered linear maps.' +description: The definition of a filtered object is available in any abelian category; in this entry, the ambient category is $\Vect_K$. We do not require the filtration to be exhaustive (i.e. $V = \bigcup_n F^n(V)$) or separated (i.e. $\bigcap_n F^n(V) = 0$). In the proofs below, we will often write $F$ for the filtration regardless of the vector space on which it is defined. +nlab_link: https://ncatlab.org/nlab/show/filtered+vector+space + +tags: + - algebra + +related_categories: + - Vect + +comments: + - 'The forgetful functor $U : \FiltVect \to \Vect$ has a left adjoint that equips a vector space with the trivial filtration. It also has a right adjoint that equips a vector space with the maximal filtration. In particular, it follows that $U$ preserves limits and colimits.' + - 'The filtration functor $F^n : \FiltVect \to \Vect$ has a left adjoint that equips a vector space $V$ with the filtration $F^n(V)=V$ and $F^{n+1}(V)=0$. In particular, it follows that $F^n$ preserves limits. However, it does not have a right adjoint. In fact, $F^n$ does not preserve coequalizers. On the other hand, $F^n$ does preserve filtered colimits; this can be verified using the concrete construction of filtered colimits.' + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\FiltVect \to \Vect$, and $\Vect$ is locally small. + + - property: preadditive + proof: We know that $\Vect$ is preadditive with pointwise operations. It is easy to check that the sum of two filtered linear maps is again a filtered linear map. Moreover, the additive inverse of a filtered linear map is again a filtered linear map. + + - property: kernels + proof: 'Let $f : (V,F) \to (W,F)$ be a filtered linear map. Equip the kernel $U \subseteq V$ of the underlying linear map $f : V \to W$ with the induced filtration $F^n(U) \coloneqq U \cap F^n(V)$. Then $(U,F)$ is a filtered vector space together with a filtered linear map $\iota : (U,F) \to (V,F)$, which is clearly the kernel of $f$ in $\FiltVect$.' + check_redundancy: false + + - property: cokernels + proof: 'Let $f : (V,F) \to (W,F)$ be a filtered linear map. Let $\pi : W \to C$ be the cokernel of the underlying linear map $f : V \to W$. Equip $C$ with the induced filtration $F^n(C) \coloneqq \pi_*(F^n(W))$. Then $(C,F)$ is a filtered vector space together with a filtered linear map $\pi : (W,F) \to (C,F)$, which is clearly the cokernel of $f$ in $\FiltVect$.' + check_redundancy: false + + - property: products + proof: 'Let $(V_i,F)_{i \in I}$ be a family of filtered vector spaces. Equip the product $\prod_{i \in I} V_i$ with the filtration $F^n(\prod_{i \in I} V_i) \coloneqq \prod_{i \in I} F^n(V_i)$. It is straightforward to check that this satisfies the universal property of products in $\FiltVect$.' + check_redundancy: false + + - property: coproducts + proof: 'Let $(V_i,F)_{i \in I}$ be a family of filtered vector spaces. Equip the direct sum $\bigoplus_{i \in I} V_i$ with the filtration $F^n(\bigoplus_{i \in I} V_i) \coloneqq \bigoplus_{i \in I} F^n(V_i)$. It is straightforward to check that this satisfies the universal property of coproducts in $\FiltVect$.' + check_redundancy: false + + - property: generator + proof: The vector space $K$ equipped with the trivial filtration $F^n(K) \coloneqq 0$ is a generator, since it represents the forgetful functor $\FiltVect \to \Set$. + check_redundancy: false + + - property: cogenerator + proof: It is straightforward to check that the vector space $K$ equipped with the maximal filtration $F^n(K) \coloneqq K$ is a cogenerator. + + - property: finitely accessible + proof: >- + Consider a filtered vector space $(V,F)$ such that $V$ is finite-dimensional and there exists some $N \in \IN$ with $F^N(V)=0$ (and hence $F^n(V)=0$ for all $n \geq N$). We claim that such an object is finitely presentable in $\FiltVect$: + + + Let $(W_i,F)$ be a filtered diagram of filtered vector spaces. Its colimit is the vector space $\colim_i W_i$ equipped with the filtration $F^n(\colim_i W_i) = \colim_i F^n(W_i)$. Let $f : (V,F) \to (\colim_i W_i,F)$ be a filtered linear map. The underlying linear map $f : V \to \colim_i W_i$ factors through some morphism $W_i \to \colim_i W_i$. Moreover, $f$ maps $F^n(V)$ into $\colim_i F^n(W_i)$ for every $n \in \IZ$. This condition is automatic when $n \geq N$, so assume that $n < N$. Since $V$ is finite-dimensional, the filtration stabilizes; that is, there exists some $M \in \IN$ such that $F^M(V) = F^n(V)$ for all $n \leq M$. Thus the filtered condition only needs to be checked in the finitely many degrees + $$n \in \{M,M+1,\cdots,N-1\}.$$ + Since the index category is filtered, there exists some index $j \geq i$ such that, for every relevant degree $n$, the map $f|_{F^n(V)}$ factors through $F^n(W_j)$. It follows that $f$ factors as a filtered linear map $(V,F) \to (W_j,F)$ followed by the colimit inclusion. This factorization is essentially unique because the corresponding statement holds in $\Vect$. + + + It remains to prove that every filtered vector space $(V,F)$ is a filtered colimit of such objects. First, it is clearly the filtered colimit of the subspaces $(V',F)$, where $V' \subseteq V$ is a finite-dimensional subspace equipped with the induced filtration. + Second, every filtered vector space $(V,F)$ is the filtered colimit of the spaces $(V,F_{< N})$ for $N \in \IN$, where + $$F_{< N}^n(V) \coloneqq \begin{cases} F^n(V) & n < N \\ 0 & n \geq N. \end{cases}$$ + Indeed, we have $F_{< N} \subseteq F_{< N+1}$, so that $\id_V : (V,F_{- + It remains to prove that regular epimorphisms are stable under pullbacks. This follows immediately from their classification below, from the fact that $F^n$ preserves limits, and from the regularity of $\Vect$. + + + In more detail, if $(V,F) \to (W,F)$ is a regular epimorphism and $(U,F) \to (W,F)$ is any morphism, then $(V,F) \times_{(W,F)} (U,F) \to (U,F)$ is a regular epimorphism, since $V \times_W U \to U$ is surjective and, for every $n \in \IZ$, the restricted map + $$F^n(V \times_W U) = F^n(V) \times_{F^n(W)} F^n(U) \to F^n(U)$$ + is surjective. + - property: coregular + proof: >- + It remains to prove that regular monomorphisms (as classified below) are stable under pushouts. Let $i : (U,F) \to (V,F)$ be a regular monomorphism, i.e. $i$ is injective and $F^n(U) = i^*(F^n(V))$. Let $f : (U,F) \to (W,F)$ be any morphism. We must prove that the canonical morphism $(W,F) \to (V,F) \oplus_{(U,F)} (W,F)$ is a regular monomorphism. It is certainly injective, since the forgetful functor to $\Vect$ preserves colimits and $\Vect$ is abelian, and hence coregular. Now suppose that $w \in W$ is an element whose image $[0,w] \in V \oplus_U W$ lies in $F^n(V \oplus_U W)$; we must show that $w \in F^n(W)$. + Since, by the construction of colimits in $\FiltVect$, the subspace $F^n(V \oplus_U W)$ is the sum of the images of $F^n(V)$ and $F^n(W)$, there exist $v \in F^n(V)$ and $w' \in F^n(W)$ such that $[0,w] = [v,w']$. This means that there exists some $u \in U$ with $v = i(u)$ and $w = f(u) + w'$. Then $u \in F^n(U)$ because $i(u) \in F^n(V)$. Hence $f(u) \in F^n(W)$, and therefore $w = f(u) + w' \in F^n(W)$. + +unsatisfied_properties: + - property: skeletal + proof: This is straightforward. + + - property: balanced + proof: 'Take any non-trivial vector space $V$ and consider the two filtrations defined by $F^n(V) \coloneqq 0$ and $G^n(V) \coloneqq V$ for all $n \in \IZ$. Then $\id_V : (V,F) \to (V,G)$ is both a monomorphism and an epimorphism of filtered vector spaces, but it is not an isomorphism.' + + - property: CSP + proof: The canonical filtered linear map $\bigoplus_{n \geq 0} (K,0) \to \prod_{n \geq 0} (K,0)$ is not an epimorphism, since its underlying linear map is the canonical map $\bigoplus_{n \geq 0} K \to \prod_{n \geq 0} K$, which is not surjective. + +special_objects: + initial object: + description: the trivial vector space equipped with the unique filtration + terminal object: + description: the trivial vector space equipped with the unique filtration + coproducts: + description: direct sums of the underlying vector spaces equipped with the filtration $F^n(\bigoplus_i V_i) \coloneqq \bigoplus_i F^n(V_i)$ + products: + description: direct products of the underlying vector spaces equipped with the filtration $F^n(\prod_i V_i) \coloneqq \prod_i F^n(V_i)$ + +special_morphisms: + isomorphisms: + description: 'A filtered linear map $f : (V,F) \to (W,G)$ is an isomorphism if $f : V \to W$ is bijective and $f_*(F^n(V)) = G^n(W)$ for all $n \in \IZ$.' + proof: This is straightforward to verify. + + monomorphisms: + description: injective filtered linear maps + proof: For the non-trivial direction, the forgetful functor $\FiltVect \to \Set$ is representable (by $K$ equipped with the trivial filtration), and therefore preserves monomorphisms. + + epimorphisms: + description: surjective filtered linear maps + proof: We saw above that the category has cokernels, and that these are preserved by the forgetful functor to $\Vect$. Moreover, a morphism is an epimorphism if and only if its cokernel is zero, and a filtered vector space is zero if and only if its underlying vector space is zero. Therefore, the claim follows from the classification of epimorphisms in $\Vect$. + + regular monomorphisms: + description: 'A filtered linear map $f : (V,F) \to (W,G)$ is a regular monomorphism if and only if $f : V \to W$ is injective and $F^n(V) = f^*(G^n(W))$ for all $n \in \IZ$.' + proof: 'Every kernel (and hence every equalizer) satisfies this property by the construction of kernels. Conversely, suppose that $f : (V,F) \to (W,G)$ is a filtered linear map satisfying this condition. Then $f$ induces an isomorphism between $(V,F)$ and $(U,G)$, where $U \coloneqq \im(f) \subseteq W$ is equipped with the induced filtration $G^n(U) \coloneqq U \cap G^n(W)$. Endow $W/U$ with the induced filtration $G^n(W/U) \coloneqq \pi_*(G^n(W))$, where $\pi : W \to W/U$ is the quotient map. Then $\pi : (W,G) \to (W/U,G)$ is a filtered linear map, and by the general construction of kernels, its kernel is the vector space $U$ equipped with the induced filtration. Hence, $f : (V,F) \to (W,G)$ is a kernel of $\pi : (W,G) \to (W/U,G)$.' + + regular epimorphisms: + description: 'A filtered linear map $f : (V,F) \to (W,G)$ is a regular epimorphism if and only if $f : V \to W$ is surjective and $G^n(W) = f_*(F^n(V))$ for all $n \in \IZ$.' + proof: >- + Every cokernel (and hence every coequalizer) satisfies this property by the construction of cokernels. Conversely, suppose that $f : (V,F) \to (W,G)$ is a filtered linear map satisfying this condition. Let $U \subseteq V$ be the kernel of the underlying linear map $f : V \to W$, equipped with the induced filtration $F^n(U) \coloneqq U \cap F^n(V)$. The inclusion $(U,F) \to (V,F)$ is a filtered linear map. By the general construction of cokernels, its cokernel is $(V/U,F)$, where $F^n(V/U) \coloneqq \pi_*(F^n(V))$ and $\pi : V \to V/U$ is the quotient map. It remains to observe that the induced isomorphism of vector spaces $h : V/U \to W$, characterized by $h \circ \pi = f$, is in fact an isomorphism of filtered vector spaces. Indeed, + $$h_*(F^n(V/U)) = h_*(\pi_*(F^n(V))) = f_*(F^n(V)) = G^n(W).$$ diff --git a/databases/catdat/data/categories/FinVect_c.yaml b/databases/catdat/data/categories/FinVect_c.yaml new file mode 100644 index 00000000..d5443984 --- /dev/null +++ b/databases/catdat/data/categories/FinVect_c.yaml @@ -0,0 +1,80 @@ +# TODO: fix duplication with FinVect_u and FinVect_f +id: FinVect_c +name: category of finite-dimensional vector spaces [countable field] +notation: $\FinVect_K$ +objects: finite-dimensional vector spaces over a countably infinite field $K$ +morphisms: linear maps +description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. In this entry, we assume that $K$ is countably infinite (e.g. $K = \IQ$) in order to determine all properties of this category. +nlab_link: https://ncatlab.org/nlab/show/FinDimVect + +tags: + - algebra + +related_categories: + - Vect + - FinVect_u + - FinVect_f + - Ab_fg + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + + - property: essentially countable + proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a countable set. + + - property: generator + proof: The forgetful functor $\FinVect_K \to \Set$ is faithful and represented by $K$. Hence, $K$ is a generator. + + - property: split abelian + proof: This follows directly from the corresponding fact for $\Vect_K$. + + - property: self-dual + proof: The functor $V \mapsto V^*$ defines an equivalence of categories $\FinVect_K^{\op} \simeq \FinVect_K$. In fact, the natural map $V \to V^{**}$, $v \mapsto (\omega \mapsto \omega(v))$ is an isomorphism by standard linear algebra. + + - property: ℵ₁-accessible + proof: 'The inclusion $\FinVect_K \hookrightarrow \Vect_K$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\FinVect_K$ has $\aleph_1$-filtered colimits. Moreover, every object in $\FinVect_K$ is $\aleph_1$-presentable: it is isomorphic to some $K^n$, which is finitely presentable in $\Vect_K$, hence $\aleph_1$-presentable in $\Vect_K$, and therefore also $\aleph_1$-presentable in $\FinVect_K$.' + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: small + proof: This is trivial. + + - property: countable + proof: This is trivial. + + - property: locally finite + proof: The hom-set $\Hom(K,K) \cong K$ is infinite by assumption. + +special_objects: + initial object: + description: the trivial vector space + terminal object: + description: the trivial vector space + coproducts: + description: '[finite case] direct sums' + products: + description: '[finite case] direct products with pointwise operations' + +special_morphisms: + isomorphisms: + description: bijective linear maps + proof: This is easy to check. + + monomorphisms: + description: injective linear maps + proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. + + epimorphisms: + description: surjective linear maps + proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' + + regular monomorphisms: + description: same as monomorphisms + proof: This holds because the category is abelian. + + regular epimorphisms: + description: same as epimorphisms + proof: This holds because the category is abelian. diff --git a/databases/catdat/data/categories/FinVect_f.yaml b/databases/catdat/data/categories/FinVect_f.yaml new file mode 100644 index 00000000..01197a41 --- /dev/null +++ b/databases/catdat/data/categories/FinVect_f.yaml @@ -0,0 +1,80 @@ +# TODO: fix duplication with FinVect_u and FinVect_c +id: FinVect_f +name: category of finite-dimensional vector spaces [finite field] +notation: $\FinVect_K$ +objects: finite-dimensional vector spaces over a countably infinite field $K$ +morphisms: linear maps +description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. In this entry, we assume that $K$ is finite (e.g. $K = \IF_2$) in order to determine all properties of this category. +nlab_link: https://ncatlab.org/nlab/show/FinDimVect + +tags: + - algebra + +related_categories: + - Vect + - FinVect_u + - FinVect_c + - Ab_fg + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + + - property: essentially countable + proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a finite, hence countable set. + + - property: locally finite + proof: Each hom-set $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is finite by assumption. + + - property: generator + proof: The forgetful functor $\FinVect_K \to \Set$ is faithful and represented by $K$. Hence, $K$ is a generator. + + - property: split abelian + proof: This follows directly from the corresponding fact for $\Vect_K$. + + - property: self-dual + proof: The functor $V \mapsto V^*$ defines an equivalence of categories $\FinVect_K^{\op} \simeq \FinVect_K$. In fact, the natural map $V \to V^{**}$, $v \mapsto (\omega \mapsto \omega(v))$ is an isomorphism by standard linear algebra. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: small + proof: This is trivial. + + - property: countable + proof: This is trivial. + + - property: thin + proof: This is trivial. + +special_objects: + initial object: + description: the trivial vector space + terminal object: + description: the trivial vector space + coproducts: + description: '[finite case] direct sums' + products: + description: '[finite case] direct products with pointwise operations' + +special_morphisms: + isomorphisms: + description: bijective linear maps + proof: This is easy to check. + + monomorphisms: + description: injective linear maps + proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. + + epimorphisms: + description: surjective linear maps + proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' + + regular monomorphisms: + description: same as monomorphisms + proof: This holds because the category is abelian. + + regular epimorphisms: + description: same as epimorphisms + proof: This holds because the category is abelian. diff --git a/databases/catdat/data/categories/FinVect_u.yaml b/databases/catdat/data/categories/FinVect_u.yaml new file mode 100644 index 00000000..42ce4e6e --- /dev/null +++ b/databases/catdat/data/categories/FinVect_u.yaml @@ -0,0 +1,80 @@ +# TODO: fix duplication with FinVect_c and FinVect_f +id: FinVect_u +name: category of finite-dimensional vector spaces [uncountable field] +notation: $\FinVect_K$ +objects: finite-dimensional vector spaces over an uncountable field $K$ +morphisms: linear maps +description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. In this entry, we assume that $K$ is uncountable (e.g. $K = \IR$) in order to determine all properties of this category. +nlab_link: https://ncatlab.org/nlab/show/FinDimVect + +tags: + - algebra + +related_categories: + - Vect + - FinVect_c + - FinVect_f + - Ab_fg + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + + - property: essentially small + proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a set. + + - property: generator + proof: The forgetful functor $\FinVect_K \to \Set$ is faithful and represented by $K$. Hence, $K$ is a generator. + + - property: split abelian + proof: This follows directly from the corresponding fact for $\Vect_K$. + + - property: self-dual + proof: The functor $V \mapsto V^*$ defines an equivalence of categories $\FinVect_K^{\op} \simeq \FinVect_K$. In fact, the natural map $V \to V^{**}$, $v \mapsto (\omega \mapsto \omega(v))$ is an isomorphism by standard linear algebra. + + - property: ℵ₁-accessible + proof: 'The inclusion $\FinVect_K \hookrightarrow \Vect_K$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\FinVect_K$ has $\aleph_1$-filtered colimits. Moreover, every object in $\FinVect_K$ is $\aleph_1$-presentable: it is isomorphic to some $K^n$, which is finitely presentable in $\Vect_K$, hence $\aleph_1$-presentable in $\Vect_K$, and therefore also $\aleph_1$-presentable in $\FinVect_K$.' + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: small + proof: This is trivial. + + - property: essentially countable + proof: The hom-set $\Hom(K,K) \cong K$ is uncountable by assumption. + + - property: locally finite + proof: The hom-set $\Hom(K,K) \cong K$ is infinite by assumption. + +special_objects: + initial object: + description: the trivial vector space + terminal object: + description: the trivial vector space + coproducts: + description: '[finite case] direct sums' + products: + description: '[finite case] direct products with pointwise operations' + +special_morphisms: + isomorphisms: + description: bijective linear maps + proof: This is easy to check. + + monomorphisms: + description: injective linear maps + proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. + + epimorphisms: + description: surjective linear maps + proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' + + regular monomorphisms: + description: same as monomorphisms + proof: This holds because the category is abelian. + + regular epimorphisms: + description: same as epimorphisms + proof: This holds because the category is abelian. diff --git a/databases/catdat/data/categories/Vect.yaml b/databases/catdat/data/categories/Vect.yaml index 68e5fc6b..3d153aa0 100644 --- a/databases/catdat/data/categories/Vect.yaml +++ b/databases/catdat/data/categories/Vect.yaml @@ -12,6 +12,11 @@ tags: related_categories: - R-Mod - R-Mod_div + - FinVect_f + - FinVect_c + - FinVect_u + - FiltVect + - FreeAb satisfied_properties: - property: locally small diff --git a/databases/catdat/data/category-properties/essentially countable.yaml b/databases/catdat/data/category-properties/essentially countable.yaml index 2d24c3d6..39d04145 100644 --- a/databases/catdat/data/category-properties/essentially countable.yaml +++ b/databases/catdat/data/category-properties/essentially countable.yaml @@ -1,6 +1,6 @@ id: essentially countable relation: is -description: A category is essentially countable if it is equivalent to a countable category. +description: A category is essentially countable if it is equivalent to a countable category. This means that up to isomorphism there is only a countable collection of objects, and for every pair of objects $A,B$ the collection $\Hom(A,B)$ is countable. dual_property: essentially countable invariant_under_equivalences: true diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 365443b0..64b607a5 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -69,6 +69,8 @@ \Ab: \mathbf{Ab} \Grp: \mathbf{Grp} \Vect: \mathbf{Vect} +\FinVect: \mathbf{FinVect} +\FiltVect: \mathbf{FiltVect} \Ring: \mathbf{Ring} \Alg: \mathbf{Alg} \CRing: \mathbf{CRing} diff --git a/databases/catdat/scripts/expected-data/decided-categories.json b/databases/catdat/scripts/expected-data/decided-categories.json index e6448d1f..6764d2e0 100644 --- a/databases/catdat/scripts/expected-data/decided-categories.json +++ b/databases/catdat/scripts/expected-data/decided-categories.json @@ -15,6 +15,9 @@ "Top", "Top*", "Vect", + "FinVect_f", + "FinVect_c", + "FinVect_u", "walking_morphism", "walking_pair" ]