diff --git a/.cspell.json b/.cspell.json index f0a1a808..ea713a95 100644 --- a/.cspell.json +++ b/.cspell.json @@ -21,7 +21,8 @@ "devlog", "cech", "Unif", - "noiso" + "noiso", + "coprod" ], "words": [ "abelian", @@ -38,10 +39,12 @@ "Axiomatising", "axiomatization", "Baer", + "Baire", "bijection", "bijections", "bijective", "bimodule", + "Binet", "biproduct", "biproducts", "Birkhoff", @@ -150,6 +153,7 @@ "cotransitivity", "counit", "counital", + "Cramer", "delooping", "deloopings", "Demazure", diff --git a/database/data/categories/Euclid_coprod.yaml b/database/data/categories/Euclid_coprod.yaml new file mode 100644 index 00000000..681c5b5c --- /dev/null +++ b/database/data/categories/Euclid_coprod.yaml @@ -0,0 +1,155 @@ +id: Euclid_coprod +name: category of coproducts of Euclidean spaces +notation: $\Euclid_{\sqcup}$ +objects: coproducts of Euclidean spaces +morphisms: continuous functions +description: >- + By definition, this is the full subcategory of $\Top$ (or $\Haus$) where every space is isomorphic to $\coprod_{i \in I} \IR^{n_i}$ for a family of natural numbers $(n_i)_{i \in I}$. These are locally Euclidean spaces in the strongest possible sense. This category provides an example of an infinitary distributive category that is not Cauchy complete. Using the fact that Euclidean spaces are connected, it is easy to see that this category is the free coproduct cocompletion of the category of Euclidean spaces. +nlab_link: null +tags: + - topology + +related: + - Top + - Haus + - Man + - Met_c + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\Top$, which is locally small. + + - property: finite products + proof: This follows since $\Top$ is infinitary distributive and Euclidean spaces are closed under finite products. Namely, $\IR^0=1$ and $\IR^n \times \IR^m \cong \IR^{n+m}$. + + - property: infinitary extensive + proof: The free coproduct cocompletion of any category is infinitary extensive; for the finite case see Proposition 2.4 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. + + - property: well-powered + proof: This is clear from the classification of monomorphisms as injective continuous maps. + + - property: well-copowered + proof: The classification of epimorphisms below shows that every epimorphism is also an epimorphism in $\Haus$, so that the claim follows from the fact that $\Haus$ is well-copowered. + + - property: semi-strongly connected + proof: This property is inherited from $\Top$. + + - property: extremal generator + proof: >- + We will prove that $\IR$ is an extremal generator. It is clearly a generator; in fact, every non-empty space is a generator in $\Top$ by using constant maps. + Now assume that $f : X \to Y$ is a map in $\Euclid_{\sqcup}$ such that + $$f_* : \Hom(\IR,X) \to \Hom(\IR,Y)$$ + is bijective. Using constant maps, it is easy to see that $f$ is bijective. It remains to show that the inverse map $f^{-1} : Y \to X$ is continuous. It suffices to check this on every Euclidean component $\IR^n \subseteq Y$. To this end, assume that $(y_k)_{k \geq 1} \to y$ is a convergent sequence in $\IR^n$. It corresponds to a continuous map + $$\{0\} \cup \{1/k : k \geq 1\} \to \IR^n$$ + mapping $0 \mapsto y$ and $1/k \mapsto y_k$. Using linear interpolation, it extends to a continuous map $[0,1] \to \IR^n$. We further extend this to a continuous map $\IR \to \IR^n$ by mapping every number $<0$ to $0$ and every number $>1$ to $y_1$. Thus, we obtain a continuous map $h : \IR \to Y$ with $h(0)=y$ and $h(1/k) = y_k$. By assumption, the map $f^{-1} \circ h : \IR \to X$ is also continuous. In particular, its restriction to $\{0\} \cup \{1/k : k \geq 1\}$ is continuous. This means that $(f^{-1}(y_k))_{k \geq 1} \to f^{-1}(y)$. + + - property: extremal cogenerator + proof: The category $\Euclid_{\sqcup}$ is a full subcategory of $\Met_c$, in which $\IR$ is an extremal cogenerator. Now apply Lemma 10 here. + references: + - Met_c_cogenerator + + - property: effective cocongruences + proof: >- + Let $i_1,i_2 : X \rightrightarrows E$ be a coreflexive corelation in $\Euclid_{\sqcup}$. (We will not need to assume cosymmetry or cosymmetry, as both properties will follow.) This means that the induced map $(i_1;i_2) : X \sqcup X \to E$ is an epimorphism, i.e. has dense image, and that there is a continuous map $r : E \to X$ satisfying + $$r \circ i_1 = r \circ i_2 = \id_X.$$ + It follows that, in $\Top$, $i_1$ is the equalizer of $\id_E$ and $i_1 \circ r : E \rightrightarrows E$. Since $E$ is Hausdorff, this implies that $i_1$ is an embedding with closed image $i_1(X)$. Likewise, $i_2$ is an embedding with closed image $i_2(X)$. Their union $i_1(X) \cup i_2(X)$ is also closed. On the other hand, since $(i_1;i_2)$ has dense image, $i_1(X) \cup i_2(X)$ is dense. Thus, + $$E = i_1(X) \cup i_2(X),$$ + i.e. $i_1,i_2$ are jointly surjective. It follows that the underlying maps of $i_1,i_2$ form a coreflexive corelation in $\Set$. Therefore, by this result, if we define the equalizer + $$U \coloneqq \{x \in X : i_1(x) = i_2(x)\},$$ + then the induced continuous map + $$X \sqcup_U X \to E$$ + is a bijection. Since the maps $i_1,i_2$ are closed embeddings, $(i_1;i_2) : X + X \to E$ is closed, and therefore a quotient map. It follows that $X \sqcup_U X \cong E$ is an isomorphism of topological spaces. In other words, $i_1,i_2$ is the cokernel pair of $U \hookrightarrow X$ in $\Top$. + + It remains to prove that $U$ belongs to $\Euclid_{\sqcup}$, since then $i_1,i_2$ is also a cokernel pair in $\Euclid_{\sqcup}$. In fact, we will prove that $U$ is a union of connected components of $X$. + + Suppose that $U$ intersects a connected component $X' \subseteq X$. Choose a point $x \in U \cap X'$ and let $e \coloneqq i_1(x) = i_2(x)$. Let $E' \subseteq E$ be the connected component containing $e$. Then $i_1(X') \subseteq E'$ and $i_2(X') \subseteq E'$. Since $r(e)=x$, we also have $r(E') \subseteq X'$. We claim that + $$E' = i_1(X') \cup i_2(X').$$ + The inclusion $\supseteq$ is clear. To show the inclusion $\subseteq$, pick any point $p \in E'$. We have either $p \in i_1(X)$ or $p \in i_2(X)$. Assume without loss of generality that $p \in i_1(X)$, say $p = i_1(y)$ for some $y \in X$. Then $y = r(p) \in r(E') \subseteq X'$, and hence $p \in i_1(X')$. + + The space $E'$ is Euclidean and therefore a Baire space. Thus, it cannot be the union of two closed sets with empty interior. Assume without loss of generality that $i_1(X')$ has non-empty interior in $E'$. Since $i_1(X') \cong X'$ is also Euclidean, the Invariance of Domain theorem implies that $X'$ and $E'$ have the same dimension and that $i_1(X')$ is open in $E'$. Since $i_1$ is a closed embedding, $i_1(X')$ is also closed in $E'$, and it is non-empty. Since $E'$ is connected, this implies + $$i_1(X') = E'.$$ + Hence, for every $y \in X'$, we have $i_2(y) = i_1(z)$ for some $z \in X'$. Applying $r$, we obtain $y=z$, and hence $y \in U$. This proves that $U$ contains the entire component $X'$ and finishes the proof. + label: Euclid_coprod_cocongruence_classification + + - property: coquotients of cocongruences + proof: >- + We have proved above that every cocongruence in $\Euclid_{\sqcup}$ is isomorphic to + $$X \rightrightarrows X \sqcup_U X$$ + for some subset $U \subseteq X$ which is a union of connected components of $X$. Since $U \hookrightarrow X$ is the equalizer of $X \rightrightarrows X \sqcup_U X$ in $\Top$, this remains true in $\Euclid_{\sqcup}$. + references: + - Euclid_coprod_cocongruence_classification + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: balanced + proof: 'The space $\IR \setminus \{0\}$ belongs to $\Euclid_{\coprod}$ because it is the coproduct of $\IR^+$ and $\IR^-$, both of which are isomorphic to $\IR$; for example, $\exp : \IR \to \IR^+$ is an isomorphism in $\Top$. Now consider the inclusion map $\IR \setminus \{0\} \hookrightarrow \IR$. It has dense image, hence is an epimorphism in $\Haus$, a fortiori in $\Euclid_{\coprod}$. It is also injective and therefore a monomorphism. But it is not an isomorphism since it is not bijective.' + + - property: Cauchy complete + proof: >- + Consider the continuous map $f : \IR \to \IR$ defined by + $$f(x) = \begin{cases} + 0 & x \leq 0 \\ + x & 0 \leq x \leq 1 \\ + 1 & x \geq 1. + \end{cases}$$ + The map is clearly idempotent. A splitting in $\Euclid_{\coprod}$ would also be a splitting in $\Top$, and therefore be necessarily isomorphic (cf. MSE/652185) to the splitting $\IR \twoheadrightarrow [0,1] \hookrightarrow \IR$ in $\Top$. But $[0,1]$ is not a coproduct of Euclidean spaces. Otherwise, being a connected space, it would be an Euclidean space, but also a compact space, which only leaves $\IR^0$, which is absurd. + + - property: countable powers + proof: >- + Assume that the power $P \coloneqq \IR^{\IN^+}$ exists in $\Euclid_{\sqcup}$ with projection map $p_n : P \to \IR$ for $n \in \IN^+$. Notice that we cannot assume that its underlying space identifies with the power in $\Top$. By applying the universal property to $1 \in \Euclid_{\sqcup}$, we merely see that the underlying set of $P$ is the cartesian product $\IR^{\IN^+}$ and $p_n(x)=x_n$. But knowing the underlying set is not sufficient. + + We first prove that $P$ is path-connected, and thus connected. The space $P$ is clearly non-empty, for example by our description of the underlying set. Take two points $x,y \in P$. For every $n \in \IN^+$, there is a continuous map $f_n : \IR \to \IR$ with $f_n(0) = p_n(x)$ and $f_n(1) = p_n(y)$; for example, we may take the affine-linear function through the points $(0,p_n(x))$ and $(1,p_n(y))$. By the universal property of $P$, there is a continuous map $f : \IR \to P$ with $p_n \circ f = f_n$ for every $n \in \IN^+$. Since the maps $p_n$ are jointly injective, it follows that $f(0)=x$ and $f(1)=y$. Thus, $f|_{[0,1]}$ is a continuous path from $x$ to $y$. + + Since $P$ is connected and belongs to $\Euclid_{\sqcup}$, it is isomorphic to $\IR^k$ for some $k \in \IN$. + + For every $n \in \IN$, we consider the continuous map $f : \IR^n \to P$, where $p_k \circ f : \IR^n \to \IR$ is the $k$th coordinate projection when $1 \leq k \leq n$, and otherwise, say, the zero map. Conversely, there is a continuous map $(p_1,\dotsc,p_n) : P \to \IR^n$. By construction, the composition $\IR^n \to P \to \IR^n$ is the identity. Therefore, for every $n \in \IN$, the Euclidean space $\IR^n$ embeds into $P$. But $P \cong \IR^k$, so if we apply this to $n = k+1$, we see that $\IR^{k+1}$ has an injective continuous map into $\IR^k$. This contradicts the theorem on the invariance of domain. + + - property: kernel pairs + proof: >- + First, we remark that the inclusion functor $\Euclid_{\sqcup} \hookrightarrow \Met_c$ preserves finite limits by Lemma 1 here, since $\Euclid_{\sqcup}$ contains the extremal cogenerator $\IR$ of $\Met_c$. The inclusion functor $\Met_c \hookrightarrow \Top$ clearly preserves finite limits. Hence, the inclusion functor $\Euclid_{\sqcup} \hookrightarrow \Top$ preserves finite limits. Therefore, $\Euclid_{\sqcup}$ has kernel pairs if and only if it is closed under kernel pairs taken in $\Top$. + + Now consider the continuous map $f : \IR \to \IR$, $x \mapsto x^2$. Its kernel pair in $\Top$ is + $$\{(x,y) \in \IR^2 : x^2=y^2\} = \{(x,x) : x \in \IR\} \cup \{(x,-x) : x \in \IR\}.$$ + But this space does not belong to $\Euclid_{\sqcup}$. In fact, since it is connected, it would have to be isomorphic to $\IR^n$. Removing $(0,0)$ from this space yields a space with four connected components. However, $\IR^n$ minus a point is connected for $n > 1$, while $\IR$ minus a point has two connected components. + references: + - Met_c_cogenerator + + - property: cokernel pairs + proof: >- + Consider the inclusion map $\{0\} \hookrightarrow \IR$. We claim that the pushout $P = \IR \sqcup_{0} \IR$ does not exist in $\Euclid_{\sqcup}$. To prove this, let $W = \IR \sqcup_{0} \IR$ be the pushout in $\Top$. Then there is a continuous map + $$p : W \to P,$$ + which is in fact the universal continuous map from $W$ to a space in $\Euclid_{\sqcup}$. Since the map $\IR \sqcup \IR \to P$ is an epimorphism in $\Euclid_{\sqcup}$, it has dense image (by the classification below). Therefore, $p : W \to P$ also has dense image. Since $W$ is connected, it follows that $P$ is connected as well. Thus, $P \cong \IR^n$ for some $n \in \IN$. + + We claim that $p$ is an embedding of topological spaces. To this end, consider the standard embedding $i : W \to \IR^2$ that maps $x \in \IR$ in the first copy to $(x,0)$ and $y \in \IR$ in the second copy to $(0,y)$. Since $\IR^2$ is Euclidean, there is a continuous map $j : W \to \IR^2$ with $j \circ p = i$. Since $i$ is an embedding, we conclude that $p$ is an embedding. + + We have shown that $W$ is isomorphic to a subspace of $\IR^n$ with dense image. Since $W$ is locally compact and $\IR^n$ is Hausdorff, this subspace is locally closed. Since it is locally closed and dense, it is open. But it is well known that $W$ is not a topological manifold, since $W \setminus \{(0,0)\}$ has too many connected components. + label: Euclid_coprod_no_cokernel_pairs + check_redundancy: false + + - property: quotients of congruences + proof: Since the category is extensive, if it had quotients of congruences, by this lemma it would have pushouts of monomorphisms. But we have seen before that $\IR \sqcup_{0} \IR$ does not exist. + references: + - Euclid_coprod_no_cokernel_pairs + +special_objects: + initial object: + description: empty space + terminal object: + description: singleton space + coproducts: + description: disjoint union + products: + description: '[finite case] direct product' + +special_morphisms: + isomorphisms: + description: homeomorphisms + proof: This is easy. + monomorphisms: + description: injective continuous maps + proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. + epimorphisms: + description: continuous maps with dense image + proof: 'A continuous map with dense image is an epimorphism in $\Haus$ and therefore also in $\Euclid_{\sqcup}$. Conversely, assume that $f : X \to Y$ is an epimorphism in $\Euclid_{\sqcup}$. Assume that there is a point $y \in Y \setminus \overline{f(X)}$. Consider the Euclidean component $\IR^n \subseteq Y$ containing $y$. Then $y \in \IR^n$ is not contained in the closed subset $\overline{f(X)} \cap \IR^n$. Since $\IR^n$ is a metric space and hence completely regular, there is a continuous map $\varphi : \IR^n \to \IR$ with $\varphi(y)=1$ and $\varphi \equiv 0$ on $\overline{f(X)} \cap \IR^n$. We may extend $\varphi$ to a continuous function $\psi : Y \to \IR$ by mapping every other component to $0$. Since $\psi$ is not the zero map and $f$ is an epimorphism, also $\psi \circ f$ is not the zero map. Choose $x \in X$ such that $\psi(f(x)) \neq 0$. Since $\psi$ maps every component to $0$ except for the mentioned $\IR^n$, we must have $f(x) \in \IR^n$. But then $\psi(f(x)) = \varphi(f(x))=0$ by construction of $\varphi$. This is a contradiction.' diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml index 49295bbe..db95dc08 100644 --- a/database/data/categories/FreeAb_fg.yaml +++ b/database/data/categories/FreeAb_fg.yaml @@ -16,6 +16,7 @@ related: - FreeAb - FinVect_c - Proj_fg(Re) + - Free_fg(ZxZ) satisfied_properties: - property: locally small diff --git a/database/data/categories/Free_fg(ZxZ).yaml b/database/data/categories/Free_fg(ZxZ).yaml new file mode 100644 index 00000000..bd0d3995 --- /dev/null +++ b/database/data/categories/Free_fg(ZxZ).yaml @@ -0,0 +1,118 @@ +id: Free_fg(ZxZ) +name: category of finitely generated free modules over Z x Z +notation: $\Free_{\fg}(\IZ \times \IZ)$ +objects: $\IZ \times \IZ$-modules that are finitely generated and free, i.e. $\cong (\IZ \times \IZ)^n$ for some $n$ +morphisms: $\IZ \times \IZ$-linear maps +description: This is a typical example of an additive category that is not Cauchy complete. It can also be seen as the free additive category on the walking idempotent. +nlab_link: null + +tags: + - algebra + +related: + - R-Mod + - FreeAb_fg + - Proj_fg(Re) + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $(\IZ \times \IZ){-}\Mod$, which is locally small. + + - property: essentially countable + proof: Every object is isomorphic to one of the countably many modules $(\IZ \times \IZ)^n$, and the set $\Hom((\IZ \times \IZ)^n,(\IZ \times \IZ)^m) \cong M_{m \times n}(\IZ \times \IZ)$ is countable. + + - property: additive + proof: The category is closed under finite direct sums in $(\IZ \times \IZ){-}\Mod$, which is additive. + + - property: extremal generator + proof: For every ring $R$, we know that $R$ is an extremal generator of $R{-}\Mod$, and hence also an extremal generator of the category of finitely generated free $R$-modules. + + - property: self-dual + proof: More generally, if $R$ is a ring, the functor $\underline{\Hom}(-,R)$ implements an equivalence of categories between the dual of the category of finitely generated free $R$-modules and the category of finitely generated free $R^{\op}$-modules. See also the proof of self-duality here. + references: + - proj_fg_self-dual + + - property: quotients of congruences + proof: >- + Since $(\IZ \times \IZ){-}\Mod$ is equivalent to $\Ab \times \Ab$ via $M \mapsto ((1,0) M, (0,1) M)$, and the equivalence maps $(\IZ \times \IZ)^n$ to $(\IZ^n,\IZ^n)$, the category $\Free_{\fg}(\IZ \times \IZ)$ is equivalent to the full subcategory of $\FreeAb_{\fg} \times \FreeAb_{\fg}$ consisting of those pairs of finitely generated free abelian groups $(A,B)$ such that $\rank(A)=\rank(B)$, i.e. $A \cong B$. We denote these equivalences by $M \mapsto (M_1,M_2)$. + + Let $E \rightrightarrows M$ be a congruence in $\Free_{\fg}(\IZ \times \IZ)$. By applying the definition to the test object $\IZ \times \IZ$, we see that it is a congruence in $(\IZ \times \IZ){-}\Mod$. Thus, we have + $$E = \{(x,y) \in M \times M : x - y \in U\}$$ + for some $\IZ \times \IZ$-submodule $U \subseteq M$ (up to isomorphism), namely + $$U = \{x \in M : (x,0) \in E\}.$$ + This implies + $$E \cong M \oplus U.$$ + The pair $(U_1,U_2)$ of $\IZ$-modules corresponding to $U$ therefore satisfies $E_i \cong M_i \oplus U_i$ for $i=1,2$. Since $E_i$ is finitely generated and free, we see that $U_i$ is a finitely generated projective $\IZ$-module, which is therefore free. Moreover, the rank of $U_i$ is + $$\rank(U_i) = \rank(E_i) - \rank(M_i).$$ + Since $\rank(E_1) = \rank(E_2)$ and $\rank(M_1) = \rank(M_2)$, we conclude that $\rank(U_1) = \rank(U_2)$. We have shown that $U$ belongs to $\Free_{\fg}(\IZ \times \IZ)$. + + The quotient of the congruence $E \rightrightarrows M$ in $(\IZ \times \IZ){-}\Mod$ is $M/U$, but this will not be the quotient in the subcategory of free modules. Instead, consider the congruences $E_i \rightrightarrows M_i$ for $i=1,2$ in $\Ab$, whose quotients in $\TorsFreeAb$ and hence also in $\FreeAb_{\fg}$ are the torsion-free reflections $(M_i / U_i) / T(M_i / U_i)$. The rank of this abelian group is $\rank(M_i) - \rank(U_i)$, which therefore does not depend on $i$. Thus, the pair of these quotients belongs to $\Free_{\fg}(\IZ \times \IZ)$. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: small + proof: Even the collection of trivial modules is not a set. + + - property: countable + proof: Even the collection of trivial modules is not countable. + + - property: locally finite + proof: The set $\Hom(\IZ \times \IZ,\IZ \times \IZ) \cong \IZ \times \IZ$ is not finite. + + - property: balanced + proof: 'The homomorphism $(2,2) : \IZ \times \IZ \to \IZ \times \IZ$ is a counterexample.' + + - property: Cauchy complete + proof: 'The idempotent endomorphism $(1,0) : \IZ \times \IZ \to \IZ \times \IZ$ does not split.' + +special_objects: + initial object: + description: trivial module + terminal object: + description: trivial module + coproducts: + description: '[finite case] direct sums' + products: + description: '[finite case] direct sums' + +special_morphisms: + isomorphisms: + description: bijective homomorphisms + proof: It is a full subcategory of $R{-}\Mod$ for $R = \IZ \times \IZ$, and we already know that the isomorphisms in $R{-}\Mod$ are the bijective homomorphisms. + monomorphisms: + description: injective homomorphisms + proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable, hence preserves monomorphisms. + epimorphisms: + description: >- + More generally, let $R$ be a commutative Noetherian ring, and let $f : R^n \to R^m$ be a linear map represented by a matrix $A \in M_{m \times n}(R)$. Let $I_m(A)$ be the ideal generated by the $m \times m$-minors of $A$. The following are equivalent: +
    +
  1. $f$ is an epimorphism in $\Free_{\fg}(R)$.
    2. +
  2. We have $\Ann(I_m(A))=0$.
    3. +
  3. The ideal $I_m(A)$ contains a regular element of $R$.
    4. +
  4. If $\coker(f)$ denotes the cokernel in $R{-}\Mod$, then $\Ann(\coker(f))$ contains a regular element of $R$.
    5. +
  5. The localized map $f \otimes \id_K : K^n \to K^m$ is surjective, where $K$ is the total ring of fractions of $R$.
    6. +
+ proof: >- + (1) $\iff$ (2): $~$ Condition (1) is clearly equivalent to the condition that the dual linear map + $$f^* : \underline{\Hom}(R^m,R) \to \underline{\Hom}(R^n,R)$$ + is injective. This identifies with a linear map $R^m \to R^n$, which is represented by the transpose matrix $A^T \in M_{n \times m}(R)$. By McCoy's rank theorem (Theorem 51 on p. 159 in: McCoy, Rings an ideals, Carus Math. Monographs, Vol. 8), $A^T$ represents an injective linear map if and only if $\Ann(I_m(A^T))=0$. But $I_m(A^T)=I_m(A)$. Thus, (1) is equivalent to (2). + + + (2) $\iff$ (3): $~$ The implication (3) $\implies$ (2) is trivial. Now assume that (3) does not hold, i.e. $I_m(A)$ contains no regular element, i.e. is contained in the set of zero divisors. Since $R$ is Noetherian, the set of zero divisors is the finite union of the associated primes (of the zero ideal). Thus, by the Prime Avoidance Lemma, $I_m(A) \subseteq P$ for some associated prime $P$, say $P = \Ann(x)$ for some $x \neq 0$. Then $x \in \Ann(I_m(A))$, which shows that (2) does not hold. + + + (3) $\implies$ (4): $~$ It suffices to prove that $I_m(A) \subseteq \Ann(\coker(f))$. For this, it suffices to prove that $\det(A') \in \Ann(\coker(f))$, where $A'$ is any $m \times m$-submatrix of $A$. By Cramer's Rule, + $$A' \cdot \adj(A') = \det(A') \cdot 1.$$ + Thus, for every $x \in R^m$ we have + $$\det(A') \, x \in \im(A') \subseteq \im(A),$$ + and hence $\det(A') \, [x] = 0$ in $\coker(f)$. + + + (4) $\implies$ (3): $~$ Assume $\coker(f)$ is annihilated by some regular element $r \in R$. Thus, $r e_i \in \im(A)$ for every $1 \leq i \leq m$. It follows that there is some matrix $B \in M_{n \times m}(R)$ with $AB = r 1$. By the Cauchy-Binet formula, + $$\textstyle r^m = \det(AB) = \sum_{\card(J)=m} \det(A_J) \det(B_J),$$ + where $A_J$ is the submatrix of $A$ which selects the columns in $J$. This shows that the regular element $r^m$ is contained in $I_m(A)$. + + + (4) $\iff$ (5): $~$ Since $(-) \otimes_R K$ is right exact, condition (5) says that $\coker(f) \otimes_R K = 0$. Since $K$ is the localization of $R$ by the subset of regular elements, this means that every element of $\coker(f)$ is annihilated by some regular element of $R$. Since $\coker(f)$ is finitely generated, this is equivalent to (4). diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index 0a8e7546..bd247539 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -13,6 +13,7 @@ tags: related: - Haus - Top + - Euclid_coprod satisfied_properties: - property: locally small diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index cbd03159..8dc57a70 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -15,6 +15,7 @@ related: - Met_oo - Top - Unif + - Euclid_coprod satisfied_properties: - property: locally small @@ -75,6 +76,7 @@ satisfied_properties: This makes it impossible for $\varphi$ to be continuous at $y$, giving a contradiction. Finally, since we have shown $f$ is bijective on underlying sets, to show $f$ is a homeomorphism, it suffices to show that $f$ is closed. Thus, let $F \subseteq X$ be closed. Then $d({-}, F) : X \to \IR$ is a continuous function, so there exists $\varphi : Y \to \IR$ such that $\varphi(f(x)) = d(x, F)$ for each $x\in X$. That implies that $f_*(F) = \{ y\in Y : \varphi(y) = 0 \}$ is closed. + label: Met_c_cogenerator unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Proj_fg(Re).yaml b/database/data/categories/Proj_fg(Re).yaml index 8abfbe52..d184b93a 100644 --- a/database/data/categories/Proj_fg(Re).yaml +++ b/database/data/categories/Proj_fg(Re).yaml @@ -15,6 +15,7 @@ related: - R-Mod - FreeAb_fg - FinVect_u + - Free_fg(ZxZ) satisfied_properties: - property: locally small diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index 219cd737..f717797b 100644 --- a/database/data/categories/R-Mod.yaml +++ b/database/data/categories/R-Mod.yaml @@ -15,6 +15,7 @@ related: - Vect - grMod_G(R) - Proj_fg(Re) + - Free_fg(ZxZ) satisfied_properties: - property: locally small diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 060551b7..84c7e6c5 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -17,6 +17,7 @@ related: - Man - Unif - Meas + - Euclid_coprod satisfied_properties: - property: locally small diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 3a68c46e..5779bd24 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -50,11 +50,13 @@ \Bilin: \operatorname{Bilin} \Ob: \operatorname{Ob} \id: \operatorname{id} +\adj: \operatorname{adj} \ev: \operatorname{ev} \even: \operatorname{even} \odd: \operatorname{odd} \card: \operatorname{card} \colim: \operatorname{colim} +\coker: \operatorname{coker} \im: \operatorname{im} \coim: \operatorname{coim} \lcm: \operatorname{lcm} @@ -72,6 +74,7 @@ \rank: \operatorname{rank} \Gal: \operatorname{Gal} \Alt: \operatorname{Alt} +\Ann: \operatorname{Ann} \Open: \operatorname{Open} \Id: \operatorname{Id} \Br: \operatorname{Br} @@ -98,10 +101,12 @@ \CMon: \mathbf{CMon} \Mod: \mathbf{Mod} \grMod: \mathbf{grMod} +\Euclid: \mathbf{Euclid} \Fld: \mathbf{Fld} \FinAb: \mathbf{FinAb} \FinGrp: \mathbf{FinGrp} \FreeAb: \mathbf{FreeAb} +\Free: \mathbf{Free} \TorsFreeAb: \mathbf{TorsFreeAb} \TorsAb: \mathbf{TorsAb} \Cat: \mathbf{Cat}