Add extremal (co)generating sets and single extremal (co)generators#280
Add extremal (co)generating sets and single extremal (co)generators#280dschepler wants to merge 12 commits into
Conversation
|
FYI #283 means that the files have changed their location, so a (trivial) rebasing is required. |
ffcd1fc to
3e834b0
Compare
|
Remark: many proofs here show something stronger, or are close to that, namely that the set or object is a dense subcategory. This property is not here yet, but maybe we should add it soon. Not in this PR perhaps because it is already big, unless you think it clarifies the proofs much better. We can also have separate PRs then for the missing proofs. Btw, should I stop looking at this PR as long is it is in draft mode? |
No, comments and suggestions in the mean time are very useful. Incidentally, I've looked at the remaining unsettled cases, and they seem very tricky. I can maybe make more detailed comments later once I'm done with work for the day. (The exception is extremal cogenerator for Sp which seems like it should be doable if I could get my head around it better. Maybe something like the set of all quotients of So I should probably be able to take the PR out of draft status soon, and then we can decide on what questions to submit to MO and/or which categories we're OK with leaving unknown for the moment. |
9d5e193 to
57968df
Compare
|
By the way, I think I've found proofs that |
Yes, in a new commit is fine! |
ScriptRaccoon
left a comment
ScriptRaccoon
left a comment
There was a problem hiding this comment.
Another chunk of comments. (not the final one, 11 files are left to review)
| proof: >- | ||
| The manifold $\IR$ is a cogenerator, since for every smooth manifold $M$ and points $p \neq q$ in $M$ there is a smooth function $f : M \to \IR$ with $f(p) = 1$ and $f(q) = 0$ (John Lee, Introduction to Smooth Manifolds, Prop. 2.25). | ||
|
|
||
| In fact, $\IR$ is an extremal cogenerator. To see this, suppose we have a smooth map $f : M \to N$ such that ${-} \circ f : \Hom(N, \IR) \to \Hom(M, \IR)$ is a bijection. Then using bump maps as before to separate points of $M$, we can see that $f$ must be injective on underlying sets. Also, since $\IR$ is a cogenerator and ${-} \circ f$ is injective, we get that $f$ is an epimorphism, so it has dense image (see below). We claim that in fact, $f$ is surjective. To see this, suppose we had $q \in N \setminus \im(f)$. Then there is a bump map $\varphi : N \to \IR$ such that the image of $\varphi$ is contained in $[0,1]$, and $\varphi$ achieves value 1 only at $q$ (for example, $e^{-|x|^2}$ achieves this on $\IR^n$; then we can multiply by a bump function which is 1 on a neighborhood of the origin and which has compact support, and then transport this to a chart around $q$). But then we can construct a smooth function $\psi : M \to \IR$ by $\psi(p) \coloneqq \frac{1}{1 - \phi(f(p))}$. The corresponding function $N \to \IR$ must agree with $\frac{1}{1 - \phi}$ on the image of $f$. We can now get a contradiction from the fact that the image of $f$ is dense, and therefore contains a sequence of points converging to $q$, whereas the values of $\frac{1}{1 - \phi}$ on this sequence diverge to $\infty$. |
There was a problem hiding this comment.
(for example, $e^{-|x|^2}$ achieves this on $\IR^n$; then we can multiply by a bump function which is 1 on a neighborhood of the origin and which has compact support, and then transport this to a chart around $q$)
This repeats the proof of a general lemma. Let's find this lemma and cite it. I can also look in Lee's book if you want.
There was a problem hiding this comment.
That would be useful. (When I took differential geometry, we didn't have an assigned textbook and just took notes in class, so I don't have an introductory textbook to check for this.)
There was a problem hiding this comment.
I think it follows from this (in Lee's mentioned book, the pdf is just one google search away btw):
We need to shrink
ScriptRaccoon
left a comment
ScriptRaccoon
left a comment
There was a problem hiding this comment.
This is the final chunk of comments. I have now checked all the files.
| proof: >- | ||
| The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. | ||
|
|
||
| We claim that $S \coloneqq \{\IQ\} \cup \{\IZ_p : p \mathrm{~prime}\}$ is an extremal cogenerating set, where $\IZ_p$ is the additive group of the $p$-adic integers. To establish this, we will show that for any torsion-free group $G$, the canonical morphism $G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By the characterization below, this is equivalent to showing it is injective, and its image is a saturated subgroup. From the above, including $\IQ$ in $S$ is already sufficient to make it a monomorphism, i.e. an injective homomorphism. For the second part, it suffices to show for each prime $p$ that if $x\in G$ is not $p$-divisible, then its image in the product is not $p$-divisible. |
There was a problem hiding this comment.
For the second part, it suffices to show for each prime $p$ that if $x\in G$ is not $p$-divisible, then its image in the product is not $p$-divisible.
Why?
There was a problem hiding this comment.
Thanks for adding the details.
-
You have explained the prime reduction, but still: it requires a proof why
$A \subseteq B$ is regular mono, which means that$B/A$ is torsion-free, if and only if your divisibility condition, i.e.$A \cap nB = nA$ , is true. If$B/A$ is torsion-free and$a = nb$ , then$[b] \in B/A$ is$n$ -torsion, so trivial, so$b \in A$ , so$a \in nA$ , done. Conversely, if$A \cap nB = nA$ for all$n > 0$ , and$[b]$ is torsion, we have$nb \in A$ for some$n > 0$ . So$nb \in A \cap nB = nA$ , say$nb = na$ . Since$B$ is torsion-free, we get$b=a$ . Thus,$[b] = 0$ . (quickly written down, do not copy paste) -
The connection to
$B/A$ being torsion-free also offers an easier proof to the prime reduction. Namely, we prove that (a)$A \to B$ is regular mono, (b)$B/A$ is torsion-free, (c)$A \cap pB = pA$ for all primes$p$ , are equivalent, perhaps via (a) => (b) => (c) => (b) => (a). -
Can you please move all of this to the description of regular monos in the bottom of the page, and add a reference to this description?
After having read through the whole PR, I now understand what you mean here. Yes, this is a good idea, but this is a good opportunity for a follow-up PR. Let's try to finish and merge the current state first. There are always improvements we can make, for example also using the already mentioned dense subcategories. |
|
I don't know why the e2e test for "user can open a proof for a deduced satisfied property of category" is failing. The code looks fine, and it also works locally. I reran the test on GitHub, but it gives the same error. For now, I think you can ignore this issue. I need to make the tests more reliable (also on my side they sometimes fail randomly for obscure reasons). If it keeps failing and it blocks us from merging, just uncomment the test case and I try to fix it after merging. |
|
Ah, right, I incorporated the suggestion to make explicit assignments of "Set has an extremal generator" for use in full subcategories, which would have broken the expected text (and even the expectation that it's testing a deduced satisfied property). I could switch that test back to testing the "generator" property, with the text that it's deduced from having an extremal generator. |
Oups, even though I was on your branch with the latest changes, I forgot to update the database. Now it also fails. Let us just replace the category by, say, Ring.
The rest of the test 'user can open a proof for a deduced satisfied property of category' can stay as is. By the way, did you check out |
…uivalence; use that to rework the proof that the walking span has an extremal cogenerator
|
I think I've now addressed all the comments, except for a couple which need more input. |
|
|
||
| - property: extremal cogenerating set | ||
| proof: >- | ||
| Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space denoted with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating set of $\FiltVect_K$. |
There was a problem hiding this comment.
denote the vector space denoted (Typo)
$F_n(V)^\perp \hookrightarrow V$ (Typo, it should be the dual space)
| proof: >- | ||
| Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space denoted with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating set of $\FiltVect_K$. | ||
|
|
||
| First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, F')$ such that ${-} \circ f : \Hom((W, F'), K_\infty) \to \Hom((V, F), K_\infty)$ is a bijection. This implies that $f^* : W^* \to V^*$ is an isomorphism of the dual vector spaces. But since $K$ is a cogenerator of $\Vect_K$ and $\Vect_K$ is balanced, in fact $K$ is an extremal cogenerator of $\Vect_K$; so from $f^*$ being an isomorphism, we conclude $f : V \to W$ is an isomorphism of vector spaces. |
There was a problem hiding this comment.
Please use display math for ${-} \circ f : \Hom((W, F'), K_\infty) \to \Hom((V, F), K_\infty)$
- this avoids the broken formula (cf. Fix word breaks in katex formulas #135, my bad this is not fixed yet)
- it gives the text more space to breathe
- it is easier to read
|
|
||
| First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, F')$ such that ${-} \circ f : \Hom((W, F'), K_\infty) \to \Hom((V, F), K_\infty)$ is a bijection. This implies that $f^* : W^* \to V^*$ is an isomorphism of the dual vector spaces. But since $K$ is a cogenerator of $\Vect_K$ and $\Vect_K$ is balanced, in fact $K$ is an extremal cogenerator of $\Vect_K$; so from $f^*$ being an isomorphism, we conclude $f : V \to W$ is an isomorphism of vector spaces. | ||
|
|
||
| It remains to show that if $f$ also induces a bijection ${-} \circ f : \Hom((W, F'), K_n) \to \Hom(V, F), K_n)$ for each $n$, then $f$ induces an isomorphism of the filtrations. For this step, we may assume without loss of generality that $f = \id_V : V \to V$. By the observations above, this then reduces to showing that if $S_1^\perp = S_2^\perp$ where $S_1 \coloneqq F_n(V), S_2 \coloneqq F_n'(V)$ are subspaces of $V$ such that $S_1^\perp = S_2^\perp$, then $S_1 = S_2$. However, if we had $x \in S_1 \setminus S_2$, then starting with a basis of $S_2$, adjoining $x$, and then extending to a basis of $V$, we see that there is a functional $\varphi \in V^*$ such that $\varphi |_{S_2} = 0$ and $\varphi(x) = 1$. But then $\varphi \in S_2^* \setminus S_1^*$, giving a contradiction. This shows $S_1 \subseteq S_2$; and similarly $S_2 \subseteq S_1$. |
There was a problem hiding this comment.
Please use display math for ${-} \circ f : \Hom((W, F'), K_n) \to \Hom(V, F), K_n)$
| proof: >- | ||
| Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space denoted with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating set of $\FiltVect_K$. | ||
|
|
||
| First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, F')$ such that ${-} \circ f : \Hom((W, F'), K_\infty) \to \Hom((V, F), K_\infty)$ is a bijection. This implies that $f^* : W^* \to V^*$ is an isomorphism of the dual vector spaces. But since $K$ is a cogenerator of $\Vect_K$ and $\Vect_K$ is balanced, in fact $K$ is an extremal cogenerator of $\Vect_K$; so from $f^*$ being an isomorphism, we conclude $f : V \to W$ is an isomorphism of vector spaces. |
There was a problem hiding this comment.
`But since
Let's not repeat linear algebra here. Just use that the dual vector space is conservative.
There was a problem hiding this comment.
(In fact I wanted to link to the functor page but then realized it currently doesn't exist...)
|
|
||
| First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, F')$ such that ${-} \circ f : \Hom((W, F'), K_\infty) \to \Hom((V, F), K_\infty)$ is a bijection. This implies that $f^* : W^* \to V^*$ is an isomorphism of the dual vector spaces. But since $K$ is a cogenerator of $\Vect_K$ and $\Vect_K$ is balanced, in fact $K$ is an extremal cogenerator of $\Vect_K$; so from $f^*$ being an isomorphism, we conclude $f : V \to W$ is an isomorphism of vector spaces. | ||
|
|
||
| It remains to show that if $f$ also induces a bijection ${-} \circ f : \Hom((W, F'), K_n) \to \Hom(V, F), K_n)$ for each $n$, then $f$ induces an isomorphism of the filtrations. For this step, we may assume without loss of generality that $f = \id_V : V \to V$. By the observations above, this then reduces to showing that if $S_1^\perp = S_2^\perp$ where $S_1 \coloneqq F_n(V), S_2 \coloneqq F_n'(V)$ are subspaces of $V$ such that $S_1^\perp = S_2^\perp$, then $S_1 = S_2$. However, if we had $x \in S_1 \setminus S_2$, then starting with a basis of $S_2$, adjoining $x$, and then extending to a basis of $V$, we see that there is a functional $\varphi \in V^*$ such that $\varphi |_{S_2} = 0$ and $\varphi(x) = 1$. But then $\varphi \in S_2^* \setminus S_1^*$, giving a contradiction. This shows $S_1 \subseteq S_2$; and similarly $S_2 \subseteq S_1$. |
There was a problem hiding this comment.
However, if we had $x \in S_1 \setminus S_2$, then starting with a basis of $S_2$, adjoining $x$, and then extending to a basis of $V$, we see that there is a functional $\varphi \in V^*$ such that $\varphi |_{S_2} = 0$ and $\varphi(x) = 1$. But then $\varphi \in S_2^* \setminus S_1^*$, giving a contradiction. This shows $S_1 \subseteq S_2$; and similarly $S_2 \subseteq S_1$.
Let's not repeat linear algebra here. Let's just write "it is well-known from linear algebra that a subspace is determined by its orthogonal complement in the dual vector space" (or something like that).
|
|
||
| - property: generator | ||
| proof: The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\PMet \to \Set$. | ||
| - property: extremal generator |
There was a problem hiding this comment.
These are quite complicated proofs right in the top of the list of properties. To quote from contribution guidelines:
- Easy properties first: The order in which properties are assigned to a category (resp. functor) will also be shown on its page. For this reason, prefer an order in which the trivial and easy assignments appear first. More technical properties should usually appear later. Assignments of closely related properties should also be grouped together whenever possible.
So I would suggest to move them down a bit. Where exactly is of course a matter of preference, there is no precise rule for that. This remark also applies to most other categories in this PR. But it has no high priority, we can also omit this (for now), but it needs to be recorded as a TODO in an issue if it is omitted.
I don't know how familiar you are with VS Code shortcuts, but Option + Arrow Down moves the selected block down, which is very convenient when rearranging this kind of stuff.
| proof: The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\PMet \to \Set$. | ||
| - property: extremal generator | ||
| proof: >- | ||
| The proof will be similar to the one for <a href="/category/Met">$\Met$</a>. Namely, let $G$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$ for $x, y \in \IR_{ge 0}$, and $d(x, 0') = d(0', x) = x$ for $x \in \IR_{\ge 0}$. We will show $G$ is an extremal generator for $\PMet$. |
| proof: >- | ||
| The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. | ||
|
|
||
| We claim that $S \coloneqq \{\IQ\} \cup \{\IZ_p : p \mathrm{~prime}\}$ is an extremal cogenerating set, where $\IZ_p$ is the additive group of the $p$-adic integers. To establish this, we will show that for any torsion-free group $G$, the canonical morphism $G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By the characterization below, this is equivalent to showing it is injective, and its image is a saturated subgroup. From the above, including $\IQ$ in $S$ is already sufficient to make it a monomorphism, i.e. an injective homomorphism. For the second part, it suffices to show for each prime $p$ that if $x\in G$ is not $p$-divisible, then its image in the product is not $p$-divisible. |
There was a problem hiding this comment.
Thanks for adding the details.
-
You have explained the prime reduction, but still: it requires a proof why
$A \subseteq B$ is regular mono, which means that$B/A$ is torsion-free, if and only if your divisibility condition, i.e.$A \cap nB = nA$ , is true. If$B/A$ is torsion-free and$a = nb$ , then$[b] \in B/A$ is$n$ -torsion, so trivial, so$b \in A$ , so$a \in nA$ , done. Conversely, if$A \cap nB = nA$ for all$n > 0$ , and$[b]$ is torsion, we have$nb \in A$ for some$n > 0$ . So$nb \in A \cap nB = nA$ , say$nb = na$ . Since$B$ is torsion-free, we get$b=a$ . Thus,$[b] = 0$ . (quickly written down, do not copy paste) -
The connection to
$B/A$ being torsion-free also offers an easier proof to the prime reduction. Namely, we prove that (a)$A \to B$ is regular mono, (b)$B/A$ is torsion-free, (c)$A \cap pB = pA$ for all primes$p$ , are equivalent, perhaps via (a) => (b) => (c) => (b) => (a). -
Can you please move all of this to the description of regular monos in the bottom of the page, and add a reference to this description?
Co-authored-by: Script Raccoon <scriptraccoon@gmail.com>
Co-authored-by: Script Raccoon <scriptraccoon@gmail.com>
Co-authored-by: Script Raccoon <scriptraccoon@gmail.com>
2 participants
My primary motivation in the short term is to get "has an extremal generating set" into the database for use in entering one of the equivalent conditions in the Giraud-type theorem for Grothendieck quasitopoi. The property is, of course, of broader interest.
Current status:
extremal generator: 1 unknown
extremal generating set: 1 unknown
extremal cogenerator: 4 unknown
extremal cogenerating set: 4 unknown
(And all of these except for the case of FreeAb are cases where we still didn't even know whether they had generating/cogenerating sets.)