Determine some accessibilities of Met

[ykawase5048]

I have added proofs for:

• Met is $\aleph_1$-accessible
• Met is not finitely accessible
• Met is not a generalized variety

[ScriptRaccoon]

Thanks a lot for your contribution!

I have checked the proofs and they look good. I have made some small adjustments, please check the changes and tell me if they are fine.

In the proof that Met is closed under ℵ₁-filtered colimits, I think we only need that I_∞ is ℵ₁-presentable, so I have changed this.

Notice: we can now remove the assignment that Met is well-powered; which I already did. In general, redundant assignments can be found via pnpm db:redundancies.

Since the proofs for "not finitely accessible" and "not filtered-colimit stable monos" are so similar (I also adjusted them accordingly and put them after another), I wonder if the implication

finitely accessible ===> filtered-colimit stable monos

is true. Currently, search has no counterexamples. I only know this for locally finitely presentable categories; these more generally have exact filtered colimits. This stronger properties is not satisfied by finitely accessible categories, though (search result). Maybe it becomes true if we have finite limits? Search does not find counterexamples.

Incidentally, the combination finitely accessible ∧ ¬filtered-colimit-stable monomorphisms is also mentioned on the page with missing data.

[ykawase5048]

I have checked the proofs and they look good. I have made some small adjustments, please check the changes and tell me if they are fine.

It looks better now. Thanks!

In the proof that Met is closed under ℵ1-filtered colimits, I think we only need that I∞ is ℵ1-presentable, so I have changed this.

Right, thanks.

Notice: we can now remove the assignment that Met is well-powered; which I already did. In general, redundant assignments can be found via pnpm db:redundancies.

I'll try it next time.

I wonder if the implication

finitely accessible ===> filtered-colimit stable monos

is true.

I think we need some additional assumption. But, I have no idea for now.
Unless I'm not mistaken, this holds without any additional assumptions:
For a finitely accessible category $A$, the canonical embedding $A\to Set^{A_{fp}}$ preserves all filtered colimits by definition of finitely presentable objects $P\in A_{fp}$, and also preserves any existing limits because it is simply a restriction of the Yoneda embedding.
Moreover, the embedding reflects the monicity of a morphism because the class of finitely presentable objects forms a generator in $A$. Then, the stability of monos is reduced to the case in $Set^{A_{fp}}$; hence true.

[dschepler]

Incidentally, this is closely related to assignments I made for Met in #280 regarding extremal generators and extremal generating sets (apparently called strong generators in Adamek-Rosicky). In particular, even though Met doesn't have coproducts, I was able to combine the extremal generating set of $I_\alpha$ into a single extremal generator, essentially as a pushout identifying all the base points.

[dschepler]

If we're adding to the Met page, I think we should be able to describe regular epimorphisms as: $f : X \to Y$ is a regular epimorphism if and only if (it is surjective so the following inf is finite and) for every $y, y'\in Y$, $d(y,y')$ is the inf of all $\sum_{i=0}^{n-1} d(x_i, x_{i+1}')$ where $f(x_0) = y$, $f(x_n') = y'$, and $f(x_i) = f(x_i')$ for $i=1, \ldots, n-1$. This would follow from the fact that a regular epimorphism must be the coequalizer of its kernel pair, along with the explicit construction of coequalizers.

(Though in the proof of the sufficiency part, we would probably need to include an argument along the lines that because the codomain is already a metric space, the pseudo-metric coequalizer already agrees with it, so applying the reflector equating points at distance zero does nothing.)

And for regular monomorphisms, I think they're the isometric embeddings of closed subsets. That's definitely a necessary condition. For sufficiency: if the domain is empty, use two maps into some $I_\alpha$ with $\alpha > 0$ to get an empty equalizer. If the domain is non-empty, then the $Met_\infty$ cokernel pair should also be in Met, and its equalizer will be the closure of the image.

Feel free to split this off into a new issue if you don't want to include it in this PR.

[ykawase5048]

Your description (in particular, of regular epi) is interesting! But it would be better to separate from this PR.

[ScriptRaccoon]

I agree, let's add the morphism info in a separate PR. I was also aware of the characterizations of regular epis already but didn't find it particular useful in practice which is why I didn't add it yet. It is very similar to the description of regular epis in Pos (which I didn't add yet for the same reason).

@ykawase5048
Thanks for providing the proof that finitely accessible categories have filtered-colimit-stable monos! Is it OK if I add it in a commit in this PR? Then I can also restructure other things I suppose. If you want to add it, let me know.

[ykawase5048]

@ScriptRaccoon
I'd really appreciate it if you could add the commit. However, I think this should be considered together with "exact filtered colimits". I opened an issue #300 about it.

[ScriptRaccoon]

@ScriptRaccoon I'd really appreciate it if you could add the commit.

Ok, I have added a commit. Please check it's OK. Then I will merge this PR.

However, I think this should be considered together with "exact filtered colimits". I opened an issue #300 about it.

That's true, but this can also be done in a second step. Let's merge this PR independently from this issue. Thanks for opening it!