Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorKarol Szumiło
   • CommentTimeAug 16th 2018
   • PermaLink
   Author: Karol Szumiło
   Format: MarkdownItexIs there a complete (hopefully easily checkable) characterization of small categories $J$ such that the colimit functor $Set^J \to Set$ preserves monomorphisms? It seems that there should be some condition similar to filteredness (obviously it would need to be more general). Does anyone know of anything like that?

   Is there a complete (hopefully easily checkable) characterization of small categories $J$ such that the colimit functor $Set^J \to Set$ preserves monomorphisms? It seems that there should be some condition similar to filteredness (obviously it would need to be more general). Does anyone know of anything like that?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeAug 16th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't know of such.

   I don’t know of such.

3. • CommentRowNumber3.
   • CommentAuthorKarol Szumiło
   • CommentTimeAug 17th 2018
   • (edited Aug 17th 2018)
   • PermaLink
   Author: Karol Szumiło
   Format: MarkdownItexAfter thinking about it for a while, I guess I have an answer. But it is suspiciously simple and I am a little skeptical myself. I would appreciate it if somebody could check my argument. My claim: the colimit functor $Set^J \to Set$ preserves monomorphisms if and only if every span in $J$ can be completed to a commutative square. First, assume that every span can be completed and let $f \colon A \to B$ be a monomorphism of diagrams of sets over $J$. Let $a_0 \in A_{i_0}$ and $a_1 \in A_{i_1}$ be two elements such that $f a_0$ and $f a_1$ are identified in $colim B$. We need to show that $a_0 and a_1$ are identified in $colim A$. $f a_0$ and $f a_1$ are connected by a zig-zag of morphisms in the category of elements of $B$. By repeatedly completing the spans in that zig-zag, we can reduce it to a single cospan, i.e., we obtain morphisms $\phi_0 \colon i_0 \to k$ and $\phi_1 \colon i_1 \to k$ such that $\phi_0 f a_0 = \phi_1 f a_1$. Since $f$ is a monomorphism, we have $\phi_0 a_0 = \phi_1 a_1$ so $a_0$ and $a_1$ are identified in $colim A$. Conversely, assume that $J$ has a span $i_0 \leftarrow j \to i_1$ that cannot be completed to a square and let's construct a monomorphism that is not preserved. Take the map $J(i_0, -) \sqcup J(i_1, -) \to J(j, -)$ and its epi/mono factorization $J(i_0, -) \sqcup J(i_1, -) \to X \to J(j, -)$. Note that the images of $J(i_0, -)$ and $J(i_1, -)$ in $J(j, -)$ are disjoint since otherwise we could complete the span. Thus $X$ is the coproduct of two diagrams $X_0$ and $X_1$ that are quotients of $J(i_0, -)$ and $J(i_1, -)$. It follows that $colim X$ has two points while $colim J(j, -)$ has one, i.e., the monomorphism $X \to J(j, -)$ is not preserved. Does that sound right?

   After thinking about it for a while, I guess I have an answer. But it is suspiciously simple and I am a little skeptical myself. I would appreciate it if somebody could check my argument.

   My claim: the colimit functor $Set^J \to Set$ preserves monomorphisms if and only if every span in $J$ can be completed to a commutative square.

   First, assume that every span can be completed and let $f \colon A \to B$ be a monomorphism of diagrams of sets over $J$. Let $a_0 \in A_{i_0}$ and $a_1 \in A_{i_1}$ be two elements such that $f a_0$ and $f a_1$ are identified in $colim B$. We need to show that $a_0 and a_1$ are identified in $colim A$. $f a_0$ and $f a_1$ are connected by a zig-zag of morphisms in the category of elements of $B$. By repeatedly completing the spans in that zig-zag, we can reduce it to a single cospan, i.e., we obtain morphisms $\phi_0 \colon i_0 \to k$ and $\phi_1 \colon i_1 \to k$ such that $\phi_0 f a_0 = \phi_1 f a_1$. Since $f$ is a monomorphism, we have $\phi_0 a_0 = \phi_1 a_1$ so $a_0$ and $a_1$ are identified in $colim A$.

   Conversely, assume that $J$ has a span $i_0 \leftarrow j \to i_1$ that cannot be completed to a square and let’s construct a monomorphism that is not preserved. Take the map $J(i_0, -) \sqcup J(i_1, -) \to J(j, -)$ and its epi/mono factorization $J(i_0, -) \sqcup J(i_1, -) \to X \to J(j, -)$. Note that the images of $J(i_0, -)$ and $J(i_1, -)$ in $J(j, -)$ are disjoint since otherwise we could complete the span. Thus $X$ is the coproduct of two diagrams $X_0$ and $X_1$ that are quotients of $J(i_0, -)$ and $J(i_1, -)$. It follows that $colim X$ has two points while $colim J(j, -)$ has one, i.e., the monomorphism $X \to J(j, -)$ is not preserved.

   Does that sound right?

4. • CommentRowNumber4.
   • CommentAuthorRichard Williamson
   • CommentTimeAug 17th 2018
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexHi Karol, I have checked the first direction, and it looks completely correct to me! Clever! Very nice! No time for the converse direction just now.

   Hi Karol, I have checked the first direction, and it looks completely correct to me! Clever! Very nice!

   No time for the converse direction just now.

5. • CommentRowNumber5.
   • CommentAuthorRichard Williamson
   • CommentTimeAug 18th 2018
   • (edited Aug 18th 2018)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexTook a look at the converse direction now. All looks fine until the final sentence. It's probably obvious, but could you elaborate upon why $colim J(j,-)$ has exactly one point (I have the same question for the two parts of the computation of $colim X$)?

   Took a look at the converse direction now. All looks fine until the final sentence. It’s probably obvious, but could you elaborate upon why $colim J(j,-)$ has exactly one point (I have the same question for the two parts of the computation of $colim X$)?

6. • CommentRowNumber6.
   • CommentAuthorKarol Szumiło
   • CommentTimeAug 18th 2018
   • PermaLink
   Author: Karol Szumiło
   Format: MarkdownItexThank you for taking time to look at the argument. The colimit of a representable functor $J(j,-)$ is a one point set since elements of this functor are morphisms $j \to k$ and each of them is related to $id_j$ via itself. Since $X_0$ is a quotient of $J(i_0, -)$, its colimit is a quotient of the colimit of $J(i_0, -)$ so it is a one point set as well.

   Thank you for taking time to look at the argument. The colimit of a representable functor $J(j,-)$ is a one point set since elements of this functor are morphisms $j \to k$ and each of them is related to $id_j$ via itself. Since $X_0$ is a quotient of $J(i_0, -)$, its colimit is a quotient of the colimit of $J(i_0, -)$ so it is a one point set as well.

7. • CommentRowNumber7.
   • CommentAuthorRichard Williamson
   • CommentTimeAug 18th 2018
   • (edited Aug 18th 2018)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexThanks very much! I sort of got half way there, but in haste couldn't quite put the argument together. I see it now. Then I think both directions of the proof are completely correct. Very nice, and rather ingenious! We should put it on the nLab. I will do it eventually, if no-one gets there before me. Thinking about it, I would like to add to the nLab some kind of mechanism where we can see that a proof of some original argument has been checked by people. Any number of people could verify it, and just add their names to the list. If anyone formalises it, that could be added as well. We can use this argument as a test case (maybe it is in the literature somewhere, but that does not really matter). My question is how the user interface should look? Anybody have any suggestions? Maybe somewhere (suggestions please!) we can write 'Proof verified by 3 people' or something like that, which can be expanded to give the names of those people. This might eventually achieve some of the aims of the 'Publications of the nLab' project, but more incrementally and with a lower barrier; it could be a more transparent, flexible, and valuable form of peer review than traditional journal refereeing provides, though of course there is absolutely nothing in it to preclude use of a piece of mathematics checked in this way in a traditional journal article.

   Thanks very much! I sort of got half way there, but in haste couldn’t quite put the argument together. I see it now. Then I think both directions of the proof are completely correct. Very nice, and rather ingenious!

   We should put it on the nLab. I will do it eventually, if no-one gets there before me.

   Thinking about it, I would like to add to the nLab some kind of mechanism where we can see that a proof of some original argument has been checked by people. Any number of people could verify it, and just add their names to the list. If anyone formalises it, that could be added as well. We can use this argument as a test case (maybe it is in the literature somewhere, but that does not really matter). My question is how the user interface should look? Anybody have any suggestions? Maybe somewhere (suggestions please!) we can write ’Proof verified by 3 people’ or something like that, which can be expanded to give the names of those people.

   This might eventually achieve some of the aims of the ’Publications of the nLab’ project, but more incrementally and with a lower barrier; it could be a more transparent, flexible, and valuable form of peer review than traditional journal refereeing provides, though of course there is absolutely nothing in it to preclude use of a piece of mathematics checked in this way in a traditional journal article.

8. • CommentRowNumber8.
   • CommentAuthorRichard Williamson
   • CommentTimeAug 18th 2018
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexAs an aside, I think that the argument does not use (in either direction) the uniqueness part of the universal property of a colimit, i.e. works already for 'weak colimits' (i.e. just asking for a co-cone which has the required existence property).

   As an aside, I think that the argument does not use (in either direction) the uniqueness part of the universal property of a colimit, i.e. works already for ’weak colimits’ (i.e. just asking for a co-cone which has the required existence property).

9. • CommentRowNumber9.
   • CommentAuthorKarol Szumiło
   • CommentTimeAug 20th 2018
   • PermaLink
   Author: Karol Szumiło
   Format: MarkdownItexI'm not sure I follow your remark about weak colimits. Firstly, weak colimits are not functorial (at least not in any obvious sense), so I don't know what it means for them to preserve monomorphisms. I could imagine interpreting the statement as follows. Let $A \to B$ be a map of diagrams with some weak colimits $X$ and $Y$. Then the weak colimit cones will induce a (non-functorial, non-canonical) map $X \to Y$. Are you saying that any such map is a monomorphism provided that $A \to B$ is? That is not true. Take any diagram whose colimit has only one point, then you can always make a weak colimit by adding a new point and a map induced by identity back to the actual colimit will not be a monomorphism. Finally, I actually think that I used the full universal property in proofs in both directions. Namely, I used the explicit computation of colimits as $\pi_0$ of the categories of elements, that's not valid for weak colimits. If you had something else in mind, please clarify. I would be happy to put this on nLab when we sort out this issue, except I'm not sure what the right page would be.

   I’m not sure I follow your remark about weak colimits. Firstly, weak colimits are not functorial (at least not in any obvious sense), so I don’t know what it means for them to preserve monomorphisms. I could imagine interpreting the statement as follows. Let $A \to B$ be a map of diagrams with some weak colimits $X$ and $Y$. Then the weak colimit cones will induce a (non-functorial, non-canonical) map $X \to Y$. Are you saying that any such map is a monomorphism provided that $A \to B$ is? That is not true. Take any diagram whose colimit has only one point, then you can always make a weak colimit by adding a new point and a map induced by identity back to the actual colimit will not be a monomorphism. Finally, I actually think that I used the full universal property in proofs in both directions. Namely, I used the explicit computation of colimits as $\pi_0$ of the categories of elements, that’s not valid for weak colimits. If you had something else in mind, please clarify.

   I would be happy to put this on nLab when we sort out this issue, except I’m not sure what the right page would be.

10. • CommentRowNumber10.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItex>Finally, I actually think that I used the full universal property in proofs in both directions. Namely, I used the explicit computation of colimits as $\pi_{0}$ of the categories of elements, that’s not valid for weak colimits. Ah yes! Thanks very much. I would probably put this in a little bit more elementary way, but it makes no difference to your essential point, which is that you are relying on an explicit construction of a colimit of sets, at least in the first direction, and this explicit construction is not valid for weak colimits (yes, by the way, I was ignoring functionality, and you interpreted what I had in mind correctly!). Great to have that settled. Could you spell out where exactly you are using the explicit construction in the converse direction, not that it matters much?

    Finally, I actually think that I used the full universal property in proofs in both directions. Namely, I used the explicit computation of colimits as $\pi_{0}$ of the categories of elements, that’s not valid for weak colimits.

    Ah yes! Thanks very much. I would probably put this in a little bit more elementary way, but it makes no difference to your essential point, which is that you are relying on an explicit construction of a colimit of sets, at least in the first direction, and this explicit construction is not valid for weak colimits (yes, by the way, I was ignoring functionality, and you interpreted what I had in mind correctly!). Great to have that settled. Could you spell out where exactly you are using the explicit construction in the converse direction, not that it matters much?

11. • CommentRowNumber11.
    • CommentAuthorKarol Szumiło
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Karol Szumiło
    Format: MarkdownItexWhen I said this: > The colimit of a representable functor $J(j,-)$ is a one point set since elements of this functor are morphisms $j \to k$ and each of them is related to $id_j$ via itself. I was basically saying: the category of elements of $J(j, -)$ has an initial object (it is actually the slice $j \downarrow J$) hence it is connected.

    When I said this:

    The colimit of a representable functor $J(j,-)$ is a one point set since elements of this functor are morphisms $j \to k$ and each of them is related to $id_j$ via itself.

    I was basically saying: the category of elements of $J(j, -)$ has an initial object (it is actually the slice $j \downarrow J$) hence it is connected.

12. • CommentRowNumber12.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexHmm. The way I spelled out your quoted comment was as follows. We wish to show that a one point set $1$ is the colimit of $J(j,-)$. There is a unique map to $1$ from $J(j,j')$ for every $j' \in J$, and all the relevant triangles commute, so there is a unique choice of co-cone structure on it. Suppose that we have some other co-cone, $X$ say. We need to construct a morphism of co-cones from $1$ equipped with its unique co-cone structure to $X$. Let $c_j' : J(j,j') \rightarrow X$ denote the map which is part of the co-cone structure of $X$. What we can do is send the single element of $1$ to the image of $id: j \rightarrow j$ under $c_j : J(j,j) \rightarrow X$. Now, take an arrow $f : j \rightarrow j'$ of $J$. Since $X$ together with the maps $c_j'$ is a co-cone, we have that $c_{j'} \circ J(j, f) = c_j$. Applying this equation to $id : j \rightarrow j$, we obtain that $c_{j'}(f) = c_j(id_j)$. In other words, everything in $J(j,j')$ is sent to $c_j(id_j)$, for all $j' \in J$. (This computation is the heart of your quoted comment, as I see it). This means that sending the single element of $1$ to $c_j(id_j)$ defines a morphism of co-cones from $1$ to $X$. Moreover, this morphism of co-cones is obviously the unique possible one. We have thus shown that $1$ with its unique co-cone structure is the colimit of $J(j,-)$, as required. I do not think I am using anything here except the abstract definition of a colimit? In the first direction of your proof, on the other hand, we are definitely using the explicit construction of colimits in sets, for the step where you say that we have a zig-zag.

    Hmm. The way I spelled out your quoted comment was as follows. We wish to show that a one point set $1$ is the colimit of $J(j,-)$. There is a unique map to $1$ from $J(j,j')$ for every $j' \in J$, and all the relevant triangles commute, so there is a unique choice of co-cone structure on it. Suppose that we have some other co-cone, $X$ say. We need to construct a morphism of co-cones from $1$ equipped with its unique co-cone structure to $X$. Let $c_j' : J(j,j') \rightarrow X$ denote the map which is part of the co-cone structure of $X$. What we can do is send the single element of $1$ to the image of $id: j \rightarrow j$ under $c_j : J(j,j) \rightarrow X$. Now, take an arrow $f : j \rightarrow j'$ of $J$. Since $X$ together with the maps $c_j'$ is a co-cone, we have that $c_{j'} \circ J(j, f) = c_j$. Applying this equation to $id : j \rightarrow j$, we obtain that $c_{j'}(f) = c_j(id_j)$. In other words, everything in $J(j,j')$ is sent to $c_j(id_j)$, for all $j' \in J$. (This computation is the heart of your quoted comment, as I see it). This means that sending the single element of $1$ to $c_j(id_j)$ defines a morphism of co-cones from $1$ to $X$. Moreover, this morphism of co-cones is obviously the unique possible one. We have thus shown that $1$ with its unique co-cone structure is the colimit of $J(j,-)$, as required.

    I do not think I am using anything here except the abstract definition of a colimit?

    In the first direction of your proof, on the other hand, we are definitely using the explicit construction of colimits in sets, for the step where you say that we have a zig-zag.

13. • CommentRowNumber13.
    • CommentAuthorKarol Szumiło
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Karol Szumiło
    Format: MarkdownItexOh, sure. You can unpack the argument in various ways. The important thing is that the colimit of a representable functor has one element while a weak colimit could be any non-empty set so weak universal property is insufficient. What is more worthwhile, however, is to note that the second part of my argument is needlessly non-constructive. I think the proof could be rephrased to start with the assumption that $X \to J(j, -)$ is a monomorphism and construct a completion of the original span from that.

    Oh, sure. You can unpack the argument in various ways. The important thing is that the colimit of a representable functor has one element while a weak colimit could be any non-empty set so weak universal property is insufficient.

    What is more worthwhile, however, is to note that the second part of my argument is needlessly non-constructive. I think the proof could be rephrased to start with the assumption that $X \to J(j, -)$ is a monomorphism and construct a completion of the original span from that.

14. • CommentRowNumber14.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItex> I think the proof could be rephrased to start with the assumption that $X \to J(j, -)$ is a monomorphism and construct a completion of the original span from that. Yes, I agree that one could rephrase the second part of the argument in that way. I don't think one has epi-mono factorisations available in general in constructive mathematics, though, so I'm not sure it makes all that much difference from that point of view. I suspect also that the explicit characterisation of colimits in $\mathsf{Set}$ that you are using will not be valid in general constructively (one will be able to show that any such 'explicit' colimit is an actual colimit, but I doubt one can show the converse). > The important thing is that the colimit of a representable functor has one element while a weak colimit could be any non-empty set so weak universal property is insufficient. Yes, in case it was not clear, I certainly agree since #9 that one cannot use weak colimits in your argument, you need actual colimits. My point, just for completeness' sake, was that it seems you need the uniqueness part of the universal property only in one direction, and only to establish an isomorphism between the abstract definition of a colimit and an explicit construction of colimits for $\mathsf{Set}$. In other words, to summarise, what is precisely being used in your argument is that we have a weak colimit which can be computed in a certain way.

    I think the proof could be rephrased to start with the assumption that $X \to J(j, -)$ is a monomorphism and construct a completion of the original span from that.

    Yes, I agree that one could rephrase the second part of the argument in that way. I don’t think one has epi-mono factorisations available in general in constructive mathematics, though, so I’m not sure it makes all that much difference from that point of view. I suspect also that the explicit characterisation of colimits in $\mathsf{Set}$ that you are using will not be valid in general constructively (one will be able to show that any such ’explicit’ colimit is an actual colimit, but I doubt one can show the converse).

    The important thing is that the colimit of a representable functor has one element while a weak colimit could be any non-empty set so weak universal property is insufficient.

    Yes, in case it was not clear, I certainly agree since #9 that one cannot use weak colimits in your argument, you need actual colimits. My point, just for completeness’ sake, was that it seems you need the uniqueness part of the universal property only in one direction, and only to establish an isomorphism between the abstract definition of a colimit and an explicit construction of colimits for $\mathsf{Set}$. In other words, to summarise, what is precisely being used in your argument is that we have a weak colimit which can be computed in a certain way.

15. • CommentRowNumber15.
    • CommentAuthorKarol Szumiło
    • CommentTimeAug 20th 2018
    • PermaLink
    Author: Karol Szumiło
    Format: MarkdownItex> Yes, I agree that one could rephrase the second part of the argument in that way. I don't think one has epi-mono factorisations available in general in constructive mathematics, though, so I'm not sure it makes all that much difference from that point of view. I suspect also that the explicit characterisation of colimits in $\mathsf{Set}$ that you are using will not be valid in general constructively (one will be able to show that any such 'explicit' colimit is an actual colimit, but I doubt one can show the converse). Well, every topos has epi/mono factorizations and there should be a topos theoretic version of this characterization. (In fact, that's actually what I'm after. This question was supposed to be just a toy case for warm up.) What I mean is that for every small category $J$ and a topos $\mathcal{E}$ there should be a characterization of functors $F \colon J \to \mathcal{E}$ such that the left Kan extension $\mathsf{Set}^{J^op} \to \mathcal{E}$ preserves monomorphisms. Mac Lane and Moerdijk prove such result for preservation of finite limits, in which case the condition says that "the category of elements of $F$ is cofiltered" in a suitable internal sense. I would expect my criterion to internalize in a similar way, although I certainly don't claim that the argument above would, at least not without some serious work. (The proof of Mac Lane and Moerdijk is rather lengthy.)

    Yes, I agree that one could rephrase the second part of the argument in that way. I don’t think one has epi-mono factorisations available in general in constructive mathematics, though, so I’m not sure it makes all that much difference from that point of view. I suspect also that the explicit characterisation of colimits in $\mathsf{Set}$ that you are using will not be valid in general constructively (one will be able to show that any such ’explicit’ colimit is an actual colimit, but I doubt one can show the converse).

    Well, every topos has epi/mono factorizations and there should be a topos theoretic version of this characterization. (In fact, that’s actually what I’m after. This question was supposed to be just a toy case for warm up.) What I mean is that for every small category $J$ and a topos $\mathcal{E}$ there should be a characterization of functors $F \colon J \to \mathcal{E}$ such that the left Kan extension $\mathsf{Set}^{J^op} \to \mathcal{E}$ preserves monomorphisms. Mac Lane and Moerdijk prove such result for preservation of finite limits, in which case the condition says that “the category of elements of $F$ is cofiltered” in a suitable internal sense. I would expect my criterion to internalize in a similar way, although I certainly don’t claim that the argument above would, at least not without some serious work. (The proof of Mac Lane and Moerdijk is rather lengthy.)

16. • CommentRowNumber16.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItex> Well, every topos has epi/mono factorizations Mike and others will be able to give more authoritative opinions on this kind of thing, but I imagine that what you are referring to here is 'external', whereas presumably what you would need is an internal version, where you would need to use constructive logic. I think it is fairly easy to give a standard kind of Brouwerian counter-example to epi/mono factorisations existing constructively. Just take for instance a map $\mathbb{N} \rightarrow \mathbb{N} \times \mathbb{N}$ taking $n$ to $(p_{0}, p_{1}$), where $p_{0}$ is the smallest prime such that there is a prime $p_{1}$ with $p_{0} + p_{1} = 2n$ if such a $p_{0}$ exists, or else to $(0,0)$. One cannot (today at least!) determine the image of this map constructively, which one would need to construct the usual epi/mono factorisation. Maybe there are some ways to get around this that I do not know about, though. Anyhow, the most important thing is that I definitely think your proof is correct, and indeed, as I have said, I think it is a rather nice little piece of mathematics, and rather clever! I will happily take a look at any topos-theoretic generalisation.

    Well, every topos has epi/mono factorizations

    Mike and others will be able to give more authoritative opinions on this kind of thing, but I imagine that what you are referring to here is ’external’, whereas presumably what you would need is an internal version, where you would need to use constructive logic.

    I think it is fairly easy to give a standard kind of Brouwerian counter-example to epi/mono factorisations existing constructively. Just take for instance a map $\mathbb{N} \rightarrow \mathbb{N} \times \mathbb{N}$ taking $n$ to $(p_{0}, p_{1}$), where $p_{0}$ is the smallest prime such that there is a prime $p_{1}$ with $p_{0} + p_{1} = 2n$ if such a $p_{0}$ exists, or else to $(0,0)$. One cannot (today at least!) determine the image of this map constructively, which one would need to construct the usual epi/mono factorisation. Maybe there are some ways to get around this that I do not know about, though.

    Anyhow, the most important thing is that I definitely think your proof is correct, and indeed, as I have said, I think it is a rather nice little piece of mathematics, and rather clever! I will happily take a look at any topos-theoretic generalisation.

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeAug 20th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI have not read this thread in detail, and I probably won't, but it is perfectly true in many kinds of constructive mathematics that epi-mono factorizations exist, in particular the category of sets is an elementary topos and hence a pretopos, and that colimits therein can be constructed in the usual way as a quotient of a disjoint union set by an equivalence relation consisting of zigzags of related morphisms. For instance, this is the case in constructive HoTT (see chapter 10 of the book), and in the internal language of any elementary topos or even Pi-pretopos (with NNO for the zigzags). The map $\mathbb{N} \to \mathbb{N}\times\mathbb{N}$ in #16 is not even constructively well-defined: its definition appeals to LEM. I believe we've established previously, however, that Richard's understanding of the word "constructive" is rather different from that of most other mathematicians, in ways that are difficult to make precise or to explain. I'm not interested in reopening that discussion here. There are also other varieties of constructive mathematics in which epi-mono factorizations fail, for instance setoid/PER models with functions rather than anafunctions (e.g. <https://mathoverflow.net/questions/302037/mathematics-without-the-principle-of-unique-choice>), where instead you have (regular epi, mono) and (epi, regular mono) factorizations that do not coincide. But I view these as fairly exotic, and to repeat, in the constructive mathematics that is the internal language of toposes, all of these properties are true as long as they are true in the metatheory wherein the category in question is constructed.

    I have not read this thread in detail, and I probably won’t, but it is perfectly true in many kinds of constructive mathematics that epi-mono factorizations exist, in particular the category of sets is an elementary topos and hence a pretopos, and that colimits therein can be constructed in the usual way as a quotient of a disjoint union set by an equivalence relation consisting of zigzags of related morphisms. For instance, this is the case in constructive HoTT (see chapter 10 of the book), and in the internal language of any elementary topos or even Pi-pretopos (with NNO for the zigzags).

    The map $\mathbb{N} \to \mathbb{N}\times\mathbb{N}$ in #16 is not even constructively well-defined: its definition appeals to LEM.

    I believe we’ve established previously, however, that Richard’s understanding of the word “constructive” is rather different from that of most other mathematicians, in ways that are difficult to make precise or to explain. I’m not interested in reopening that discussion here. There are also other varieties of constructive mathematics in which epi-mono factorizations fail, for instance setoid/PER models with functions rather than anafunctions (e.g. https://mathoverflow.net/questions/302037/mathematics-without-the-principle-of-unique-choice), where instead you have (regular epi, mono) and (epi, regular mono) factorizations that do not coincide. But I view these as fairly exotic, and to repeat, in the constructive mathematics that is the internal language of toposes, all of these properties are true as long as they are true in the metatheory wherein the category in question is constructed.

18. • CommentRowNumber18.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 20th 2018
    • (edited Aug 20th 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexMy apologies for introducing any confusion, this was not my intention! > The map $\mathbb{N} \to \mathbb{N}\times\mathbb{N}$ in #16 is not even constructively well-defined: its definition appeals to LEM. Again, apologies for any confusion. I just wished to clarify that in what I had in mind, the definition does not appear to me to use LEM. The understanding of 'function' that I had in mind is: an algorithm which given an input, produces an output. So to define the function I mentioned, we need to have an algorithm for producing either $(p_{0}, p_{1})$ or $(0,0)$ given $n$. Unless one is worried about resources (ultrafinitism, etc), there is certainly such an algorithm for any conventional notion of natural numbers (just go through all possibilities, and return $(0,0)$ at the end if nothing is found) which does not appeal to LEM. Apologies for the sidetrack, the example was intended to be helpful. > in the constructive mathematics that is the internal language of toposes, all of these properties are true as long as they are true in the metatheory wherein the category in question is constructed. Yes, sorry, I see now how one would do this in those settings. It feels strange to me to call that constructive, but, as I say, it was not my intention to get into that kind of debate here.

    My apologies for introducing any confusion, this was not my intention!

    The map $\mathbb{N} \to \mathbb{N}\times\mathbb{N}$ in #16 is not even constructively well-defined: its definition appeals to LEM.

    Again, apologies for any confusion. I just wished to clarify that in what I had in mind, the definition does not appear to me to use LEM. The understanding of ’function’ that I had in mind is: an algorithm which given an input, produces an output. So to define the function I mentioned, we need to have an algorithm for producing either $(p_{0}, p_{1})$ or $(0,0)$ given $n$. Unless one is worried about resources (ultrafinitism, etc), there is certainly such an algorithm for any conventional notion of natural numbers (just go through all possibilities, and return $(0,0)$ at the end if nothing is found) which does not appeal to LEM.

    Apologies for the sidetrack, the example was intended to be helpful.

    in the constructive mathematics that is the internal language of toposes, all of these properties are true as long as they are true in the metatheory wherein the category in question is constructed.

    Yes, sorry, I see now how one would do this in those settings. It feels strange to me to call that constructive, but, as I say, it was not my intention to get into that kind of debate here.

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeAug 20th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOh, sorry, I must have misread your function, or else wasn't thinking clearly. Yes, of course, you only have to decide finitely many cases.

    Oh, sorry, I must have misread your function, or else wasn’t thinking clearly. Yes, of course, you only have to decide finitely many cases.

20. • CommentRowNumber20.
    • CommentAuthorKarol Szumiło
    • CommentTimeAug 21st 2018
    • PermaLink
    Author: Karol Szumiło
    Format: MarkdownItexOK, right now I regret bringing up constructive arguments since the discussion went in a completely different direction to what I intended. I'm really just interested in a topos-theoretic result that I suggested in #15 and I only need a classical proof of that. (In fact, I would be happy with just the case of $\mathcal{E}$ being a category of presheaves which would make it a statement entirely about sets.)

    OK, right now I regret bringing up constructive arguments since the discussion went in a completely different direction to what I intended. I’m really just interested in a topos-theoretic result that I suggested in #15 and I only need a classical proof of that. (In fact, I would be happy with just the case of $\mathcal{E}$ being a category of presheaves which would make it a statement entirely about sets.)

21. • CommentRowNumber21.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 21st 2018
    • (edited Aug 21st 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexRe #19: No problem. I took a quick look at the HoTT construction of the epi/mono factorisation. Is there any chance, maybe in a different thread, that you could hint at what it is in HoTT that allows one to carry out this construction, despite the weak Brouwerian counterexample? That it is possible in the internal language of a topos is less surprising to me, but HoTT is not so far from type theories where the Brouwerian counterexample would be able to made.

    Re #19: No problem. I took a quick look at the HoTT construction of the epi/mono factorisation. Is there any chance, maybe in a different thread, that you could hint at what it is in HoTT that allows one to carry out this construction, despite the weak Brouwerian counterexample? That it is possible in the internal language of a topos is less surprising to me, but HoTT is not so far from type theories where the Brouwerian counterexample would be able to made.

22. • CommentRowNumber22.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 21st 2018
    • (edited Aug 21st 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexRe #20: The first direction of your argument goes through immediately, I think, for presheaf categories, just arguing levelwise. The converse direction looks slightly trickier, because representable functors are not available anymore. Maybe one can use the internal hom $\underline{\mathsf{Hom}}(F(j), F(-))$ and so on instead. But then one can only something about the image of the span in $J$ under $F$. Perhaps that is what the condition should be in general: that every span in $J$ must be able to be completed to a commutative square in $\mathcal{E}$ after applying $F$?

    Re #20: The first direction of your argument goes through immediately, I think, for presheaf categories, just arguing levelwise. The converse direction looks slightly trickier, because representable functors are not available anymore. Maybe one can use the internal hom $\underline{\mathsf{Hom}}(F(j), F(-))$ and so on instead. But then one can only something about the image of the span in $J$ under $F$. Perhaps that is what the condition should be in general: that every span in $J$ must be able to be completed to a commutative square in $\mathcal{E}$ after applying $F$?

23. • CommentRowNumber23.
    • CommentAuthorKarol Szumiło
    • CommentTimeAug 21st 2018
    • PermaLink
    Author: Karol Szumiło
    Format: MarkdownItexThe first part looks fine, I agree. For the second part, following Mac Lane and Moerdijk I believe that the condition should say: for every cospan $i_0 \to j \leftarrow i_1$ the morphisms $F k \to F i_0 \times_{F j} F i_1$ are jointly epimorphic where $i_0 \leftarrow k \to i_1$ varies over all spans completing the original cospan. (Note that I changed spans to cospans since I switched from covariant diagrams over $J$ to presheaves.) The counterexample with representable functors is still technically available since we are looking at a functor $\Set^{J^op} \to \mathcal{E}$, but it just doesn't seem strong enough.

    The first part looks fine, I agree.

    For the second part, following Mac Lane and Moerdijk I believe that the condition should say: for every cospan $i_0 \to j \leftarrow i_1$ the morphisms $F k \to F i_0 \times_{F j} F i_1$ are jointly epimorphic where $i_0 \leftarrow k \to i_1$ varies over all spans completing the original cospan. (Note that I changed spans to cospans since I switched from covariant diagrams over $J$ to presheaves.) The counterexample with representable functors is still technically available since we are looking at a functor $\Set^{J^op} \to \mathcal{E}$, but it just doesn’t seem strong enough.

24. • CommentRowNumber24.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 21st 2018
    • (edited Aug 21st 2018)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexI have not thought properly about your condition in #23 yet, but I just looked a bit more closely into what I suggested in #22. As far as I can see, if one takes the condition to be that the image of every span in $J$ under $F$ can be completed to a commutative square in $\mathcal{E}$, and if, for the converse part of the proof, one uses the functor $\underline{\mathsf{Hom}}(F(j), F(-))$ and similarly for $i_{0}$ and $i_{1}$, then I think that direction of the proof goes through. But then the first direction of the proof seems problematic, because without knowing that we can complete the span in $J$, we cannot factor through $colim A$. Does your proposed condition not suffer from the same problem? What if there is no span completing the original co-span? [Edit: I suppose that is implicit in the fact that we have a joint epimorphism. Hmm. I will have to think a bit more about whether the converse direction of your proof goes through with that condiition.]

    I have not thought properly about your condition in #23 yet, but I just looked a bit more closely into what I suggested in #22. As far as I can see, if one takes the condition to be that the image of every span in $J$ under $F$ can be completed to a commutative square in $\mathcal{E}$, and if, for the converse part of the proof, one uses the functor $\underline{\mathsf{Hom}}(F(j), F(-))$ and similarly for $i_{0}$ and $i_{1}$, then I think that direction of the proof goes through. But then the first direction of the proof seems problematic, because without knowing that we can complete the span in $J$, we cannot factor through $colim A$.

    Does your proposed condition not suffer from the same problem? What if there is no span completing the original co-span? [Edit: I suppose that is implicit in the fact that we have a joint epimorphism. Hmm. I will have to think a bit more about whether the converse direction of your proof goes through with that condiition.]