Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJun 27th 2018
    • (edited Jun 27th 2018)

    added pointer to a reference: Borceux 94, Vol 1, section 4.4

    diff, v12, current

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeAug 21st 2018

    In another thread, the question was raised of how constructive the epi-mono factorization is, e.g. whether its construction in Set can be done “internally” to produce it in any topos. The answer to that particular question, as recorded there, is yes.

    Richard also wrote:

    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 nn to (p 0,p 1(p_{0}, p_{1}), where p 0p_{0} is the smallest prime such that there is a prime p 1p_{1} with p 0+p 1=2np_{0} + p_{1} = 2n if such a p 0p_{0} exists, or else to (0,0)(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.

    I agreed (after making a stupid error) that this map is well-defined, but that doesn’t make it a Brouwerian counterexample. I don’t see any constructive problem with having the set of all prime numbers p 0p_0 such that blah blah. A subset of a set AA is just a way to associated a proposition to every element of AA, it doesn’t have to be decidable or anything of course. Even in setoid/PER models where epi-mono factorizations don’t exist, it’s still true that every map has an “image” – indeed, the problem is rather that it has two different images depending on what kind of “proposition” and hence what kind of “subset” you are looking at!

    • CommentRowNumber3.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 21st 2018
    • (edited Aug 21st 2018)

    Thanks for the reply! It would be nice to summarise the discussion of in what contexts the epi/mono factorisation can be made constructively on the nLab page.

    I don’t see any constructive problem with having the set of all prime numbers p 0p_0 such that blah blah.

    For me it is problematic, because I think that constructively to give a set should mean to give an algorithm which can be used to construct the set, and that is not possible for the image of the map i gave (because, for instance, we do not know whether or not (0,0)(0,0) belongs to the image). The difference from this point of view between the function and its image is that the latter is a totality; one has to consider all nn \in \mathbb{N}, and here exhausting all possibilities is not acceptable.

    But if this is not the mainstream interpretation, that is fine, and answers my question. Thanks very much!

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 21st 2018

    I was, coincidentally, just looking at the page image and the construction there of the regular image and the regular coimage. When I tried to view the page after making a small edit (with no comment), it gives me an error:

    XML Parsing Error: mismatched tag. Expected: </ul>. Location: https://ncatlab.org/nlab/show/image Line Number 614, Column 3:
    </div>
    --^
    
    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 21st 2018

    Re #3

    so I guess you only want to think about constructively decidable subsets (those whose characteristic function lands in the booleans), rather than arbitrary subsets (whose characteristic function maps to the object of all truth values)? And presumably ’decidable’ would means computable or something with a realiser, for you, since you want an algorithm. (possibly with bounded search space?) This feels like a kind of predicativism, but possibly not.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeAug 22nd 2018

    I think there’s a potentially interesting logic that is the internal logic of the fibration of complemented subobjects in a non-Boolean category (maybe a pretopos). This logic is “constructive” in some sense, but it still satisfies LEM, while it doesn’t have all existential quantifications and here not all images. I haven’t investigated it very much, but when I was a grad student I had an interesting conversation with Damir Dzhafarov which made me think that this logic ought to be at least related to the subsystems of set theory used in classical reverse mathematics.

    • CommentRowNumber7.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 22nd 2018
    • (edited Aug 22nd 2018)

    Re #4: Thanks very much, David, for pointing this out. There was another small bug in the table of contents renderer. I have fixed it now; hopefully it does not break any other pages!

    The logic is a bit subtle in the table of contents renderer. Actually, with so many bright sparks here, maybe I can post the code, and perhaps somebody would be kind enough to go through it? Here it is. I have extracted it from a larger file; I think one should just be able to use the code if you would like to do so, but if there is something missing, let me know, and I’ll add it. Also let me know if you are not familiar with Python and need to know something in order to understand the code.

    The bugs have been to do with closing the <ul> tags, which is handled towards the end, in the while loop, and just before and after it. The bug I just fixed was that there previously was

    table_of_contents_html += "</ul>\n" * depth
    

    rather than

    table_of_contents_html += "</ul>\n" * (depth + 1)
    

    towards the end.

    (The while loop by the way could just begin while True rather than while depth < max_depth but I am using the latter for additional safety, to avoid busy looping endlessly in case of a programming error which leads to not exiting the loop.)

    class EmptyHeaderException(Exception):
        pass
    
    class _NotAHeaderException(Exception):
        pass
    
    def _split_header(header_line):
        split_at_header_beginning = header_line.split("<h", 1)
        after_header_beginning = split_at_header_beginning[1]
        try:
            header_size = int(after_header_beginning[0])
        except ValueError:
            raise _NotAHeaderException()
        if header_size > 5 or header_size < 2:
            raise _NotAHeaderException()
        split_at_id = after_header_beginning.split("id='", 1)
        after_id = split_at_id[1]
        href = after_id.split("'", 1)[0]
        after_header_tag = after_header_beginning.split(">",1)[1]
        header = after_header_tag.split("</h")[0]
        return header_size, href, header
    
    def _table_of_contents(page_content, placeholder):
        page_lines = page_content.splitlines()
        current_header_size = 1
        header_sizes = []
        table_of_contents_html = "<div class='maruku_toc'>\n"
        after_table_of_contents = False
        for line in page_lines:
            if not after_table_of_contents:
                if placeholder in line:
                    after_table_of_contents = True
                else:
                    continue
            stripped_line = line.strip()
            if not "<h" in stripped_line:
                continue
            try:
                header_size, href, header = _split_header(stripped_line)
            except _NotAHeaderException:
                continue
            if not header:
                raise EmptyHeaderException()
            header_contents_html = (
                "<li>" +
                "<a href='#" +
                href +
                "'>" +
                header +
                "</a>" +
                "</li>" +
                "\n")
            if header_size == current_header_size:
                table_of_contents_html += header_contents_html
            elif header_size > current_header_size:
                table_of_contents_html += "<ul>\n"
                table_of_contents_html += header_contents_html
                header_sizes.append(header_size)
                current_header_size = header_size
            else:
                header_sizes.pop()
                max_depth = len(header_sizes)
                depth = 1
                if depth == max_depth:
                    table_of_contents_html += "</ul>\n" * depth
                    table_of_contents_html += header_contents_html
                    current_header_size = 2
                    continue
                while depth < max_depth:
                    previous_header_size = header_sizes.pop()
                    if previous_header_size <= header_size:
                        table_of_contents_html += "</ul>\n" * depth
                        table_of_contents_html += header_contents_html
                        if previous_header_size != header_size:
                            header_sizes.extend([previous_header_size, header_size])
                        else:
                            header_sizes.append(header_size)
                        current_header_size = header_size
                        break
                    if depth + 1 == max_depth:
                        table_of_contents_html += "</ul>\n" * (depth + 1)
                        table_of_contents_html += header_contents_html
                        current_header_size = 2
                        break
                    depth += 1
        table_of_contents_html += "</ul>\n" * len(header_sizes)
        table_of_contents_html += "</div>\n"
        return table_of_contents_html
    
  1. I’ll reply to #5 and #6 later, thanks for the interest!

  2. Re #5:

    so I guess you only want to think about constructively decidable subsets (those whose characteristic function lands in the booleans), rather than arbitrary subsets (whose characteristic function maps to the object of all truth values)? And presumably ’decidable’ would means computable or something with a realiser, for you, since you want an algorithm. (possibly with bounded search space?)

    In general, I am just guided by attempting to have a valid semantics for the kind of constructivism I have in mind, which is at its heart very simple: that one should be able to actually construct the things one wishes to treat. I realise that I may be going one step further than in Martin-Löf’s type theory, because I do not think that he considers it necessary to, from the beginning, take the notion of type to be constructively meaningful.

    I am reluctant to agree too strongly, because it might lead to confusion if some aspect of it disagrees with the more philosophical point of view I just described, which is the primary thing for me. However, with that caveat, what you wrote does seem accurate yes, if decidable is, as you say, given constructive meaning. Whilst I am sympathetic to ultrafinitism, I am typically fine with allowing algorithms that are able to be carried out in principle, so an infinite amount of steps is not permitted, but a finite number would be allowed.

    This feels like a kind of predicativism, but possibly not.

    Yes, interestingly, exactly the same thought occurred to me. I agree that it does share something with predicativism.

    Re #6: this sounds interesting! Presumably a bit different from my way of thinking, but interesting nonetheless.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeAug 26th 2018

    Richard, it might be helpful if you come up with a name for your kind of constructivism. That way, when you object that what someone else is doing doesn’t seem “constructive” to you, you can say “This doesn’t seem Williamson-constructive” or something, and then at least they won’t be confused or spend time explaining to you why it is perfectly “constructive” the way most other mathematicians use the word.

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 27th 2018

    Ditto

  3. Sincere apologies for any wasted time! As mentioned in the thread where this discussion came from, my intentions were genuine, and were not to lead things into a discussion of my views on constructivism. Those views are not systematically worked out or sophisticated anyhow, they are just my attempt to work out what constructivism as I see it philosophically means in practise. But out of the discussion came the realisation I mentioned in #9, that my point of view actually differs, it seems, from Martin-Löf’s when it comes to the meaning of what a ’type’ is; this, I think, should stick in my mind, and help me remember that the way I think about constructivism differs from the norm!