Add two categories of finitely generated projective modules

.cspell.json

@@ -39,6 +39,7 @@
 		"bijection",
 		"bijections",
 		"bijective",
+		"bimodule",
 		"biproduct",
 		"biproducts",
 		"Birkhoff",

content/free-cocompletion.md

@@ -173,7 +173,7 @@ Let $F \rightrightarrows G$ be a cocongruence in $\widehat{\C}$. Since the inclu
 $$F \rightrightarrows F \sqcup_E F,$$
 where $E \coloneqq \eq(F \rightrightarrows G)$ is the objectwise defined equalizer in $[\C^{\op},\Set]$. We would be done if $E$ were small, which however is not the case in general. But we can prove that $E$ is a quotient of a small presheaf, or equivalently, a quotient of a coproduct of representable presheaves, which is sufficient, since any epimorphism $E' \to E$ satisfies $F \sqcup_E F = F \sqcup_{E'} F$. (Such presheaves are also called _petty_ in the literature.)
 
-We view the pushout $P := F \sqcup_E F$ as the union of two copies $F_1,F_2$ of $F$ with $F_1 \cap F_2 = E$. In particular, we regard $E,F_1,F_2$ as sub-presheaves of $P$. For a morphism $f$ in $\C$, we write $f^*$ instead of $P(f)$.
+We view the pushout $P \coloneqq F \sqcup_E F$ as the union of two copies $F_1,F_2$ of $F$ with $F_1 \cap F_2 = E$. In particular, we regard $E,F_1,F_2$ as sub-presheaves of $P$. For a morphism $f$ in $\C$, we write $f^*$ instead of $P(f)$.
 
 Since $P \cong G$ is small, its category of elements $\int P$ has a finally small subcategory $\K$. Let $K \subseteq \Ob(\C)$ be the set of objects that appear in $\K$. We claim that
 $$\{(A,a) : A \in K, \, a \in E(A)\}$$

database/data/categories/Ab_fg.yaml

@@ -13,10 +13,11 @@ related:
   - Ab
   - FinAb
   - FinVect_c
+  - FreeAb_fg
 
 satisfied_properties:
   - property: locally small
-    proof: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small.
+    proof: There is a forgetful functor $\Ab_{fg} \to \Set$ and $\Set$ is locally small.
 
   - property: abelian
     proof: This follows from the fact for abelian groups and the fact that subgroups of finitely generated abelian groups are also finitely generated.
@@ -29,7 +30,8 @@ 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 <a href="https://mathoverflow.net/questions/400763/" target="_blank">MO/400763</a>. 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 <a href="https://mathoverflow.net/questions/400763/" target="_blank">MO/400763</a>. 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$, a fortiori $\aleph_1$-presentable, and hence also $\aleph_1$-presentable in $\Ab_{\fg}$.
+    label: Ab_fg_aleph1-accessible
 
   - property: ℵ₁-cofiltered limits
     proof: >-

database/data/categories/FinVect_c.yaml

@@ -13,6 +13,7 @@ tags:
 related:
   - Vect
   - Ab_fg
+  - FreeAb_fg
 
 satisfied_properties:
   - property: essentially countable

database/data/categories/FinVect_u.yaml

@@ -13,6 +13,7 @@ tags:
 related:
   - Vect
   - Ab_fg
+  - Proj_fg(Re)
 
 satisfied_properties: []
 

database/data/categories/FreeAb.yaml

@@ -3,7 +3,7 @@ name: category of free abelian groups
 notation: $\FreeAb$
 objects: free abelian groups
 morphisms: group homomorphisms
-description: This is the full subcategory of $\Ab$ that consists of the <a href="https://ncatlab.org/nlab/show/free+abelian+group" target="_blank">free abelian groups</a>.
+description: This is the full subcategory of $\Ab$ consisting of the <a href="https://ncatlab.org/nlab/show/free+abelian+group" target="_blank">free abelian groups</a>. Since $\IZ$ is a principal ideal domain, these coincide with the <a href="https://ncatlab.org/nlab/show/projective+module" target="_blank">projective</a> $\IZ$-modules, so that $\FreeAb \cong \Proj(\IZ)$.
 nlab_link: null
 
 tags:
@@ -12,6 +12,7 @@ tags:
 related:
   - Ab
   - TorsFreeAb
+  - FreeAb_fg
 
 satisfied_properties:
   - property: locally small
@@ -23,6 +24,10 @@ satisfied_properties:
   - property: coproducts
     proof: This is is because free abelian groups are closed under direct sums of abelian groups.
 
+  - property: equalizers
+    proof: This follows from the fact that a subgroup of a free abelian group is again free abelian.
+    check_redundancy: false
+
   - property: extremal generator
     proof: The group $\IZ$ is an extremal generator even in <a href="/category/Grp">$\Grp$</a>. Now apply Lemma 10 <a href="/content/subcategories">here</a>.
     references:
@@ -37,11 +42,12 @@ satisfied_properties:
   - property: well-copowered
     proof: See <a href="https://math.stackexchange.com/questions/5025660" target="_blank">MSE/5025660</a>.
 
+  - property: coequalizers of kernel pairs
+    proof: 'Let $f : A \to B$ be a homomorphism of free abelian groups. The coequalizer of its kernel pair $A \times_B A \rightrightarrows A$ in $\Ab$ is the image $\im(f)$. As a subgroup of $B$, it is also free abelian. Then it is also the coequalizer of the kernel pair in $\FreeAb$.'
+    check_redundancy: false
+
   - property: regular
-    proof: |-
-      This follows formally from the fact that <a href="/category/Ab">$\Ab$</a> is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the <a href="https://ncatlab.org/nlab/show/regular+category">nLab</a> it suffices to prove that there are (reg epi, mono)-factorizations that are stable under pullbacks. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup of $B$, hence free abelian, and $A \to C$ is surjective. Clearly, surjective homomorphisms are stable under pullbacks. It remains to show that they coincide with the regular epimorphisms.
-      (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\Ab$. Since $A \times_B A$ is free abelian (as a subgroup of $A \times A$), $f$ is also a coequalizer in $\FreeAb$.
-      (2) If $f : A \to B$ is a regular epimorphism in $\FreeAb$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective.
+    proof: It remains to prove that regular epimorphisms are stable under pullback. This is clear since they coincide with the surjective homomorphisms (see below).
 
 unsatisfied_properties:
   - property: balanced
@@ -79,13 +85,13 @@ special_morphisms:
     proof: It is a full subcategory of $\Ab$, for which we know that isomorphisms are bijective homomorphisms.
   monomorphisms:
     description: injective homomorphisms
-    proof: 'Let $f : A \to B$ be a monomorphism of free abelian groups. Let $a \in A$ be in the kernel of $a$. Then we may view $a$ as a morphism $a : \IZ \to A$ with $f \circ a = 0$, and $\IZ$ is free. Hence, $a = 0$.'
+    proof: The non-trivial direction follows from the observation that the forgetful functor to $\Set$ is representable (by $\IZ$), hence preserves monomorphisms.
   epimorphisms:
     description: 'homomorphisms $f : A \to B$ with the property that $f(A)$ is not contained in a proper direct summand of $B$'
-    proof: 'Let $f : A \to B$ be a morphism of free abelian groups such that $f(A)$ is not contained in a proper direct summand of $B$. Then $f$ is an epimorphism: If $t : B \to C$ is a morphism with $t \circ f = 0$, we want to show $t = 0$. Since the image of $t$ is free abelian (as a subgroup of $B$), we may assume that $t$ is surjective. Since $C$ is free, $t$ splits, so its kernel $K$ is a direct summand of $B$ (Splitting Lemma). It contains $f(A)$ because of $t \circ f = 0$. By assumption, $K = B$, so that $t = 0$. Conversely, assume that $f : A \to B$ is an epimorphism, and that $f(A)$ is contained in a direct summand $K$ of $B$. Let $L$ be a complement of $B$ (which is free abelian) and let $p : B \to L$ be the projection. Then $t \circ f = 0$, so $t = 0$. But then $L = 0$, which means $K = B$.'
+    proof: 'Let $f : A \to B$ be a morphism of free abelian groups such that $f(A)$ is not contained in a proper direct summand of $B$. Then $f$ is an epimorphism: If $t : B \to C$ is a morphism with $t \circ f = 0$, we want to show $t = 0$. Since the image of $t$ is free abelian (as a subgroup of $B$), we may assume that $t$ is surjective. Since $C$ is free, $t$ splits, so by the splitting lemma its kernel $K$ is a direct summand of $B$. It contains $f(A)$ because of $t \circ f = 0$. By assumption, $K = B$, so that $t = 0$. Conversely, assume that $f : A \to B$ is an epimorphism, and that $f(A)$ is contained in a direct summand $K$ of $B$. Let $L$ be a complement of $B$ (which is free abelian) and let $p : B \to L$ be the projection. Then $p \circ f = 0$, so $p = 0$. But then $L = 0$, which means $K = B$.'
   regular monomorphisms:
     description: 'injective homomorphisms $f : A \to B$ with the property that $B/f(A)$ is free abelian (which are automatically split monomorphisms)'
-    proof: 'If $f$ is injective and $B/f(A)$ is free abelian, then $f$ is a kernel of the projection $B \to B/f(A)$. Since $B/f(A)$ is free abelian, the sequence $0 \to A \to B \to B/f(A) \to 0$ splits, so by the splitting lemma, $f$ is a split monomorphism. Conversely, if $f$ is a kernel of some homomorphism $g : B \to C$ of free abelian groups, by applying $\Hom(\IZ,-)$ we see that it is also the kernel in $\Ab$. In particular, $f$ is injective, and the quotient $B/f(A)$ embeds into $C$ and is therefore free abelian.'
+    proof: 'If $f$ is injective and $B/f(A)$ is free abelian, then $f$ is a kernel of the canonical projection $B \to B/f(A)$. Since $B/f(A)$ is free abelian, the sequence $0 \to A \to B \to B/f(A) \to 0$ splits, so by the splitting lemma, $f$ is a split monomorphism. Conversely, if $f$ is a kernel of some homomorphism $g : B \to C$ of free abelian groups, by applying $\Hom(\IZ,-)$ we see that it is also the kernel in $\Ab$. In particular, $f$ is injective, and the quotient $B/f(A)$ embeds into $C$ and is therefore free abelian.'
   regular epimorphisms:
     description: surjective homomorphisms (which are automatically split epimorphisms)
-    proof: Regular homomorphisms coincide with surjective homomorphisms by the proof above that $\FreeAb$ is regular. They are automatically split because their codomain is free abelian.
+    proof: 'If $f : A \to B$ is a surjective homomorphism in $\FreeAb$ with kernel $K$, then $f$ is the cokernel of $K \hookrightarrow A$ in $\Ab$. Since $K$ is free abelian, this remains true in $\FreeAb$. Moreover, $f$ splits since $B$ is projective. Conversely, assume that $f : A \to B$ is a regular epimorphism in $\FreeAb$ and hence the cokernel of some homomorphism $g : C \to A$ in $\FreeAb$. Consider the image factorization $A \to \im(f) \hookrightarrow B$ in $\Ab$. Here, $\im(f)$ is also free abelian. Since $\im(f) \hookrightarrow B$ is a monomorphism in $\FreeAb$ and $f$ is a regular, hence extremal, epimorphism, $\im(f) \hookrightarrow B$ is an isomorphism. Thus, $f$ is surjective.'

database/data/categories/FreeAb_fg.yaml

@@ -0,0 +1,95 @@
+id: FreeAb_fg
+name: category of finitely generated free abelian groups
+notation: $\FreeAb_\fg$
+objects: finitely generated free abelian groups
+morphisms: group homomorphisms
+description: This is the full subcategory of $\Ab$ consisting of the <a href="https://ncatlab.org/nlab/show/free+abelian+group" target="_blank">free abelian groups</a> that are also <a href="https://ncatlab.org/nlab/show/finitely+generated+group" target="_blank">finitely generated</a>. Equivalently, it is the category $\Proj_\fg(\IZ)$ of finitely generated <a href="https://ncatlab.org/nlab/show/projective+module" target="_blank">projective</a> $\IZ$-modules. Every object is isomorphic to $\IZ^n$ for a unique $n \in \IN$.
+nlab_link: null
+
+tags:
+  - algebra
+
+related:
+  - Ab
+  - TorsFreeAb
+  - Ab_fg
+  - FreeAb
+  - FinVect_c
+  - Proj_fg(Re)
+
+satisfied_properties:
+  - property: locally small
+    proof: The category is a full subcategory of $\Ab$, which is locally small.
+
+  - property: essentially countable
+    proof: Every object is isomorphic to one of the countably many groups $\IZ^n$, and the set $\Hom(\IZ^n,\IZ^m) \cong M_{m \times n}(\IZ)$ is countable.
+
+  - property: additive
+    proof: The category is closed under finite direct sums in $\Ab$, which is additive.
+
+  - property: equalizers
+    proof: This follows from the standard fact that every subgroup of a finitely generated free abelian group is again finitely generated and free abelian.
+    check_redundancy: false
+
+  - property: extremal generator
+    proof: The group $\IZ$ is an extremal generator, even in $\Ab$.
+
+  - property: self-dual
+    proof: More generally, if $R$ is a commutative ring, $\Proj_\fg(R)$ is self-dual, as proven <a href="/category/Proj_fg(Re)">here</a>.
+    references:
+      - proj_fg_self-dual
+
+  - property: regular
+    proof: We already know that the category is finitely complete and self-dual, hence also finitely cocomplete. It remains to prove that regular epimorphisms are stable under pullback. This is clear since they coincide with the surjective homomorphisms (see below).
+
+  - property: ℵ₁-accessible
+    proof: >-
+      The proof is very similar to the proof for <a href="/category/Ab_fg">$\Ab_\fg$</a>. The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by <a href="https://mathoverflow.net/questions/400763/" target="_blank">MO/400763</a>. Furthermore, the inclusion $\TorsFreeAb \hookrightarrow \Ab$ is clearly closed under $\aleph_0$-filtered colimits, and hence under $\aleph_1$-filtered colimits. Since $\FreeAb_\fg = \Ab_\fg \cap \TorsFreeAb$, it follows that $\FreeAb_\fg \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits. In particular, $\FreeAb_\fg$ has $\aleph_1$-filtered colimits. Every finitely generated free abelian group is isomorphic to one in the set $\{\IZ^n : n \in \IN\}$, and each $\IZ^n$ is finitely presentable in $\Ab$, hence $\aleph_1$-presentable, and therefore also $\aleph_1$-presentable in $\FreeAb_\fg$.
+
+      More generally, if $R$ is a left Noetherian ring, then $\Proj_\fg(R)$ is $\aleph_1$-accessible, as proven <a href="/category/Proj_fg(Re)">here</a>.
+    references:
+      - Ab_fg_aleph1-accessible
+      - Proj_fg_aleph1-accessible
+
+unsatisfied_properties:
+  - property: skeletal
+    proof: This is trivial.
+
+  - property: small
+    proof: Even the collection of trivial groups is not a set.
+
+  - property: countable
+    proof: Even the collection of trivial groups is not countable.
+
+  - property: locally finite
+    proof: The set $\Hom(\IZ,\IZ) \cong \IZ$ is not finite.
+
+  - property: balanced
+    proof: 'The homomorphism $2 : \IZ \to \IZ$ is a counterexample.'
+
+special_objects:
+  initial object:
+    description: trivial group
+  terminal object:
+    description: trivial group
+  coproducts:
+    description: '[finite case] direct sums'
+  products:
+    description: '[finite case] direct sums'
+
+special_morphisms:
+  isomorphisms:
+    description: bijective homomorphisms
+    proof: We can copy the proof from <a href="/category/FreeAb">$\FreeAb$</a>.
+  monomorphisms:
+    description: injective homomorphisms
+    proof: We can copy the proof from <a href="/category/FreeAb">$\FreeAb$</a>.
+  epimorphisms:
+    description: 'homomorphisms $f : A \to B$ such that $f(A)$ is not contained in a proper direct summand of $B$'
+    proof: We can copy the proof from <a href="/category/FreeAb">$\FreeAb$</a>.
+  regular monomorphisms:
+    description: 'injective homomorphisms $f : A \to B$ such that $B/f(A)$ is torsion-free  (and these are automatically split monomorphisms)'
+    proof: We can copy the proof from <a href="/category/FreeAb">$\FreeAb$</a>, since a finitely generated torsion-free abelian group is free.
+  regular epimorphisms:
+    description: surjective homomorphisms (which are automatically split epimorphisms)
+    proof: We can copy the proof from <a href="/category/FreeAb">$\FreeAb$</a>.