From 15bfd7e18ba0603053c0cc5157922e2b663171dc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 3 Sep 2026 17:02:45 +0200 Subject: [PATCH 1/6] fix schema for proof references --- database/schema/002_properties.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/schema/002_properties.sql b/database/schema/002_properties.sql index d751a6829..439aaae8d 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -78,7 +78,7 @@ CREATE TABLE proof_references ( property_id TEXT NOT NULL, type TEXT NOT NULL, reference TEXT NOT NULL, - PRIMARY KEY (structure_id, property_id), + PRIMARY KEY (structure_id, property_id, reference), FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, FOREIGN KEY (property_id, type) From 31d2565c8df7e662acd380c752e21adbc30173b7 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 2 Sep 2026 22:00:04 +0200 Subject: [PATCH 2/6] add the category of finitely generated free abelian groups --- database/data/categories/Ab_fg.yaml | 6 +- database/data/categories/FinVect_c.yaml | 1 + database/data/categories/FreeAb.yaml | 1 + database/data/categories/FreeAb_fg.yaml | 94 +++++++++++++++++++++++++ 4 files changed, 100 insertions(+), 2 deletions(-) create mode 100644 database/data/categories/FreeAb_fg.yaml diff --git a/database/data/categories/Ab_fg.yaml b/database/data/categories/Ab_fg.yaml index 324d7e15f..1a3b79624 100644 --- a/database/data/categories/Ab_fg.yaml +++ b/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 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$, a fortiori $\aleph_1$-presentable, and hence also $\aleph_1$-presentable in $\Ab_{\fg}$. + label: Ab_fg_aleph1-accessible - property: ℵ₁-cofiltered limits proof: >- diff --git a/database/data/categories/FinVect_c.yaml b/database/data/categories/FinVect_c.yaml index 57d73dd52..788fcd601 100644 --- a/database/data/categories/FinVect_c.yaml +++ b/database/data/categories/FinVect_c.yaml @@ -13,6 +13,7 @@ tags: related: - Vect - Ab_fg + - FreeAb_fg satisfied_properties: - property: essentially countable diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 1fbd065ca..66b1aac0e 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -12,6 +12,7 @@ tags: related: - Ab - TorsFreeAb + - FreeAb_fg satisfied_properties: - property: locally small diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml new file mode 100644 index 000000000..ff6c4fe57 --- /dev/null +++ b/database/data/categories/FreeAb_fg.yaml @@ -0,0 +1,94 @@ +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 free abelian groups that are also finitely generated. Equivalently, it is the category of finitely generated projective $\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 + +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: regular + proof: It remains to prove that regular epimorphisms are stable under pullback. This is clear since they coincide with the surjective homomorphisms (see below). + + - property: self-dual + proof: >- + The functor $\Hom(-,\IZ) : \FreeAb_\fg^{\op} \to \Set$ lifts to an additive functor $$\underline{\Hom}(-,\IZ) : \FreeAb_\fg^{\op} \to \Ab.$$ + It corestricts to $\FreeAb_\fg$ because of $\underline{\Hom}(\IZ^n,\IZ) \cong \IZ^n$. The functor + $$\underline{\Hom}(-,\IZ) : \FreeAb_\fg^{\op} \to \FreeAb_\fg$$ + dualizes to a functor in the other direction, and we claim that these are inverse to each other. For this, it suffices to prove that the natural homomorphism + $$A \to \underline{\Hom}(\underline{\Hom}(A,\IZ),\IZ)$$ + defined by $a \mapsto (\varphi \mapsto \varphi(a))$ is an isomorphism. The collection of abelian groups for which this is true is closed under finite direct sums (since both sides are additive functors), and it contains $\IZ$ by a direct calculation. Therefore, it contains every $\IZ^n$. + + - property: ℵ₁-accessible + proof: 'The proof is very similar to the proof for $\Ab_\fg$. The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. 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$.' + references: + - Ab_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 $\FreeAb$. + monomorphisms: + description: injective homomorphisms + proof: We can copy the proof from $\FreeAb$. + 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 $\FreeAb$. + regular monomorphisms: + description: 'injective homomorphisms $f : A \to B$ such that $B/f(A)$ is free abelian (and hence which are automatically split monomorphisms)' + proof: We can copy the proof from $\FreeAb$. + regular epimorphisms: + description: surjective homomorphisms (which are automatically split epimorphisms) + proof: 'If $f : A \to B$ is a surjective homomorphism in $\FreeAb_\fg$ with kernel $K$, then $f$ is the cokernel of $K \hookrightarrow A$ in $\Ab$. Since $K$ is finitely generated and free abelian, this remains true in $\FreeAb_\fg$. Moreover, $f$ splits since $B$ is projective. Conversely, assume that $f : A \to B$ is a regular epimorphism in $\FreeAb_\fg$ and hence the cokernel of some homomorphism $g : C \to A$ in $\FreeAb_\fg$. Consider the image factorization $A \to \im(f) \hookrightarrow B$ in $\Ab$. Here, $\im(f)$ is also finitely generated and free abelian. Since $\im(f) \hookrightarrow B$ is a monomorphism in $\FreeAb_\fg$ and $f$ is a regular, hence extremal, epimorphism, $\im(f) \hookrightarrow B$ is an isomorphism. Thus, $f$ is surjective.' From 7a711e4907a58b2e35322518d38b31a7b1741b1a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 3 Sep 2026 11:15:21 +0200 Subject: [PATCH 3/6] add the category of f.g. projective R[eps]-modules --- .cspell.json | 1 + content/free-cocompletion.md | 2 +- database/data/categories/FinVect_u.yaml | 1 + database/data/categories/FreeAb_fg.yaml | 3 +- database/data/categories/Proj_fg(R[e]).yaml | 97 +++++++++++++++++++++ database/data/categories/R-Mod.yaml | 1 + database/data/macros.yaml | 1 + 7 files changed, 104 insertions(+), 2 deletions(-) create mode 100644 database/data/categories/Proj_fg(R[e]).yaml diff --git a/.cspell.json b/.cspell.json index 01b039647..e81b4d931 100644 --- a/.cspell.json +++ b/.cspell.json @@ -39,6 +39,7 @@ "bijection", "bijections", "bijective", + "bimodule", "biproduct", "biproducts", "Birkhoff", diff --git a/content/free-cocompletion.md b/content/free-cocompletion.md index 66b9082fc..d13cc5c9c 100644 --- a/content/free-cocompletion.md +++ b/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)\}$$ diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index bd20868b1..5b3eda1d8 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -13,6 +13,7 @@ tags: related: - Vect - Ab_fg + - Proj_fg(R[e]) satisfied_properties: [] diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml index ff6c4fe57..4da2b3d20 100644 --- a/database/data/categories/FreeAb_fg.yaml +++ b/database/data/categories/FreeAb_fg.yaml @@ -3,7 +3,7 @@ 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 free abelian groups that are also finitely generated. Equivalently, it is the category of finitely generated projective $\IZ$-modules. Every object is isomorphic to $\IZ^n$ for a unique $n \in \IN$. +description: This is the full subcategory of $\Ab$ consisting of the free abelian groups that are also finitely generated. Equivalently, it is the category $\Proj_\fg(\IZ)$ of finitely generated projective $\IZ$-modules. Every object is isomorphic to $\IZ^n$ for a unique $n \in \IN$. nlab_link: null tags: @@ -15,6 +15,7 @@ related: - Ab_fg - FreeAb - FinVect_c + - Proj_fg(R[e]) satisfied_properties: - property: locally small diff --git a/database/data/categories/Proj_fg(R[e]).yaml b/database/data/categories/Proj_fg(R[e]).yaml new file mode 100644 index 000000000..ef9508ad5 --- /dev/null +++ b/database/data/categories/Proj_fg(R[e]).yaml @@ -0,0 +1,97 @@ +id: Proj_fg(R[e]) +name: category of finitely generated projective modules over the ring of dual numbers +notation: $\Proj_\fg(\IR[\varepsilon])$ +objects: finitely generated projective modules over $\IR[\varepsilon]$ +morphisms: $\IR[\varepsilon]$-linear maps +description: >- + In this entry, $R \coloneqq \IR[\varepsilon] \coloneqq \IR[X]/\langle X^2 \rangle$ is the ring of dual numbers over the real numbers, and we consider the full subcategory of $R{-}\Mod$ consisting of the modules that are finitely generated and projective. Thus, the objects are the direct summands of $R^n$ for some $n \in \IN$. But actually, since $R$ is local, every projective module is already free. + + Some of the properties proven here hold for every commutative ring $R$. But for the specific choice $R = \IR[\varepsilon]$, this category provides an example of an additive, normal, and conormal category which is not abelian. +nlab_link: null +tags: + - algebra + +related: + - R-Mod + - FreeAb_fg + - FinVect_u + +satisfied_properties: + - property: locally small + proof: The category is a full subcategory of $R{-}\Mod$, which is locally small. + + - property: essentially small + proof: 'This is because the category is locally small and every object is isomorphic to one in the set $\{R^n : n \in \IN\}$.' + + - property: additive + proof: The category is closed under finite direct sums in $R{-}\Mod$, which is additive. + + - property: extremal generator + proof: The module $R$ is an extremal generator, even in $R{-}\Mod$. + + - property: self-dual + proof: >- + More generally, if $R$ is any ring, the category $\Proj_\fg(R)$ of finitely generated projective left $R$-modules is dual to $\Proj_\fg(R^\op)$, which simplifies to $\Proj_\fg(R)$ if $R$ is commutative. In fact, since $R$ is an $R$-bimodule, the functor $\Hom(-,R) : R{-}\Mod^{\op} \to \Set$ lifts to an additive functor + $$\underline{\Hom}(-,R) : R{-}\Mod^{\op} \to R^{\op}{-}\Mod.$$ + It restricts to a functor + $$\underline{\Hom}(-,R) : \Proj_\fg(R)^{\op} \to \Proj_\fg(R^\op)$$ + because of $\underline{\Hom}(R^n,R) \cong R^n$ and since an additive functor preserves direct summands. This functor dualizes to a functor in the other direction, and we claim that these are inverse to each other. For this, it suffices to prove that the natural homomorphism + $$M \to \underline{\Hom}(\underline{\Hom}(M,R),R^{\op})$$ + defined by $m \mapsto (\varphi \mapsto \varphi(m))$ is an isomorphism. The collection of modules for which this is true is closed under finite direct sums and direct summands (since both sides are additive functors), and it contains $R$ by a direct calculation. Therefore, it contains every finitely generated projective left $R$-module. + + - property: quotients of congruences + proof: 'Let $p_1,p_2 : E \rightrightarrows M$ be a congruence in $\Proj_\fg(R)$. In particular, it is a reflexive relation on $M$ in $R{-}\Mod$. Thus, there is some submodule $U \subseteq M$ such that (up to isomorphism) $E = \{(x,y) \in M^2 : x-y \in U\}$ and $p_1,p_2$ are the two projections. Since $E \cong U \oplus M$ and $E$ is finitely generated and projective, it follows that $U$ is finitely generated and projective. Moreover, the coequalizer of $p_1,p_2$ in $R{-}\Mod$ is given by $M/U$, which is clearly finitely generated, and we claim that $M/U$ is also projective. For this, it suffices to prove that the monomorphism $U \hookrightarrow M$ splits, since then $M/U$ is a direct summand of $M$. But every monomorphism splits in this category since it is self-dual, and every epimorphism is surjective (see below) and therefore splits.' + label: proj_dual_numbers_quotients_congruences + + - property: effective congruences + proof: 'We saw before that every congruence $p_1,p_2 : E \rightrightarrows M$ in $\Proj_\fg(R)$ is isomorphic to $\{(x,y) \in M^2 : x-y \in U\}$ for some direct summand $U \subseteq M$, where $p_1,p_2$ are the two projections. Thus, it is the kernel pair of the projection $M \to M/U$, which indeed lies in $\Proj_\fg(R)$.' + references: + - proj_dual_numbers_quotients_congruences + + - property: ℵ₁-accessible + proof: >- + We will prove more generally that for left Noetherian rings $R$, $\Proj_\fg(R)$ is $\aleph_1$-accessible. The proof is similar to $\Ab_\fg$. + + First, we show that the inclusion $\Proj_\fg(R) \hookrightarrow R{-}\Mod$ is closed under $\aleph_1$-filtered colimits. Assume that $(M_i)$ is an $\aleph_1$-filtered diagram of $R$-modules with colimit $M$, where each $M_i$ is finitely generated and projective. Since $R$ is left Noetherian, finitely generated modules coincide with Noetherian modules. Therefore, MO/400763 implies that $M$ is finitely generated. + We conclude that $M$ is finitely presentable since $R$ is left Noetherian. Since $(M_i)$ is also an $\aleph_0$-filtered diagram, it follows that $\id_M : M \to M = \colim_i M_i$ factors through some $M_i \to M$. Therefore, $M$ is a direct summand of $M_i$. Since $M_i$ is projective, it follows that $M$ is projective as well. This proves the claim that $\aleph_1$-filtered colimits exist. + + To finish the proof that $\Proj_\fg(R)$ is $\aleph_1$-accessible, since it is essentially small, it suffices to prove that every object is $\aleph_1$-presentable. This follows since every finitely generated $R$-module is $\aleph_0$-presentable and therefore also $\aleph_1$-presentable in $R{-}\Mod$. + references: + - Ab_fg_aleph1-accessible + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: small + proof: Even the collection of trivial modules is not a set. + + - property: essentially countable + proof: The set $\Hom(R,R) \cong R = \IR[\varepsilon]$ is not countable. + + - property: locally finite + proof: The set $\Hom(R,R) \cong R = \IR[\varepsilon]$ is infinite. + + - property: kernels + proof: 'Assume that the linear map $\varepsilon : R \to R$ has a kernel $i : K \to R$, i.e. an equalizer with the zero map $0 : R \to R$. Since the forgetful functor to $\Set$ is representable, and therefore preserves equalizers, the underlying set of $K$ is $\{r \in R : r \varepsilon = 0\} = \IR \cdot \varepsilon$ and $i$ is the inclusion map. Thus, $K$ is isomorphic to the $R$-module $\IR$ on which $\varepsilon$ acts as zero. But this module is not projective. This is because it is not free, but a more elementary approach is to observe that the surjective $R$-linear map $R \to \IR$, $a + b \varepsilon \mapsto a$ does not split.' + +special_objects: + initial object: + description: zero module + terminal object: + description: zero module + coproducts: + description: '[finite case] direct sums' + products: + description: '[finite case] direct sums' + +special_morphisms: + isomorphisms: + description: bijective linear maps + proof: This follows from the corresponding fact for $R{-}\Mod$. + monomorphisms: + description: injective linear maps + proof: The non-trivial direction follows from the observation that the forgetful functor to $\Set$ is representable (by the free module of rank $1$) and therefore preserves monomorphisms. + epimorphisms: + description: surjective linear maps + proof: 'Surjective linear maps are clearly epimorphisms. Conversely, assume that $f : M \to N$ is an epimorphism in $\Proj_\fg(R)$. If $f$ is not surjective, $Q \coloneqq N/f(M)$ is a non-zero finitely generated $R$-module. Therefore, it has a simple quotient. Since $R$ is a local commutative ring with residue field $\IR$, the only simple $R$-module is $\IR$, on which $\varepsilon$ acts as zero. Thus, there is a surjective linear map $\varphi : Q \to \IR$. Composing this with the injective linear map $\IR \to R$, $r \mapsto r \varepsilon$, and the projection $N \twoheadrightarrow Q$, we get a non-zero linear map $\psi : N \to R$ with $\psi \circ f = 0$, which contradicts the assumption that $f$ is an epimorphism.' diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index a1aa527a3..4c24bddae 100644 --- a/database/data/categories/R-Mod.yaml +++ b/database/data/categories/R-Mod.yaml @@ -14,6 +14,7 @@ related: - Ab - Vect - grMod_G(R) + - Proj_fg(R[e]) satisfied_properties: - property: locally small diff --git a/database/data/macros.yaml b/database/data/macros.yaml index d464eb05e..89a01c15b 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -140,3 +140,4 @@ \Arr: \mathbf{Arr} \Mono: \mathbf{Mono} \Sh: \mathbf{Sh} +\Proj: \mathbf{Proj} From fc5ac5da38579baea5dbd0b7e876cfe11b6682ae Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 3 Sep 2026 13:02:14 +0200 Subject: [PATCH 4/6] rework the proofs that FreeAb and FreeAb_fg are regular --- database/data/categories/FreeAb.yaml | 15 ++++++++++----- database/data/categories/FreeAb_fg.yaml | 8 ++++---- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 66b1aac0e..0b3a23c0b 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -24,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 $\Grp$. Now apply Lemma 10 here. references: @@ -38,11 +42,12 @@ satisfied_properties: - property: well-copowered proof: See MSE/5025660. + - 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 $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the nLab 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 @@ -89,4 +94,4 @@ special_morphisms: 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.' 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.' diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml index 4da2b3d20..488fdb771 100644 --- a/database/data/categories/FreeAb_fg.yaml +++ b/database/data/categories/FreeAb_fg.yaml @@ -34,9 +34,6 @@ satisfied_properties: - property: extremal generator proof: The group $\IZ$ is an extremal generator, even in $\Ab$. - - property: regular - proof: It remains to prove that regular epimorphisms are stable under pullback. This is clear since they coincide with the surjective homomorphisms (see below). - - property: self-dual proof: >- The functor $\Hom(-,\IZ) : \FreeAb_\fg^{\op} \to \Set$ lifts to an additive functor $$\underline{\Hom}(-,\IZ) : \FreeAb_\fg^{\op} \to \Ab.$$ @@ -46,6 +43,9 @@ satisfied_properties: $$A \to \underline{\Hom}(\underline{\Hom}(A,\IZ),\IZ)$$ defined by $a \mapsto (\varphi \mapsto \varphi(a))$ is an isomorphism. The collection of abelian groups for which this is true is closed under finite direct sums (since both sides are additive functors), and it contains $\IZ$ by a direct calculation. Therefore, it contains every $\IZ^n$. + - 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 $\Ab_\fg$. The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. 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$.' references: @@ -92,4 +92,4 @@ special_morphisms: proof: We can copy the proof from $\FreeAb$. regular epimorphisms: description: surjective homomorphisms (which are automatically split epimorphisms) - proof: 'If $f : A \to B$ is a surjective homomorphism in $\FreeAb_\fg$ with kernel $K$, then $f$ is the cokernel of $K \hookrightarrow A$ in $\Ab$. Since $K$ is finitely generated and free abelian, this remains true in $\FreeAb_\fg$. Moreover, $f$ splits since $B$ is projective. Conversely, assume that $f : A \to B$ is a regular epimorphism in $\FreeAb_\fg$ and hence the cokernel of some homomorphism $g : C \to A$ in $\FreeAb_\fg$. Consider the image factorization $A \to \im(f) \hookrightarrow B$ in $\Ab$. Here, $\im(f)$ is also finitely generated and free abelian. Since $\im(f) \hookrightarrow B$ is a monomorphism in $\FreeAb_\fg$ and $f$ is a regular, hence extremal, epimorphism, $\im(f) \hookrightarrow B$ is an isomorphism. Thus, $f$ is surjective.' + proof: We can copy the proof from $\FreeAb$. From 6eaa16bd4a1c136df04eff41f3f67914747039de Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 3 Sep 2026 17:19:04 +0200 Subject: [PATCH 5/6] various improvements to categories of f.g. projective modules --- database/data/categories/FreeAb.yaml | 8 ++++---- database/data/categories/FreeAb_fg.yaml | 20 ++++++++++---------- database/data/categories/Proj_fg(R[e]).yaml | 16 ++++++++++------ 3 files changed, 24 insertions(+), 20 deletions(-) diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 0b3a23c0b..9899d7de2 100644 --- a/database/data/categories/FreeAb.yaml +++ b/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 free abelian groups. +description: This is the full subcategory of $\Ab$ consisting of the free abelian groups. Since $\IZ$ is a principal ideal domain, these coincide with the projective $\IZ$-modules, so that $\FreeAb \cong \Proj(\IZ)$. nlab_link: null tags: @@ -85,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: '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.' diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml index 488fdb771..0dc0a4d8d 100644 --- a/database/data/categories/FreeAb_fg.yaml +++ b/database/data/categories/FreeAb_fg.yaml @@ -35,21 +35,21 @@ satisfied_properties: proof: The group $\IZ$ is an extremal generator, even in $\Ab$. - property: self-dual - proof: >- - The functor $\Hom(-,\IZ) : \FreeAb_\fg^{\op} \to \Set$ lifts to an additive functor $$\underline{\Hom}(-,\IZ) : \FreeAb_\fg^{\op} \to \Ab.$$ - It corestricts to $\FreeAb_\fg$ because of $\underline{\Hom}(\IZ^n,\IZ) \cong \IZ^n$. The functor - $$\underline{\Hom}(-,\IZ) : \FreeAb_\fg^{\op} \to \FreeAb_\fg$$ - dualizes to a functor in the other direction, and we claim that these are inverse to each other. For this, it suffices to prove that the natural homomorphism - $$A \to \underline{\Hom}(\underline{\Hom}(A,\IZ),\IZ)$$ - defined by $a \mapsto (\varphi \mapsto \varphi(a))$ is an isomorphism. The collection of abelian groups for which this is true is closed under finite direct sums (since both sides are additive functors), and it contains $\IZ$ by a direct calculation. Therefore, it contains every $\IZ^n$. + proof: More generally, if $R$ is a commutative ring, $\Proj_\fg(R)$ is self-dual, as proven here. + 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 $\Ab_\fg$. The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. 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$.' + proof: >- + The proof is very similar to the proof for $\Ab_\fg$. The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. 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 here. references: - Ab_fg_aleph1-accessible + - Proj_fg_aleph1-accessible unsatisfied_properties: - property: skeletal @@ -88,8 +88,8 @@ special_morphisms: 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 $\FreeAb$. regular monomorphisms: - description: 'injective homomorphisms $f : A \to B$ such that $B/f(A)$ is free abelian (and hence which are automatically split monomorphisms)' - proof: We can copy the proof from $\FreeAb$. + 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 $\FreeAb$, 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 $\FreeAb$. diff --git a/database/data/categories/Proj_fg(R[e]).yaml b/database/data/categories/Proj_fg(R[e]).yaml index ef9508ad5..c7abc6405 100644 --- a/database/data/categories/Proj_fg(R[e]).yaml +++ b/database/data/categories/Proj_fg(R[e]).yaml @@ -31,16 +31,19 @@ satisfied_properties: - property: self-dual proof: >- - More generally, if $R$ is any ring, the category $\Proj_\fg(R)$ of finitely generated projective left $R$-modules is dual to $\Proj_\fg(R^\op)$, which simplifies to $\Proj_\fg(R)$ if $R$ is commutative. In fact, since $R$ is an $R$-bimodule, the functor $\Hom(-,R) : R{-}\Mod^{\op} \to \Set$ lifts to an additive functor + More generally, if $R$ is any ring, the category $\Proj_\fg(R)$ of finitely generated projective left $R$-modules is dual to $\Proj_\fg(R^{\op})$, which simplifies to $\Proj_\fg(R)$ if $R$ is commutative. In fact, since $R$ is an $R$-bimodule, the functor $\Hom(-,R) : R{-}\Mod^{\op} \to \Set$ lifts to an additive functor $$\underline{\Hom}(-,R) : R{-}\Mod^{\op} \to R^{\op}{-}\Mod.$$ It restricts to a functor - $$\underline{\Hom}(-,R) : \Proj_\fg(R)^{\op} \to \Proj_\fg(R^\op)$$ - because of $\underline{\Hom}(R^n,R) \cong R^n$ and since an additive functor preserves direct summands. This functor dualizes to a functor in the other direction, and we claim that these are inverse to each other. For this, it suffices to prove that the natural homomorphism + $$\underline{\Hom}(-,R) : \Proj_\fg(R)^{\op} \to \Proj_\fg(R^{\op})$$ + because of $\underline{\Hom}(R^n,R) \cong (R^{\op})^n$ and since an additive functor preserves direct summands. By replacing $R$ with $R^{\op}$ and considering the dual functor, we get a functor + $$\underline{\Hom}(-,R^{\op}) : \Proj_\fg(R^{\op}) \to \Proj_\fg(R)^{\op}$$ + in the other direction, and we claim that these are inverse to each other. For this, it suffices to prove that, for every $M \in \Proj_\fg(R)$, the natural homomorphism $$M \to \underline{\Hom}(\underline{\Hom}(M,R),R^{\op})$$ defined by $m \mapsto (\varphi \mapsto \varphi(m))$ is an isomorphism. The collection of modules for which this is true is closed under finite direct sums and direct summands (since both sides are additive functors), and it contains $R$ by a direct calculation. Therefore, it contains every finitely generated projective left $R$-module. + label: proj_fg_self-dual - property: quotients of congruences - proof: 'Let $p_1,p_2 : E \rightrightarrows M$ be a congruence in $\Proj_\fg(R)$. In particular, it is a reflexive relation on $M$ in $R{-}\Mod$. Thus, there is some submodule $U \subseteq M$ such that (up to isomorphism) $E = \{(x,y) \in M^2 : x-y \in U\}$ and $p_1,p_2$ are the two projections. Since $E \cong U \oplus M$ and $E$ is finitely generated and projective, it follows that $U$ is finitely generated and projective. Moreover, the coequalizer of $p_1,p_2$ in $R{-}\Mod$ is given by $M/U$, which is clearly finitely generated, and we claim that $M/U$ is also projective. For this, it suffices to prove that the monomorphism $U \hookrightarrow M$ splits, since then $M/U$ is a direct summand of $M$. But every monomorphism splits in this category since it is self-dual, and every epimorphism is surjective (see below) and therefore splits.' + proof: 'Let $p_1,p_2 : E \rightrightarrows M$ be a congruence in $\Proj_\fg(R)$. In particular, it is a reflexive relation in $R{-}\Mod$. Thus, there is some submodule $U \subseteq M$ such that $E$ is isomorphic to the module $\{(x,y) \in M^2 : x-y \in U\}$, where $p_1,p_2$ are the two evident projections. Since $E \cong U \oplus M$ and $E$ is finitely generated and projective, it follows that $U$ is finitely generated and projective. Moreover, the coequalizer of $p_1,p_2$ in $R{-}\Mod$ is given by $M/U$, which is clearly finitely generated, and we claim that $M/U$ is also projective. For this, it suffices to prove that the monomorphism $U \hookrightarrow M$ splits, since then $M/U$ is a direct summand of $M$. But every monomorphism splits in this category since it is self-dual and every epimorphism splits by their classification below.' label: proj_dual_numbers_quotients_congruences - property: effective congruences @@ -56,6 +59,7 @@ satisfied_properties: We conclude that $M$ is finitely presentable since $R$ is left Noetherian. Since $(M_i)$ is also an $\aleph_0$-filtered diagram, it follows that $\id_M : M \to M = \colim_i M_i$ factors through some $M_i \to M$. Therefore, $M$ is a direct summand of $M_i$. Since $M_i$ is projective, it follows that $M$ is projective as well. This proves the claim that $\aleph_1$-filtered colimits exist. To finish the proof that $\Proj_\fg(R)$ is $\aleph_1$-accessible, since it is essentially small, it suffices to prove that every object is $\aleph_1$-presentable. This follows since every finitely generated $R$-module is $\aleph_0$-presentable and therefore also $\aleph_1$-presentable in $R{-}\Mod$. + label: Proj_fg_aleph1-accessible references: - Ab_fg_aleph1-accessible @@ -93,5 +97,5 @@ special_morphisms: description: injective linear maps proof: The non-trivial direction follows from the observation that the forgetful functor to $\Set$ is representable (by the free module of rank $1$) and therefore preserves monomorphisms. epimorphisms: - description: surjective linear maps - proof: 'Surjective linear maps are clearly epimorphisms. Conversely, assume that $f : M \to N$ is an epimorphism in $\Proj_\fg(R)$. If $f$ is not surjective, $Q \coloneqq N/f(M)$ is a non-zero finitely generated $R$-module. Therefore, it has a simple quotient. Since $R$ is a local commutative ring with residue field $\IR$, the only simple $R$-module is $\IR$, on which $\varepsilon$ acts as zero. Thus, there is a surjective linear map $\varphi : Q \to \IR$. Composing this with the injective linear map $\IR \to R$, $r \mapsto r \varepsilon$, and the projection $N \twoheadrightarrow Q$, we get a non-zero linear map $\psi : N \to R$ with $\psi \circ f = 0$, which contradicts the assumption that $f$ is an epimorphism.' + description: surjective linear maps (which are automatically split epimorphisms) + proof: 'Surjective linear maps are clearly epimorphisms, and they split because their codomain is projective. Conversely, assume that $f : M \to N$ is an epimorphism in $\Proj_\fg(R)$. If $f$ is not surjective, $Q \coloneqq N/f(M)$ is a non-zero finitely generated $R$-module. Therefore, it has a simple quotient. Since $R$ is a local commutative ring with residue field $\IR$, the only simple $R$-module is $\IR$, on which $\varepsilon$ acts as zero. Thus, there is a surjective linear map $\varphi : Q \to \IR$. Composing this with the injective linear map $\IR \to R$, $r \mapsto r \varepsilon$, and the projection $N \twoheadrightarrow Q$, we get a non-zero linear map $\psi : N \to R$ with $\psi \circ f = 0$, which contradicts the assumption that $f$ is an epimorphism.' From b8f6e38028e67abb89aae9f2f55a8bf8d8407060 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 3 Sep 2026 17:20:34 +0200 Subject: [PATCH 6/6] remove brackets from category ID --- database/data/categories/FinVect_u.yaml | 2 +- database/data/categories/FreeAb_fg.yaml | 6 +++--- .../categories/{Proj_fg(R[e]).yaml => Proj_fg(Re).yaml} | 2 +- database/data/categories/R-Mod.yaml | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) rename database/data/categories/{Proj_fg(R[e]).yaml => Proj_fg(Re).yaml} (99%) diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index 5b3eda1d8..b5f85fd18 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -13,7 +13,7 @@ tags: related: - Vect - Ab_fg - - Proj_fg(R[e]) + - Proj_fg(Re) satisfied_properties: [] diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml index 0dc0a4d8d..49295bbef 100644 --- a/database/data/categories/FreeAb_fg.yaml +++ b/database/data/categories/FreeAb_fg.yaml @@ -15,7 +15,7 @@ related: - Ab_fg - FreeAb - FinVect_c - - Proj_fg(R[e]) + - Proj_fg(Re) satisfied_properties: - property: locally small @@ -35,7 +35,7 @@ satisfied_properties: 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 here. + proof: More generally, if $R$ is a commutative ring, $\Proj_\fg(R)$ is self-dual, as proven here. references: - proj_fg_self-dual @@ -46,7 +46,7 @@ satisfied_properties: proof: >- The proof is very similar to the proof for $\Ab_\fg$. The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. 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 here. + More generally, if $R$ is a left Noetherian ring, then $\Proj_\fg(R)$ is $\aleph_1$-accessible, as proven here. references: - Ab_fg_aleph1-accessible - Proj_fg_aleph1-accessible diff --git a/database/data/categories/Proj_fg(R[e]).yaml b/database/data/categories/Proj_fg(Re).yaml similarity index 99% rename from database/data/categories/Proj_fg(R[e]).yaml rename to database/data/categories/Proj_fg(Re).yaml index c7abc6405..8abfbe526 100644 --- a/database/data/categories/Proj_fg(R[e]).yaml +++ b/database/data/categories/Proj_fg(Re).yaml @@ -1,4 +1,4 @@ -id: Proj_fg(R[e]) +id: Proj_fg(Re) name: category of finitely generated projective modules over the ring of dual numbers notation: $\Proj_\fg(\IR[\varepsilon])$ objects: finitely generated projective modules over $\IR[\varepsilon]$ diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index 4c24bddae..219cd737f 100644 --- a/database/data/categories/R-Mod.yaml +++ b/database/data/categories/R-Mod.yaml @@ -14,7 +14,7 @@ related: - Ab - Vect - grMod_G(R) - - Proj_fg(R[e]) + - Proj_fg(Re) satisfied_properties: - property: locally small