Consider internal categories and in a finitely complete ambient category , and functors . Assume we have a natural transformation . To say that is a(n internal) natural isomorphism, in my 2012 paper in TAC I wrote > “We say a natural transformation is a natural isomorphism if it has an inverse with respect to vertical composition”, that is to say, there is some natural transformation such that the vertical composition and . For any internal category internal to a finitely complete category we can form the pullback (the sketchy formatting is deliberate here) Y^iso_1 ---> Y_1 x_{Y_0^2} Y_1 | | | | (m,m) | | v v Y_0 x Y_0 ---> Y_1 x Y_1 u^2 where the top right pullback is Y_1 x_{Y_0^2} Y_1 ---> Y_1 | | | | (s,t) | | v v Y_1 -----------> Y_0 x Y_0 (t,s) Since is a section (as is a section of both and ) it is a monomorphism, and so the projection is a monomorphism. Moreover: CLAIM: is a monomorphism. Suppose I have such that . Write and , so that we have . Since , we can do so that , and hence is a monomorphism. The argument here can be, with routine effort, written out using purely diagrammatic reasoning. Note that we have the swap involution which restricts to an involution , which is inversion. Now if we have a natural transformation with data , and it is a natural isomorphism as defined above, then by the existence of , we in fact get a map , by the universal property of the pullbacks involved in its definition. That is to say, a factors through the monomorphism . Conversely, suppose the natural transformation has data that factors through , then it has an inverse and so is a natural isomorphism. Note that is an internal groupoid and there is an identity-on-objects faithful functor , or in other words, a wide subcategory that is an internal groupoid. This construction was essentially contained in Bunge–Paré 1979 (page 376), though the details weren’t spelled out. The thing to note is that is a monomorphism, a pullback of a split monomorphism, but in different categories monomorphisms can be better or worse behaved. In particular, in , a monomorphism doesn’t always mean its domain has the subspace topology of the codomain. Thus inversion on might not be continuous with respect to the subspace topology, but it’s continuous with respect to the topology coming from the limit that defines it, hence the subspace topology from . This is familiar territory for people who work with topological algebras, for instance, so that the group of units of can be given the topology coming from . As a result, you have a natural transformation between internal functors , for and topological categories, which is pointwise invertible, but is not an _internal_ natural isomorphism, because it fails to have an inverse. As a particular example, if one takes an internal fully faithful functor , between topological categories and ask that it be _pointwise_ essentially surjective, which means that there is a map such that , … and is invertible for all , then this is not sufficient to construct and then say that there is a natural isomorphism between and the composite , following an internalised version of the construction in e.g. Mac Lane [Theorem IV.4.1]. Since we want internal essential surjectivity to behave well, and in particular an (internal eso)+ff functor should give an equivalence according to the expected construction, it should be clear that taking the naive “ factors through the subspace of invertible arrows” is not actually the correct definition. But what we can instead do is ask that (the arrow component of) a factors through the monomorphism instead, and so we recover the expected construction. One alternative that might be tempting is to ask that a “corrected” definition of internal category includes the condition that the inversion map on the subspace of invertible arrows is continuous. However, this rules out examples coming from functional analysis, for instance, where, as hinted, the subset of invertible endomorphisms (or invertible bounded maps) is not always given the subspace topology, but a finer topology so that inversion is rendered continuous. Another option that seems reasonable is to restrict attention to the largest subspace of on which inversion is continuous, and I myself have claimed this in a hurry, in a flawed attempt to explain what the above construction of gives. This also has issues, despite being an incorrect description, in that there is no reason to expect that it gives a functor , whereas _is_ a functor. I was prompted to write the above because I was asked about a point in my 2024 paper that concerned topological categories, where I had defined “essential -surjectivity” using described as “the subspace of invertible arrows”. The question came from Zeraoulia Rafik, who has been assembling a collection of documents detailing inaccuracies in a bunch of papers including Perelman, Guth-Wang-Zahl, Yitang Zhang, even Atiyah‘s flawed RH proof attempt (how flattering to be included among such luminaries!). If one replaced “subspace” with “subobject” in the paper and took the hint in my 2012 paper where I had myself earlier defined essential -surjectivity pointing back to Bunge–Paré (and Everaert–Kieboom–van der Linden’s 2004 paper), then one naturally arrives at the above approach. Further the explicit use of my 2012 main theorem in the proof of Corollary 5.1 means that the approach of _loc. cit_. is not just suggested, but necessary. So, while on the face of it, the counterexample painstakingly analysed in Rafik’s document seems to show that the results of my 2024 paper are flawed, what it _really_ serves to show is that the naive pointwise-invertible definition of natural isomorphism is not the correct definition. Despite me writing “subspace”, nothing relies on actually using the subspace topology on , and rather the treatment in Roberts 2012 is how one should approach the definitions, which doesn’t implicate using the subspace topology at all. ### Share this: * Share on X (Opens in new window) X * Share on Facebook (Opens in new window) Facebook * Like Loading... ### _Related_

The new Adelaide University is not on track to meet its international student targets and is staring down tens of millions in lost revenue, with the federal government's migration clampdown squeezing the business case for the newly merged institution.

Recall that an elementary topos is a cartesian closed category with finite limits and a subobject classifier. A Grothendieck topos is a category equivalent to the category of sheaves on a site. Are

The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of $\mathrm{ZF}$. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of $\mathrm{ZF}$, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some $V_ρ$ is already a model of $\mathrm{ZF}$; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way $\mathrm{ZF}$ has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.

Not long after OpenAI swept in to announce it had solved the famous Navier-Stokes math problem, angering the math community and spurring speculation that the AI lifted its findings from other mathematicians, the company is allegedly homing in on another Millennium Prize Problem. The Information reported Thursday, citing a single source at OpenAI, that employees at the AI firm expect to soon crack the Hodge Conjecture. That’s a famous unresolved question in math concerning whether certain topological features of geometric figures defined by polynomial equations can always be constructed by smaller geometric slices of the same figure. Scientific American noted it is “arguably the most abstract of the seven Millennium Prize puzzles,” of which just five remain to be solved. (Each puzzle carries a $1 million reward.) Critics have argued AI firms are appropriating the work of mathematicians to pump out quick solutions to unsolved problems without contributing to overall understanding of mathematics. They’ve also noted that AI firms don’t seem nearly as interested in less glamorous academic tasks like verifying their solutions—which can take third-party experts and the Clay Institute, the Millennium Prize’s sponsor, years—as they are a quick PR hit. Numerous mathematicians have signed onto open letters excoriating OpenAI, and it has withdrawn its sponsorship of next month’s AI-themed Caltech Mathathon. The Information noted that OpenAI engineers not only seem to see a business opportunity in doing for math what large language models did for coding, but also believe dominating math is an important pathway to recursive self-improvement (RSI). That’s the idea that a sufficiently smart computer will enter a phase of exponential, autonomous self-improvement. Depending on who one asks, RSI is a marketing buzzword, tech-bro philosophical babble, or the gateway to the apocalypse. OpenAI does at least seem aware, in the wake of the Navier-Stokes fiasco, that mathematicians now view it like a Dust Bowl farmer eyeing an approaching cloud of locusts. “It could take the company longer to announce the solution, though, because it’s trying to figure out how to collaborate with the math community to make the announcement without triggering another PR nightmare,” The Information paraphrased its source as saying.

For modular curves over schemes there are two main references that I use, namely Deligne Rapoport [DR], and Katz-Mazur [KM]. However I recently noticed that there is a difference in conventions in ...

To the best of my understanding, given two elliptic curves over the same base over $\operatorname{Spec}(\mathbb{Z})$, there is a scheme of degree-$d$ isogenies between them. This was claimed to me in