Add extremal (co)generating sets and single extremal (co)generators

[dschepler]

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.)

[ScriptRaccoon]

FYI #283 means that the files have changed their location, so a (trivial) rebasing is required.

[ScriptRaccoon]

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?

[dschepler]

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 $\Sigma_n$ is an extremal cogenerating set for $\Sigma_n-Set$, and then take products and finally the tuple of those products?)

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.

[dschepler]

Some comments on some of the remaining undecided cases:

For TorsFreeAb: Extremal cogenerator / cogenerating set would be equivalent. We could conjecture that the family of localizations of Z might work. But if it does, I haven't found a simple proof. A sample case to illustrate the difficulties (constructed partially with the aid of AI): the subgroup of Q^2 generated by Z^2 and $(1/2^k, 3/2^k)$ for k=1,2,... Since the category is coregular, the extremal monomorphisms are regular monomorphisms; so we are looking for a saturated embedding of that group into a product of localizations. The map G -> Z[1/2] x Z[1/2] x Z, $(x,y) \mapsto (x, y, 3x-y)$, appears to work for that case, but has a twist required to get it to work. It's easy to imagine more complex examples requiring more and more complex twists, and maybe even a possibility of constructing a counterexample where "too many twists are required" to be able to build a valid map.

For FreeAb: Given the difficulties with infinite products, and that infinite-dimensional free abelian groups probably can't be cut out as regular subobjects of the product in Ab, it seems likely that Z won't work as an extremal cogenerator. In fact, it seems unlikely for any small set of free abelian groups (with limited cardinalities of generating sets) to work as an extremal cogenerating set. But I haven't been able to find a proof of either assertion.

For the various metric space categories with non-expansive maps as morphisms: R doesn't work as an extremal cogenerator, for example because it can't detect the failure of (0,1) -> [0,1] to be an isomorphism. That suggests that any extremal cogenerating set would probably have to contain lots of objects to detect various forms of failure to be complete, perhaps too many to form a set. I haven't succeeded in finding a proof along those lines, though (beyond vague ideas such as considering spaces formed by a pushout of $\kappa$ copies of R joined at a single point, and the inclusion of the space with that point removed).

Then there's still the question whether the category of combinatorial species has a single extremal cogenerator, which I still haven't quite managed to get a good grasp on.

[dschepler]

Looking at the proof I added that TorsFreeAb has $Q \times \prod_p Z_p$ as an extremal cogenerator, I wonder how many other proofs I could simplify by applying the same pattern: prove the canonical map to a product is in fact a regular monomorphism, using already established descriptions of products and regular monomorphisms (and dually for generators of course). For example, looking at the proofs in Ban, I can definitely see that strategy applying there.

If you want, I can look into this; or, we can merge this for now and I can create another PR within a couple days to make those simplifications.

[ScriptRaccoon]

I need some time to fully review the PR which I haven't done so far. My comments were only after skimming through it.

[ScriptRaccoon]

This is the first part of my review. I will have a look at the rest later.

[ScriptRaccoon]

Then for any $x \in X$, by the Hahn-Banach theorem, there exists $\varphi \in X^*$ such that $|\varphi| = 1$ and $\varphi(x) = |x|$.

As commented before, this is not true for, say, $X = 0$. I think we should assume $x \neq 0$.

[ScriptRaccoon]

As commented before, the norms are missing in

Therefore, $|x| = \psi(f(x)) \le |f(x)|$;

[ScriptRaccoon]

I assume we are using the following fact?

If C is a full subcategory of D and X is an object in C which is an extremal generator in D, then it is an extremal generator in C.

This is trivial, but it is used so much (see the other comments below) that maybe we can add it to subcategories.md. Either way, I would like to mention this somewhere.

[ScriptRaccoon]

To make this more similar to $\Delta$, cannot we say again that it is even an extremal generator in PreOrd and then use the fact that I have mentioned there?

[ScriptRaccoon]

Suggested change

Now, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f : \Hom(Q, \{0<1\}) \to \Hom(P, \{0<1\})$ is a bijection. Since it is injective and $\{0<1\}$ is a cogenerator, we get that $f$ is an epimorphism and therefore surjective on the underlying sets (see below). On the other hand, the fact that ${-} \circ f$ induces a bijection of upper sets implies that $f$ is also injective on the underlying sets, and also that $f(a_1) \le f(a_2)$ implies $a_1 \le a_2$. Therefore, $f$ is an isomorphism.

Now, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f : \Hom(Q, \{0<1\}) \to \Hom(P, \{0<1\})$ is a bijection. Since it is injective and $\{0<1\}$ is a cogenerator, we get that $f$ is an epimorphism and therefore surjective on the underlying sets (see below). On the other hand, the fact that $f$ induces a bijection of upper sets implies that $f$ is also injective on the underlying sets, and also that $f(a_1) \le f(a_2)$ implies $a_1 \le a_2$. Therefore, $f$ is an isomorphism.

[ScriptRaccoon]

As in my other comments: Let's try to make this clear that not an extra proof is needed, but that this can be deduced from the general lemma.

[ScriptRaccoon]

Suggested change

Now, suppose we have a surjective morphism $f : X \to Y$ of finite sets such that ${-} \circ f : \Hom(Y, \{0,1\}) \to \Hom(X, \{0,1\})$ is bijective. That means that $f^* : P(Y) \to P(X)$ is bijective on non-empty subsets, and it certainly also maps $\varnothing \mapsto \varnothing$. Therefore, since the <a href="/functor/power_set_contravariant">contravariant powerset functor</a> is conservative, that implies $f$ is an isomorphism.

Now, suppose we have a surjective map $f : X \to Y$ of finite sets such that ${-} \circ f : \Hom(Y, \{0,1\}) \to \Hom(X, \{0,1\})$ is bijective. That means that $f^* : P(Y) \to P(X)$ is bijective on non-empty proper subsets, and it certainly also maps $\varnothing \mapsto \varnothing$ and $Y \mapsto X$. Therefore, since the <a href="/functor/power_set_contravariant">contravariant powerset functor</a> is conservative, that implies $f$ is an isomorphism.

[ScriptRaccoon]

As before, let's rather use that Z is an extremal generator in Grp which happens to be in the subcategory.

[ScriptRaccoon]

Thanks for adding this result!

Nit:

Suggested change

proof: 'It is easy to see that a faithful functor $F$ reflects monomorphisms: If we have two morphisms $x_1, x_2 : U \to X$ and $f : X \to Y$ such that $f(x_1) = f(x_2)$, and $F(f)$ is a monomorphism, then $F(x_1) = F(x_2)$; therefore, $x_1 = x_2$, so $f$ is also a monomorphism. The dual argument shows that $F$ also reflects epimorphisms. Therefore, if $F(f)$ is an isomorphism, then $f$ is both a monomorphism and an epimorphism; by the assumption on the domain category, this implies that $f$ is an isomorphism.'

proof: 'It is easy to see that a faithful functor $F$ reflects monomorphisms: If we have two morphisms $x_1, x_2 : U \rightrightarrows X$ and $f : X \to Y$ such that $f(x_1) = f(x_2)$, and $F(f)$ is a monomorphism, then $F(x_1) = F(x_2)$; therefore, $x_1 = x_2$, so $f$ is also a monomorphism. The dual argument shows that $F$ also reflects epimorphisms. Therefore, if $F(f)$ is an isomorphism, then $f$ is both a monomorphism and an epimorphism; by the assumption on the domain category, this implies that $f$ is an isomorphism.'

[ScriptRaccoon]

Notice that the assumption "right cancellative" should be "left cancellative". (Luckily, this doesn't make a difference since the implication is only applied to On.)

I also made some other improvements below.

- id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set
  assumptions:
    - locally finite
    - left cancellative
    - semi-strongly connected
    - extremal generating set
  conclusions:
    - essentially small
  proof: >-
    Suppose a category $\C$ is locally finite, left cancellative, semi-strongly connected, and has an extremal generating set $S$. We then claim that
    $$\Ob(\C) \to \IN^S, \, X \mapsto (G \mapsto \card(\Hom(G, X)))$$
    is injective on isomorphism classes of $\Ob(\C)$. To see this, suppose two objects $X$ and $Y$ map into the same cardinality tuple. Since $\C$ is semi-strongly connected, we may assume without loss of generality that there is a morphism $f : X \to Y$. Then since $f$ is a monomorphism, for each $G \in S$ we have
    $$f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$$
    is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating set, we thus have $f$ is an isomorphism.

    This shows that the collection of isomorphism classes of objects of $X$ is in bijection with a set. Together with the assumption that the category is locally finite, this implies the category is essentially small.

[ScriptRaccoon]

A couple more comments.

[ScriptRaccoon]

Let's use the Yoneda Lemma instead.

[ScriptRaccoon]

See my comment for FinSet.

[ScriptRaccoon]

See my comment for FinSet.

[ScriptRaccoon]

See my comment for FinSet.

[ScriptRaccoon]

This is not correct. The object [0] is a generator, but not an extremal generator.

[dschepler]

By the way, I think I've found proofs that $(0, \infty)$ is an extremal cogenerator for Met; similarly $(0, \infty]$ is an extremal cogenerator for $\mathbf{Met}_\infty$; and $[0, \infty) \sqcup { 0' }$ is an extremal cogenerator for PMet. Is it OK for me to add these now, or should I wait until after the current review is done so you don't have a moving target?

[ScriptRaccoon]

Is it OK for me to add these now

Yes, in a new commit is fine!

[ScriptRaccoon]

Another chunk of comments. (not the final one, 11 files are left to review)

[ScriptRaccoon]

Suggested change

	To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $\im(f) \cap \kappa$. This is a subset of $\kappa$ whose cardinality is strictly less than $\kappa$, so its supremum $\alpha$ is also less than $\kappa$. Therefore, $f^*(\{ \kappa \}) = f^*((\alpha, \kappa])$ is open, showing that $f$ is also continuous as a function $G \to \kappa \sqcup \{ \kappa \}$.
	To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $T := \im(f) \cap \kappa$. Then $T \subseteq \kappa$ and $\card(T) \leq \card(G) < \kappa$. Since $\kappa$ is regular, this implies $\alpha := \sup(T) < \kappa$. Therefore, $f^*(\{ \kappa \}) = f^*((\alpha, \kappa])$ is open, showing that $f$ is also continuous as a function $G \to \kappa \sqcup \{ \kappa \}$.

[ScriptRaccoon]

Remark: I like this new and even stronger proof that no extremal generating set exists much more than the previous one that no small dense subcategory exists (which referenced https://math.stackexchange.com/questions/4097315/).

[ScriptRaccoon]

Suggested change

Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. We then claim that $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ is a bijection for every $G \in S$, showing that $S$ cannot be an extremal generating set. Here we use the standard order topology on both $\kappa$ and $\kappa + 1$.

Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. Equip ordinal numbers with the order topology as usual. We then claim that the canonical continuous bijection $\kappa \sqcup \{ \kappa \} \to \kappa + 1$, which is not a homeomorphism, induces a bijection $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ for every $G \in S$, showing that $S$ cannot be an extremal generating set.

[ScriptRaccoon]

Suggested change

It is easily checked that the indiscrete two-point space is a cogenerator. We claim that adding the Sierpinski space $(\{ 0, 1 \}, \{ \varnothing, \{ 1 \}, \{ 0, 1 \} \})$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection.

It is easily checked that the indiscrete two-point space is a cogenerator, using that the two-element set is a cogenerator in $\Set$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. That is, $f$ is a homeomorphism.

The definition of the Sierpinski space doesn't need to be repeated since it is already used anyway in various places (even here in Top.yaml); in doubt we can add a link to Wikipedia.

Also, this is an interesting characterization of homeomorphism which most texts on general topology do not mention, right?

Here is the easy proof + generalization: Let $f : X \to Y$ be a surjective map which induces a surjection on open sets via pullback. Let $U \subseteq X$ be open. By assumption there is an open subset $V \subseteq Y$ with $U = f^*(V)$. Then $f_*(U) = f_*(f^*(V)) = V$, the last step uses that $f$ is surjective. Thus, $f$ is an open map.

[ScriptRaccoon]

I am not 100% sure if we should remove this (even if it is redundant), since this is a very instructive proof which many people should know. WDYT?

We can definitely remove it for pointed spaces since this is just a boring variation of the proof for spaces.

[ScriptRaccoon]

Let's add a reference to the extremal cogenerator in Set_*.

[ScriptRaccoon]

Let's use T_p for the tanget space.

As you say, it consists of equivalence classes of curves. I think the proof needs to mention the equivalence relation, otherwise it cannot be complete.

Also, let's cite the inverse function theorem in the end: it shows that $f$ is a local diffeo. Since $f$ is bijective, it is a diffeo.

Actually, we only need to show that $f$ is surjective on tangent spaces. Then we can apply the submersion theorem. The fibers are $0$-dimensional, so we can finish.

[ScriptRaccoon]

(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.

[ScriptRaccoon]

Let's write $\psi(p) \coloneqq \frac{1}{1 - \phi(f(p))}$ in display math ($$).

[ScriptRaccoon]

Suggested change

Now, recall that the tangent space of $M$ at a point $p$ is defined as the space of $\IR$-linear functions $\partial : C^\infty(M) \to \IR$ such that $\partial(\varphi \psi) = \varphi(p) \partial(\psi) + \psi(p) \partial(\varphi)$; and similarly for the tangent space of $N$ at $f(p)$. (Alternately, some authors might use germs of functions near $p$; however, such germs are easy to extend to global smooth functions with the same germ, via the technique of multiplying by a bump map.) Also, the push-forward $f_* : \T_{M,p} \to \T_{N,f(p)}$ is defined as composition with $f$. But by assumption, $f$ induces a bijection between $C^\infty(M)$ and $C^\infty(N)$, and it is easy to check that this restricts to an isomorphism $f_* : \T_{M,p} \to \T_{N,f(p)}$. Thus, $f$ is a diffeomorphism.

Now, recall that the tangent space $T_p(M)$ of $M$ at a point $p$ can be defined as the space of $\IR$-linear functions $\partial : C^\infty(M) \to \IR$ such that $\partial(fg) = f(p) \partial(g) + g(p) \partial(f)$; and similarly for the tangent space of $N$ at $f(p)$. Also, the push-forward $f_* : T_p(M) \to T_{f(p)}(N)$ is defined by precomposition with $f^* : C^\infty(N) \to C^\infty(M)$. But by assumption, $f^* : C^\infty(N) \to C^\infty(M)$ is a bijection, and it is easy to check that this restricts to an isomorphism $f_* : T_p(M) \to T_{f(p)}(N)$. Thus, by the inverse function theorem, $f$ is a local diffeomorphism. Since $f$ is bijective, $f$ must be a diffeomorphism.

Also, please fill in the details for "it is easy to check that". This is similar to the missing part in the other proof above. Basically, we need to prove that an algebraic condition is reflected, which is not guaranteed from a pure topological condition (from a high level POV, I haven't tried to write down the proof).

[dschepler]

The reason I used $\varphi$ and $\psi$ instead of $f$ and $g$ was because $f$ was already taken for the morphism in Man.

I guess a large bulk of the proof will essentially boil down to the fact that $f^*$ is automatically a morphism of $\mathbb{R}$-algebras, so if it's a bijection, its inverse will also be a morphism of $\mathbb{R}$-algebras.

[dschepler]

I think an alternate proof would be: Once you've shown $f$ is bijective, then show that $f$ must be open (and therefore a homeomorphism) using that a smooth bump map whose non-zero set corresponds to the unit open ball of a coordinate chart of $M$ induces a smooth map on $N$ whose non-zero set is therefore open; and these subsets of $M$ form a basis of the topology. Then, use the fact that smoothness of $f^{-1}$ is evaluated based on coordinate charts of $M$ and $N$, and the assumption on $f$ easily implies that there's a bijection between such coordinate charts.

[ScriptRaccoon]

Suggested change

	proof: >-
	The proof is similar to the one for <a href="/category/Top">$\Top$</a>. In this case, suppose $\kappa$ is an uncountable regular cardinal. We can then define $\M_\kappa$ to be the collection of subsets $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\kappa \in E$. This is easily checked to be a $\sigma$-algebra on $\kappa + 1$. Similarly, define $\M_\kappa'$ to be the $\sigma$-algebra generated by $\M_\kappa \cup \{ \{ \kappa \} \}$; this can be described as the set of $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta, \gamma \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\gamma \in E$.
	Now, suppose $S$ is a set of measurable spaces, and let $\kappa$ be an uncountable regular cardinal greater than $\card(G)$ for each $G \in S$. Then for any measurable function $f : G \to (\kappa + 1, \M_\kappa)$ with $G \in S$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that the $f$ factors through $(\kappa + 1, \M_\kappa')$. This shows that $\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$ is a bijection for each $G \in S$, implying that $S$ cannot be an extremal generating set.
	proof: >-
	The proof is similar to the one for <a href="/category/Top">$\Top$</a>. In this case, suppose $\kappa$ is an uncountable regular cardinal. We can then define $\M_\kappa$ to be the collection of subsets $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\kappa \in E$. This is easily checked to be a $\sigma$-algebra on $\kappa + 1$. Similarly, define $\M_\kappa'$ to be the $\sigma$-algebra generated by $\M_\kappa \cup \{ \{ \kappa \} \}$; this can be described as the set of $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta, \gamma \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\gamma \in E$.
	Now, suppose $S$ is a set of measurable spaces, and let $\kappa$ be an uncountable regular cardinal greater than $\card(G)$ for each $G \in S$. We claim that the bijective measurable map
	$$(\kappa+1, M_\kappa') \to (\kappa+1, \M_\kappa), \, \alpha \mapsto \alpha,$$
	which is not an isomorphism, induces a bijection
	$$\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$$
	for each $G \in S$, implying that $S$ cannot be an extremal generating set. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that the $f$ factors through $(\kappa + 1, \M_\kappa')$.

[ScriptRaccoon]

Why not removing this as you have done with several other categories where 1 was a generator?

[ScriptRaccoon]

Since $f$ is injective on underlying sets, the fact that this morphism is in the image of $f \circ {-}$ implies that $\delta \le d(f(x_1), f(x_2))$ also.

What is going on here?

[ScriptRaccoon]

On the other hand, there is a morphism $G \to Y$ which maps $\delta$ to $x_2$ and every other element of $\IR_{\ge 0}$ to $x_1$.

This is not a map to $Y$.

[ScriptRaccoon]

(not as a suggestion since git diff is misleading)

    proof: >-
      We claim that $\IR_+$ (where $0 \notin \IR+$) with metric inherited from the usual metric on $\IR$ is a cogenerator. Let $a,b \in X$ be two points of a metric space such that $f(a)=f(b)$ for all non-expansive maps $f : X \to \IR_+$. This applies in particular to $f(x) \coloneqq d(a,x)+1$ and shows that $1=d(a,a)+1=d(a,b)+1$, so that $a=b$.

      In fact, $\IR_+$ is an extremal cogenerator. To see this, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that ${-} \circ f : \Hom(Y, \IR_+) \to \Hom(X, \IR_+)$ is a bijection. First of all, since ${-} \circ f$ is injective and $\IR_+$ is a cogenerator, $f$ is an epimorphism, so it has dense image (see below). Now for each $x \in X$, we have a non-expansive map
      $$\varphi : X \to \IR_+, \,x' \mapsto d(x, x') + 1.$$
      By the assumption, there exists a non-expansive map $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. Therefore,
      $$\begin{align*}
      d(x, x') &= |d(x, x') - d(x, x)| \\
      & = |\varphi(x') - \varphi(x)| \\
      & = |\psi(f(x')) - \psi(f(x))| \\
      & \le d(f(x), f(x')) \\
      & \le d(x,x').
      \end{align*}$$
      This shows that $f$ is isometric, which in particular implies $f$ is injective on underlying sets.

      It remains to show $f$ is surjective on underlying sets. To see this, suppose to the contrary that we have $y \in Y \setminus f(X)$. Then we have a non-expansive map 
      $$\varphi : X \to \IR_+,\, x \mapsto d(y, f(x)).$$
      By the assumption on $f$, there exists a non-expansive map $\psi : Y \to \IR_+$ such that $\psi \circ f = \varphi$. However, since $\psi$ (seen as a function with codomain $\IR$) and $d(y, {-})$ are two continuous functions $Y \to \IR$ which agree on the dense subset $f(X)$, they must be the same function. Thus, $\psi(y) = d(y, y) = 0$, giving a contradiction.

[ScriptRaccoon]

Can also add a short remark why IR and IR_{>=0} are not extremal cogenerators? Can be as a comment.

[ScriptRaccoon]

I would remove this last paragraph since it has been said before (see suggestion above).

[ScriptRaccoon]

This is the final chunk of comments. I have now checked all the files.

[ScriptRaccoon]

The same proof as for <a href="/category/Met">$\Met$</a> shows that $\IR$ with the usual metric is a cogenerator.

Let's repeat the argument here. The reason is that Met now only mentions IR_+, and uses f(x) = d(a,x) + 1 instead of f(x) = d(a,x).

[ScriptRaccoon]

For long equations such as

$d(x_1, x_2) = \varphi(f(x_2)) = \varphi(f(x_1)) = d(x_1, x_1) = 0$

let's use display style. Let's also use display style for (in the paragraph below)

$X \to \IR$, $x \mapsto \frac{1}{d(f(x), y)}$

and the other formulas involving fractions.

Alternative: Write $a^{-1}$ instead of $\frac{1}{a}$.

[ScriptRaccoon]

Suggested change

	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.
	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.

[ScriptRaccoon]

Suggested change

	proof: 'The proof is similar to $\Met$: an extremal cogenerator is given by $\IR_+ \cup \{\infty\}$ with the metric in which $d(a,\infty)=\infty$ for $a \in \IR_+$. Then one checks that the maps $1 + d(a,-) : X \to \IR \cup \{\infty\}$ are non-expansive and finishes as for <a href="/category/Met">$\Met$</a>.'
	proof: 'The proof is similar to $\Met$: an extremal cogenerator is given by $\IR_+ \cup \{\infty\}$ with the metric in which $d(a,\infty)=\infty$ for $a \in \IR_+$. Then one checks that the maps $1 + d(a,-) : X \to \IR_+ \cup \{\infty\}$ are non-expansive and finishes as for <a href="/category/Met">$\Met$</a>.'

[ScriptRaccoon]

[...] the bijection of morphisms for that object implies that $f$ is a bijection $X \to Y$

We might again add a reference to the fact that the contravariant power set functor is conservative. Or that {0,1} is an extremal cogenerator in Set. But you can decide.

[ScriptRaccoon]

Why couldn't this be deduced before? Why does the extremal cogenerator give us an initial object? I tried to look through the generated properties, but this is not very enlightening.

[dschepler]

I guess before it auto-deduced having a cogenerator from initial object -> inhabited and the assignment of thin. But now the implication is extremal cogenerator -> cogenerator -> inhabited. And the rest is:

[ScriptRaccoon]

Thank you!

I suspect that there must be a much shorter deduction. Since the search page always finds the shortest deduction, this means that some implication is missing.

[ScriptRaccoon]

We might add an implication stating

thin + finite + binary products + inhabited => initial object

which is easy to prove. Even though it can be deduced from existing implications, the detour via ℵ₁-accessible categories and locally multi-presentable categories is wild. Also, we have no redundancy check for implications anyway, and even if so, the implication above would be marked as skipped.

I remember a similar discussion came up during the development of the redundancy script itself.

[dschepler]

(Though of course, an easier manual proof of thin + inhabited + essentially finite + binary products -> initial object would be to observe that the product of all objects must be weakly initial, and therefore initial since the category is thin.)

[dschepler]

On further reflection, I did an experiment adding an easy proof of sifted + thin -> filtered. Now the search for the other implication returns:

And even though "initial object" is still towards the end of the deduced properties, the justification now reads: Since it is cofiltered and is essentially finite and is thin, it has an initial object (by this result).
which is fairly close to the reasoning for the other implication.

[ScriptRaccoon]

Suggested change

proof: 'The object $1$ is a generator, since the only parallel pair of non-equal morphisms is $\id_1, ip : 1 \rightrightarrows 1$ with domain $1$. It is also an extremal generator since $\Hom(1, 0) = \{ p \}$ and $\Hom(1, 1) = \{ \id_1, ip \}$ are not bijective. The only other non-isomorphism to check is $ip : 1 \rightrightarrows 1$, where left multiplication by the non-unit $ip$ cannot induce a bijection on $\End(1)$.'

proof: 'The object $1$ is a generator, since the only parallel pair of non-equal morphisms is $\id_1, ip : 1 \rightrightarrows 1$ with domain $1$. It is also an extremal generator since $\Hom(1, 0) = \{ p \}$ and $\Hom(1, 1) = \{ \id_1, ip \}$ are not bijective. The only other non-isomorphism to check is $ip : 1 \to 1$, where left multiplication by the non-unit $ip$ cannot induce a bijection on $\End(1)$.'

[ScriptRaccoon]

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?

[ScriptRaccoon]

To see this, let $\{y_i : i \in I\}$ be a set

In the following, you write x_i.

Also, it would be good to specify that this is a subset of $G$.

[ScriptRaccoon]

Please write down a precise definition of $\varphi$ and in particular why it is well-defined.

I would do something like: Let $G/p^n G \to Z/p^n$ be the coordinate projection at $i_0$. These are compatible in $n$ (since the basis has been chosen uniformly), hence yield a homomorphism $G \to \lim_n G/p^n G \to \lim_n Z/p^n = Z_p$.

[ScriptRaccoon]

Looking at the proof I added that TorsFreeAb has Q × ∏ p Z p as an extremal cogenerator, I wonder how many other proofs I could simplify by applying the same pattern: prove the canonical map to a product is in fact a regular monomorphism, using already established descriptions of products and regular monomorphisms (and dually for generators of course). For example, looking at the proofs in Ban, I can definitely see that strategy applying there.

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.