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/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/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index bd20868b1..b5f85fd18 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(Re) satisfied_properties: [] diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 1fbd065ca..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: @@ -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 $\Grp$. Now apply Lemma 10 here. references: @@ -37,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 @@ -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.' diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml new file mode 100644 index 000000000..49295bbef --- /dev/null +++ b/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 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: + - 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 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$. + + 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 + 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 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(Re).yaml b/database/data/categories/Proj_fg(Re).yaml new file mode 100644 index 000000000..8abfbe526 --- /dev/null +++ b/database/data/categories/Proj_fg(Re).yaml @@ -0,0 +1,101 @@ +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]$ +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^{\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 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 + 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$. + label: Proj_fg_aleph1-accessible + 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 (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.' diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index a1aa527a3..219cd737f 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(Re) 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} 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)