Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: our work

Topic: David Roberts

David Michael Roberts (Apr 13 2021 at 02:12):

Well, in the spirit of sharing WIP, I am finalising a short note that puts strong constraints on the classification of finite-dimensional bundle gerbes on manifolds. If you are stack-minded, this is saying something about how one can give finite-dimensional Lie groupoid presentations of differentiable stacks over a manifold, of a certain sort.

A nice corollary is that no smooth 2-group extension of a compact simple connected Lie group (not necessarily simply-connected) can be topologically nontrivial and given by a finite-dimensional crossed module of Lie groups at the same time.

It also implies that on a manifold $M$ with finite $\pi_1$, every classical twist of K-theory of $M$ arising from a principal $G$-bundle and a central extension of $G$ by $U(1)$ is torsion, where $G$ is any finite-dimensional Lie group (this is well-known to be true for $G=PU(n)$).

More geometry/topology, but there some category theory hiding in there.

David Michael Roberts (Apr 13 2021 at 04:08):

When that's done I have to get back to writing up the construction of strict models for the universal basic gerbe and universal 2-gerbe using all kinds of crossed machinery and simplicial diffeological groups (joint with Raymond Vozzo). This is so we can present concrete formulas for a differential string structure on certain homogeneous spaces.

When that's done, I might be able to look at a note I'm writing with John Rice about the construction of the long exact sequence in cohomology in an elementary way using fractions for the connecting homomorphism, rather than the snake lemma, and some ideas about how to present spectral sequences is a pedagogical way in a similar vein.

And there's my paper with Martti that started here on Zulip, waiting to be refactored for an expert audience, rather than a generic mathematician (I felt that was a bit too hard, and likely to fail at a generalist journal, in the end).

And a project with Rohit Holkar on functoriality of groupoid C^*-algebras, building off a paper on my own about localising 2-categories of internal groupoids using certain cospans.

Plus a bunch of other stalled projects (class forcing, presentable stacks of categories and their appearance in algebraic geometry/number theory,...)

John Baez (Apr 13 2021 at 05:46):

Exciting stuff!

David Michael Roberts (Apr 16 2021 at 10:01):

Ok, so the paper is submitted to the arxiv. The result also implies that for connections on String_G 2-bundles, if one uses crossed modules of Lie algebras as coefficients then they have to be infinite-dimensional. The alternative is finite dimensional but non-strict 2-truncated L_oo-algebras.

John Baez (Apr 16 2021 at 14:35):

On Twitter you made a comment about how quickly you were able to write this paper. I think that when you've thought about something a long time, you tend to build up a reserve of interconnected ideas that you can write up pretty quickly, yet are not obvious to someone who hasn't put in the time. So this is a great way to write papers.

Mike Shulman (Apr 16 2021 at 15:07):

I've noticed that too.

Matteo Capucci (he/him) (Apr 17 2021 at 06:10):

I've noticed that too, because I still didn't get to write down a paper :joy:

David Michael Roberts (Apr 19 2021 at 05:56):

For what it's worth: https://arxiv.org/abs/2104.07936

David Michael Roberts (May 13 2021 at 13:43):

The torsion gerbe paper is now massively upgraded, because I learned how to do some spectral sequence stuff, and also work over the integers rather than rationally. Now, in hindsight, the earlier versions of the paper were rather trivial versions of the main theorem.

David Michael Roberts (May 13 2021 at 13:48):

The applications are practically untouched, but I can get a much sharper statement in a large class of examples.

There's now a bunch of low-degree group homology hypotheses that ensure that all lifting gerbes are torsion, but one main takeaway is that if I'm playing on a space X with pi_1(X) locally finite, or with a Lie group G with pi_0(G) locally finite, there's a single hypothesis, namely that Ext^1 of its Schur multiplier is a torsion group. This then implies all possible lifting gerbes either on that space, or involving that group, respectively, will be torsion.

I give an explicit example of a countable, abelian locally finite group K (hence purely torsion) with Ext(H_2(K),Z) not purely torsion, and then give a (1-dimensional!) Lie group G with pi_0(G)=K, so that there are many non-torsion lifting gerbes built using that group.

John Baez (May 13 2021 at 17:24):

What's an example of something you knew using Q before but Z now? Please keep it simple... I'm just wondering which sort of pairs of facts are comparable.

David Michael Roberts (May 14 2021 at 07:53):

I can't quite parse your question. Do you mean didn't know using Q before and Z now?

When cohomology is finitely generated, tensoring with Q and taking rational coefficients gives you the same information. But for infinitely-generated stuff, it gets weird. I'm getting cohomology (over the integers) containing a subgroup that is the product of all prime cyclic groups, hence has lots of non-torsion elements. working over Q you don't see this subgroup!

I wanted to know something like when a certain cohomology group was purely torsion, and also wanted to construct a nontrivial example when it wasn't torsion, but was right on the cusp. So my group K for instance is the direct sum of all the squares of the prime cyclic groups. And the third cohomology group of this turns out to be the product of all the prime cyclic groups (and this injects into the group I really cared about).

John Baez (May 15 2021 at 17:30):

I think you parsed my question just fine, answering what I meant to ask instead of what I actually wrote.

John Baez (May 15 2021 at 17:32):

I'm interested in the most basic aspect of this. Is this what you're saying: if $X$ is a space such that $H^\ast(X,\mathbb{Z})$ is finitely generated then we have

$H^\ast(X,\mathbb{Q}) \cong H^\ast(X,\mathbb{Z}) \otimes_{\mathbb{Z}} \mathbb{Q}$

but not necessarily if $H^\ast(X,\mathbb{Z})$ is infinitely generated?

Tim Hosgood (May 15 2021 at 20:26):

isn’t this always true by the universal coefficient theorem? (since $\mathbb{Q}$ is flat)

Tim Hosgood (May 15 2021 at 20:30):

oh, your question is about cohomology not homology, woops

David Michael Roberts (May 15 2021 at 23:43):

Something like that. If that's not quite right, then I can say more precisely what goes wrong: at some point there's homology of some K(G,Z) where G an infinite filtered colimit of finite groups (which would be trivial over Q). But then I have to take Ext of that to use the universal coefficient theorem, which turns coproducts into products, and the product of infinitely many finite groups is not torsion, even when the sum is. So tensoring with Q at the end finds the non-torsion, but taking Q coefficients gives you zero from the start.

David Michael Roberts (Aug 08 2021 at 03:39):

FWIW, the torsion gerbe paper has been accepted at the Bulletin of the Australian Math. Soc.

I'm trying to get my little diagonal argument/fixed point theorem paper finished next. It started as a little two-page note making a tiny observation, and now I have a suite of variations on the theme of getting the two theorems in weaker assumptions, though the diagonal argument makes fewer appearances.

And I'm writing an essay about the Liquid Tensor Experiment, got to get that to the magazine on Thursday.

David Michael Roberts (Aug 08 2021 at 03:39):

The gerbe/2-gerbe work has got connections all over it, and thanks for picking up an error in an older paper, I can now proceed with more confidence, now that I have the correct definition. That will be a trilogy of papers now:

• rigid 2-gerbes with connections, and why the Chern–Simons 2-gerbe and its geometry has been secretly rigid the whole time;
• the universal 2-gerbe, which we show is a Chern–Simons type diffeological 2-gerbe, and hence is rigid. We also give an explicit classifying span for the so-called _basic gerbe_ on a compact simple simply-connected Lie group in the category of diffeological gerbes
• differential string structures on homogeneous spaces, using the machinery from part 1.

David Michael Roberts (Aug 13 2021 at 06:16):

• LTE essay is sent off, hopefully comments by Monday for next review cycle.
• Now trying to finish the diagonal arg/lawvere FPT paper: the last theorem to put in is a fixed point theorem in a setting with a flat comonad on a magmoidal closed category with diagonals, so that one can get the assignment $\flat(C^C)\to C$, sending an endomorphism "discontinuously" to a fixed point. Of course, one can take $\flat$ to be the identity comonad, in which case this is a map $C^C \to C$.

David Michael Roberts (Aug 13 2021 at 06:26):

This result is reminiscent of the work of @Mike Shulman on Brouwer's FPT in real cohesive HoTT, but I haven't tried to link to that.

Johan Commelin (Aug 13 2021 at 10:07):

@David Michael Roberts Is there a preview version of the LTE essay available?

David Michael Roberts (Aug 13 2021 at 10:15):

@Johan Commelin no, but I'm happy to share it privately. I'd appreciate comments, it's still got scope for improvements.

David Michael Roberts (Aug 13 2021 at 23:41):

First impressions back from the editors on the LTE essay — it is now going to be split into two parts.
(Thanks also to Johan for the careful reading, which picked up a silly error)

David Michael Roberts (Aug 18 2021 at 06:40):

I now have a first complete version of the diagonal argument/fixed point theorem paper: it is available from here: https://thehighergeometer.wordpress.com/2021/08/18/substructural-fixed-point-theorems-and-the-diagonal-argument-theme-and-variations/

David Michael Roberts (Aug 18 2021 at 06:42):

Somewhat amusingly, I don't even need $\flat$ to be a comonad for two out of the three variations, merely a copointed endofunctor.

Valeria de Paiva (Aug 18 2021 at 20:16):

David Michael Roberts said:

Somewhat amusingly, I don't even need $\flat$ to be a comonad for two out of the three variations, merely a copointed endofunctor.

very interesting @David Michael Roberts. I have done some work on a 'linear' version of NNOs (Natural Number Objects in Dialectica Categories with Charles Morgan and Samuel g da Silva, Electronic Notes in Theoretical Computer Science Volume 305, 11 July 2014, Pages 53-65) because I thought I needed a NNO to think about fixed points. maybe one can simply bypass them, as you seem to do in your note.

David Michael Roberts (Aug 18 2021 at 23:14):

Thanks, @Valeria de Paiva ! Perhaps the best new idea from the paper is the very last bit, this has been swirling around in my head for so long — I just had to get it on paper and out — that I'm too close to the material to make a sensible judgement.

David Michael Roberts (Sep 08 2021 at 00:05):

David Michael Roberts said:

• rigid 2-gerbes with connections, and why the Chern–Simons 2-gerbe and its geometry has been secretly rigid the whole time;

We now have this geometry pinned down. From a descent point of view, where we have a bundle gerbe with connection and curving as "transition function" (really a map $$Q\times_M Q \to \mathbf{BdlGrb_{\text{conn}}$$ where the codomain is a 2-stack), then the "cocycle equation" is not literally an equation (as it's a priori an equivalence in a 2-category), but it is the most "equation-like" it can possibly be, and the coherence condition for it is again as strict as possible.

David Michael Roberts (Sep 08 2021 at 00:18):

I am also going to be working on rewriting the intro to the diagonal argument/FPT paper, since it was clearly written for (and by a) category theorists, and I've been strongly suggested to make it more accessible to computer sciency types

David Michael Roberts (Oct 01 2021 at 07:26):

• The Lawvere fixed-point theorem/diagonal argument paper is submitted to the arXiv! (edit: here: https://arxiv.org/abs/2110.00239)
• Corrections to BCSS are sent to @John Baez to peruse
• Project on abstract construction of crossed modules of Lie groups and their categorical representations will kick off in earnest next week with Pedram Hekmati
• Project on constructing explicit String connections on homogeneous spaces: paper I is being written up in earnest, paper II and III have sketchy drafts, and Raymond Vozzo and I were thinking yesterday about the end-game of getting Lie-2-algebra-valued forms on the Lie groupoid total space of a String bundle.

David Michael Roberts (Feb 14 2022 at 21:17):

Yay, my paper on the Lawvere fixed-point theorem/diagonal argument has been accepted to Compositionally! (modulo some edits).

Paper I in the previous comment is almost finished, we late discovered we had to check coherence for a bundle 2-gerbe multiplication constructed out of other data, rather than it being automatic. (Home teaching and uni teaching is slowing this process down, we'd planned to be done by now! )

David Michael Roberts (Mar 10 2022 at 10:27):

I posted on the arXiv today notes from a talk in 2014, Explicit string bundles, so they have a stable home, because they've been cited.

David Michael Roberts (Apr 05 2022 at 06:13):

1. After getting an email from a PhD student who stumbled on a theorem I claimed in an obscure corner of the nLab, and who wanted the actual details, I thought it might be time to dig out the (finished - epsilon) paper I was writing during my PhD and make it public. The title is Homotopy equivalence of topological categories, and gives a version of Quillen's Theorem A for categories internal to CGH.

This can be applied to show that a topological stack presented by a "well-pointed" category in CGH, on the site (CGH,numerable open covers), has a well-defined homotopy type, and in fact this a 2-functor from the (2,2)-category of such topological stacks to the (2,1)-cat that is CGH with homotopy classes of homotopies as 2-arrows.

2. I found some more sign errors in a precursor paper to the asymptotically approaching "Paper I", and I had to work with one of the authors through that. This potentially had some impact, but it turns out to not really be an issue, we treat the paper as a black box. But another paper that just came out was re-explaining material, and that's why I started looking: things were a bit screwy when written out in full!

3. But then someone else told me some stuff he was sorting out for a nearly-finished paper that means the Chern–Simons bundle 2-gerbe associated to a principal G-bundle (suitable G) has as its characteristic class the negative of $\tfrac{1}{2}p_1$ (!). As far as obstruction theory goes, it makes no difference, and for physics, extremising the Chern–Simons action doesn't care if the sign in front is + or -, and it turns out people have been casual with the related web of facts going back to possibly the 80s, or else not seen the need to spell things out really clearly. This will only have minimal impact on "Paper I", and not on the calculations, thankfully.

David Michael Roberts (Apr 06 2022 at 08:38):

The lesson of writing in a way to be kind to your future self really struck home today. Things I claimed without proof in 2008 were not obvious to me now, and after worrying that certain claims weren't true, they turned out to be ok. I'm not going to expend a lot of effort on figuring out every single claim and loose end, though. Cutting the knots at some point, and cleaning up the exposition is where I will draw the line.

John Baez (Apr 06 2022 at 19:20):

Hmm, I'd feel funny releasing a paper I don't fully understand at the time of releasing it.

John Baez (Apr 06 2022 at 19:21):

But perhaps I'm being silly because there are plenty of papers I've written that I no longer fully understand now.

John Baez (Apr 06 2022 at 19:22):

I guess it depends on how much you trust your past self to have correctly understood what you were doing.

David Michael Roberts (Apr 07 2022 at 02:42):

@John Baez Oh, I'm not releasing stuff I don't understand. I was cutting the sections where I was floundering and not really proving stuff, and where I could reconstruct the argument, I filled it in!

David Michael Roberts (Apr 07 2022 at 02:42):

So here's the paper: Homotopy equivalence of topological categories

John Baez (Apr 07 2022 at 03:59):

Oh, good! I misinterpreted what you said.

David Michael Roberts (Jun 20 2022 at 07:14):

Since Rist–Saemann–Wolf have released the second version of their paper, re-doing all the needed calculations (based on extended discussions between the four of us(, I have sent @John Baez updated corrections for BCSS.

So the way is definitely clear for my paper with Raymond Vozzo to arrive, belatedly. The was another issue in the literature that delayed us again, I'm writing up the last outstanding proof now. Intro needs writing, too, though.

John Baez (Jun 20 2022 at 18:15):

Thanks, @David Michael Roberts. I haven't read today's email yet. I will do this soon!

David Michael Roberts (Sep 07 2022 at 14:48):

Well, it's nearly landed. This semester I'm teaching at two unis and a school, so just as we were about to finalise, progress ground to a halt.

But, it is close to release now, here's a pre-arXiv version. It's 62+5 pages long, because there's explicit nontrivial differential form calculations that we don't want to avoid. But comments on the intro are particularly welcome.

• David Michael Roberts and Raymond Vozzo, Rigid models of 2-gerbes I: Chern–Simons geometry, prerelease version https://www.dropbox.com/s/uwfmotydjv1hjed/paperI.pdf?dl=0

Motivated by the problem of constructing explicit geometric string structures, we give a rigid model for bundle 2-gerbes, and define connective structures thereon. This model is designed to make explicit calculations easier,for instance in physics applications. To compare to the existing definition, we give a functorial construction of a bundle 2-gerbe as in the literature from our rigid model, including with connections. As an example we prove that the Chern–Simons bundle 2-gerbe from the literature, with its connective structure,can be rigidified—it arises, up to isomorphism in the strongest possible sense,from a rigid bundle 2-gerbe with connective structure via this construction.Further, our rigid version of 2-gerbe trivialisation (with connections) gives rise to trivialisations (with connections) of bundle 2-gerbes in the usual sense, and as such can be used to describe geometric string structures

paperI.pdf

David Michael Roberts (Sep 07 2022 at 14:53):

There's a big appendix that proves that our structure gives rise to a bundle 2-gerbe in the usual sense, and this is hopefully the black box that contains all the difficulty that bundle 2-gerbes usually bring to the table. The model we give is much cleaner, and, ultimately, enough to directly capture the major examples up to iso, but in fact all examples (to be proved in part II) up to usual notion of weaker equivalence.

David Michael Roberts (Sep 07 2022 at 15:09):

That is, we can build a diffeological rigid bundle 2-gerbe over a diffeological model for K(Z,4), representing a generator of the relevant cohomology class. And so every bundle 2-gerbe is stably isomorphic to one that is a) a pullback of the universal one and b) this has a rigidification in the sense of the paper. One thing which I'm pretty certain is true is that given a smooth manifold X, we should be able to find a rigid bundle 2-gerbe built out of manifolds on X that is stably-isomorphic to any pullback of the universal rigid bundle 2-gerbe (which is diffeological) along X -> K(Z,4). This is a paper II problem, however.

David Michael Roberts (Sep 07 2022 at 15:11):

Paper III will have a large class of examples of geometric string structures, and in fact we plan to write this one next. There's also another application paper after that, but this is very much projecting down the line somewhat.

David Michael Roberts (Sep 07 2022 at 15:12):

I have started attacking revisions to my diagonal argument paper, I realised I probably don't have to do significant rewrites. Then I can get that back to Compositionality as quick as I can.

David Michael Roberts (Sep 09 2022 at 14:33):

My diagonal argument paper is now edited and sent back to Compositionality! :tada:

David Michael Roberts (Sep 09 2022 at 14:35):

Once this is finally published, and the geometry paper is submitted to a journal, then I have a choice as to what project to pick up! I have three other (disjoint) collaborators who haven't needed urgent progress, and have been very patient...

David Michael Roberts (Sep 14 2022 at 00:24):

Well, it's out

David Michael Roberts, Raymond F. Vozzo, Rigid models for 2-gerbes I: Chern-Simons geometry, https://arxiv.org/abs/2209.05521

Next task: move house.

David Michael Roberts (Sep 25 2022 at 23:36):

House mostly moved :-)

David Michael Roberts (Sep 25 2022 at 23:37):

For better or worse, I was convinced I should run in the MathOverflow moderator election. I hope that, if elected, I can do the role justice.

David Michael Roberts (Oct 05 2022 at 11:21):

:large_blue_diamond:

David Michael Roberts (Jul 21 2023 at 09:12):

Currently actively working on two research projects:

1. The history and prehistory of the phrase "canonical map/isomorphism" pre-1960. From Grothendieck back to Bourbaki in a connected tradition, and then proposing a reconstruction of the rationale for adopting it, and reflections on how the word used to be used before then.

2. (with Raymond Vozzo) Building a universal rigid bundle 2-gerbe in diffeological spaces that is equipped with a universal twisted "string" structure (except substituting the usual 2-group $\mathrm{String}_G$ with the universal strictly multiplicative bundle gerbe, again in diffeological spaces, and we are building this, too). The trick is to make it so that the functor to compactly-generated topological spaces maps this to the correct thing, and not just using subductions, which are a too weak.

David Michael Roberts (Aug 03 2023 at 01:07):

For those that want to see the slow-burn thread where I work backwards in time tracking the use of "canonical", you can consult it here: https://mathstodon.xyz/@highergeometer/110665668385051041

David Michael Roberts (Aug 03 2023 at 01:11):

I've worked back from the 1960 EGA1 by Grothendieck and Dieudonné, all the way to the draft Dieudonné wrote for Bourbaki in 1938, for the Fascicule de Résultats for the much later released Théorie des Ensembles. But I have a bit over a year to go back towards the original introduction (spoiler: I think it is in part due to Ehresmann, but there's a small amount of theorising I'm doing to join the dots in making that claim)

David Michael Roberts (Aug 09 2023 at 12:44):

Hurray! My fixed-point/diagonal argument paper that was accepted to Compositionality has been finalised! It will appear in the next arXiv update, with some typo fixes, but also a corrected theorem statement whose proof was fine, but a systematic update of letters for objects in the previous version hadn't gone through properly in that one spot.

David Michael Roberts (Aug 09 2023 at 12:47):

Due to scheduling, it is to be issue 8 of the current volume, and issues 6 and 7 are still in the pipeline, so it probably won't appear on the website for a little bit (my guess is that things like doi assignment can make this a rigid process - the journal has the vol/issue numbers embedded in the doi).

John Baez (Aug 09 2023 at 13:06):

Congratulations! I hope your paper is fixed at this point.

Yes, I think Compositionality was suffering in part from the fact that some slow-to-fix papers had already been assigned DOI numbers!

David Michael Roberts (Aug 10 2023 at 00:41):

your paper is fixed at this point

Very droll :-) Yes, it was obvious, the proof was a single diagram commuting diagram, the statement could be reconstructed from that very easily.

Final version has landed with all the journal metadata and reference/doi https://arxiv.org/abs/2110.00239

Edit: and now published

David Michael Roberts (Aug 10 2023 at 06:33):

On a different topic, and it's been on my todo list for over a month, I wrote up on MathOverflow a proof of the following fact

• Given a site $(S,J)$ and an internal category $C$ in $S$ such that the representable presheaf on $S$ associated to the object of arrows $C_1$ is a $J$-sheaf, the representable presheaf $よ(C)$ of categories is a prestack.

(Here a prestack is the analogue of a separated presheaf, not a general presheaf. I just realised a recently-published paper seems to use "prestack" for "presheaf of categories", which wasn't what I thought it was doing)

This feels unsurprising if you think about the definition of prestack as meaning "the local hom-presheaves are sheaves", but I didn't use this definition.

John Baez (Aug 10 2023 at 09:27):

There's a process - I forget it's name - such that if you do it once to a presheaf of sets you get a separated presheaf, and if you do it twice you get a sheaf. Similarly there's a process such that if you do it once to a presheaf of categories you get a ???, and if you do it twice you get a ????, and if you do it thrice you get a stack. And this pattern continues to higher $n$-categories.

John Baez (Aug 10 2023 at 09:29):

I don't know the terms that fill in ??? and ????. But one of them should probably be 'separated prestack'.

Morgan Rogers (he/him) (Aug 10 2023 at 09:36):

The former is Grothendieck's plus construction (not to be confused with either of the other things called [[plus construction]]).

John Baez (Aug 10 2023 at 09:36):

That sounds familiar now! Thanks!

David Michael Roberts (Aug 10 2023 at 11:18):

Yes, that was what the question was about: why does just one application of Grothendieck's +-construction seem to work, when a priori you only have a presheaf of groupoids coming from mapping into a Lie groupoid. BTW your ????, the step before a stack, is called a prestack, in what is probably a poor choice of terminology.

Mike Shulman (Aug 10 2023 at 14:44):

Fortunately once we get past $n=2$ I think people just put a numerical index on "separated".

Mike Shulman (Aug 10 2023 at 14:45):

Intriguingly, however, the pattern doesn't continue to $n=\infty$ in the obvious way. There's still a plus-construction, but it doesn't in general suffice to apply it $\omega$ times; you may have to continue into higher ordinals.

Martti Karvonen (Aug 10 2023 at 16:22):

That's curious. When you say higher ordinals, do they still remain countable or can they get larger than that? Or more generally, is there an upper bound?

Mike Shulman (Aug 10 2023 at 16:39):

The size of the ordinals is determined by the size of the site, so for arbitrary sites the ordinals can be arbitrarily large, certainly not countable in general. Arguably this is what we should expect in the first place, since sheafification is essentially constructing a least fixed point of an endofunctor and the [[transfinite construction of free algebras]] in general requires large ordinals. It's sort of an accident that for sheafifying $n$-presheaves for $n<\infty$ you can get away with only $n+2$ iterations.

Mike Shulman (Aug 10 2023 at 16:42):

Mathieu Anel and Chaitanya Leena Subramaniam recently wrote a nice paper comparing the plus-construction to the small object argument, including the $\infty$-categorical case.

David Michael Roberts (Sep 17 2023 at 04:58):

I'm working on showing Section 2.2 and Proposition 1 of my paper https://arxiv.org/abs/hep-th/0509037 are actually wrong. The fix, if there is one, is not a simple matter of flipping a whole bunch of signs. There's a "group action" of a group on an affine space that suspect is really a non-strict group action on some kind of internal groupoid, and the "action" in the paper is merely the object component of that. At least, that's my guess, which I'll have to consider after I've calculated this explicit counterexample.

David Michael Roberts (Sep 17 2023 at 07:28):

Although, it might a strict 2-group acting weakly on a groupoid..

John Baez (Sep 17 2023 at 10:05):

Good luck! Though I'm glad it's your paper this time. :upside_down:

David Michael Roberts (Sep 17 2023 at 11:44):

To be honest, I was a little unsatisfied at the time at the form of the results: why should the result depend on the particular choice of surjective submersion $Y\to M$? If one got an equivalence-invariant result about higher gauge theory on abelian 2-bundles, then it shouldn't change so wildly depending on the actual object manifold of the Lie groupoid underlying the 2-bundle. But I didn't know what I know now, I was just vaguely perturbed and hoping to get a somehow "better" result. Although, to be fair, almost nobody at the time had enough experience with 2-bundles and higher gauge theory in 2005 to intuit what the "correct" result would look like on general principles.

It might be that my intuition was just strong enough at the time to feel like something what suboptimal. If a fix to this paper actually addresses the niggling bother I had at the time, then at least something good has come out of this process.

David Michael Roberts (Sep 19 2023 at 04:42):

OK, I believe I have constructed an explicit counterexample to the proof of Proposition 1. To be fair, if one is being super careful, one might still wonder if Proposition 1 is true by some other means, or if Section 2.2 is still potentially sound, with a different choice of data. I suspect not, but that's a more subtle task than what I've done so far.

David Michael Roberts (Sep 21 2023 at 08:25):

Even better. I was able to strengthen the disproof using results about Banach Lie algebras and their cohomology, to give a general non-existence result under conditions that hold for $U(\mathcal{H})$, in a way that generalises (albeit just in dimension 2 for now) a result about compact Lie groups and the fact their de Rham cohomology as a graded ring is isomorphic to the bi-invariant differential forms.

David Michael Roberts (Sep 21 2023 at 08:27):

I expect that Banach Lie groups/algebras here are not optimal, and I hope to strengthen this to more general settings. It gives a nice obstruction to precisely how one can construct central extensions of Lie groups à la Murray and Stevenson (i.e. some of the data really can't be transformed away and must play an essential role)

David Michael Roberts (Sep 27 2023 at 07:01):

Here's a preliminary version of the write-up, titled On the non-existence of primitive 2-forms on Lie groups. I had to squeeze a little blood out of the stone to have something to show for the erroneous old paper

https://www.dropbox.com/scl/fi/mf6349ui6klb28mxw1wst/primitive_2-forms.pdf?rlkey=31hyj8lvro45typw7vm0pqzju&dl=0

Getting a working replacement for the paper is another matter. I have preliminary ideas, but nothing conclusive yet.

John Baez (Sep 27 2023 at 12:02):

We talked a bit more about this on Mathstodon. (David knows, but others may not, and unfortunately you have to keep running around the web to follow all the math conversations!)

David Michael Roberts (Oct 28 2023 at 04:06):

Here's the updated version of the above note, expanding the focus to bi-invariant 2-forms more generally

https://www.dropbox.com/scl/fi/wrg201mm1ttlvekwksps4/bi-invariant-2-forms.pdf?rlkey=flvyfk4bulozgx9x8abfovh4q&dl=0

David Michael Roberts (Oct 28 2023 at 04:07):

I plan to arXiv this as soon as I can, in the absence of any obvious complaints.

John Baez (Oct 28 2023 at 10:04):

Looks nice! A minor point:

So as a first approximation one can try to understand the existence of bi-invariant 2-forms on a Lie group, before trying to examine its subspace of primitive 2-forms. The space... of bi-invariant 2-forms on G, as a subspace of $\Omega^2(G)$, is very much smaller.

John Baez (Oct 28 2023 at 10:08):

Since you were just describing the space of bi-invariant forms as a "first approximation" to the space of primitive forms, when you say the space of bi-invariant forms is "much smaller" I momentarily think "no, it's larger than the space of primitive forms". Then I realize what you mean.

John Baez (Oct 28 2023 at 10:09):

This momentary misstep could be avoided if your last sentence was something like

The space... of bi-invariant 2-forms on G is very much smaller than $\Omega^2(G)$.

John Baez (Oct 28 2023 at 10:09):

I.e. ultra-clearly answer the question "very much smaller than what?"

Jorge Soto-Andrade (Oct 28 2023 at 13:55):

David Michael Roberts said:

Yay, my paper on the Lawvere fixed-point theorem/diagonal argument has been accepted to Compositionally! (modulo some edits).

Jorge Soto-Andrade (Oct 28 2023 at 13:59):

David Michael Roberts said:

Yay, my paper on the Lawvere fixed-point theorem/diagonal argument has been accepted to Compositionally! (modulo some edits).

Congrats for your paper!   By the way, you might want to have a look at this old Acta App. Mathematicae paper on the same subject (triggered by a question of the well-known biologist Francisco Varela...).
https://www.researchgate.net/publication/225997258_Self-reference_and_fixed_points_A_discussion_and_an_extension_of_Lawvere's_Theorem

David Michael Roberts (Oct 28 2023 at 21:42):

@Jorge Soto-Andrade can you re-paste that link in plain text (i.e. not in a code block?) It's hard for me to get it in a usable form on mobile

David Michael Roberts (Oct 28 2023 at 21:44):

@John Baez thanks, good suggestion.

I need to clean up the very last paragraph a little, too.

Jorge Soto-Andrade (Oct 28 2023 at 23:23):

Sorry, here it is :

Jorge Soto-Andrade (Oct 28 2023 at 23:27):

hope it works now

Nathaniel Virgo (Oct 29 2023 at 00:38):

That didn't seem to work either, but this should do it:

Jorge Soto-Andrade said:

Congrats for your paper! By the way, you might want to have a look at this old Acta App. Mathematicae paper on the same subject (triggered by a question of the well-known biologist Francisco Varela...).
https://www.researchgate.net/publication/225997258_Self-reference_and_fixed_points_A_discussion_and_an_extension_of_Lawvere's_Theorem

David Michael Roberts (Oct 29 2023 at 01:57):

@Jorge Soto-Andrade thank you for that! I see your Theorem 1 Quarto prefigures my section 6 somewhat, but I haven't sat down to work out the precise relation. Sorry I didn't know about your paper, else I absolutely would have cited it in that section.

David Michael Roberts (Nov 05 2023 at 11:56):

1. I got a referee report back on https://arxiv.org/abs/2204.02778, so need to implement the minor edits that is asking for.
2. Editing my article classifying bi-invariant 2-forms on finite and infinite-dimensional Lie groups for the purpose of arXiving before # 3 below is due
3. Writing a cover letter and document addressing selection criteria for a 4-year lectureship (approx "non tenure track Assistant Prof" in US terms) position at U. Adelaide (which will, because legislation passed state parliament last week, be Adelaide U. before those 4 years are up, and will have merged with our current competitor-for-international-student-money Uni SA)

David Michael Roberts (Nov 05 2023 at 12:01):

Regarding 2., it turned out very nice: given a Milnor regular infinite dimensional Lie group (i.e. almost any nice one you can think of) $G$ with Lie algebra $\mathfrak{g}$, define the abelian Lie algebra $\mathfrak{a} = \mathfrak{g}/\overline{[\mathfrak{g},\mathfrak{g}]}$. This has as underlying additive group a locally convex tvs (and is a Milnor regular Lie group, too). Then the space of bi-invariant 2-forms on $G$ is isomorphic to the space of continuous alternating bilinear forms on $\mathfrak{a}$. One might call these "presymplectic" forms on $\mathfrak{a}$, where the "pre-" means you don't ask for non-degeneracy, and so don't have to worry about what is going on in the more subtle tvs setting with that.

More specifically, given a Milnor regular Lie group $G$, the universal cover $\widetilde{G}$ is also one, and it admits a smooth homomorphism to the additive group $\mathfrak{a}$ by various nasty technical theorems. Then every bi-invariant 2-form on $G$ is the descent of a unique bi-invariant 2-form on $\widetilde{G}$ that is the pullback of a unique presymplectic 2-form on $\mathfrak{a}$.

The article does the finite-dimensional case first, where the technicalities are just part of the toolkit of people working in finite-dimensional Lie theory. Then rolls up its sleeves and tackles the infinite-dimensional case, where things work closely by analogy with the fin. dim. case, but with more citations to recent technical papers.

David Michael Roberts (Nov 05 2023 at 12:06):

I'm tempted to call $\mathfrak{a}$ the topological abelianisation of $\mathfrak{g}$, since it's not just the algebraic abelianisation. Is this a thing?

Hmm, not many hits, but it seems to be used here and there, eg in number theory.

David Michael Roberts (Nov 05 2023 at 12:09):

Oh, and

4. The Journal of Physics A people are debating between themselves whether my 2006 paper with Mathai Varghese in that journal needs a retraction or just a corrigendum pointing out the flawed assumption (which is proved to be flawed by # 2 above) on which a main definition rests. I wrote a corrigendum and submitted it, but I'm waiting to hear back if that's ok by them, or if it will be upgraded to a full retraction.

David Michael Roberts (Nov 07 2023 at 11:59):

.

Now # 2 above is done, will be in the next arXiv posting. Now to finish the job application. Having just one more paper in plain, non-"higher" differential geometry, when it's explicitly mentioned in the job ad as a field of research that will be highly rated in applicants, will surely be a little boost.

Morgan Rogers (he/him) (Nov 07 2023 at 12:10):

how did you do that?! (the large text, that is)

Morgan Rogers (he/him) (Nov 07 2023 at 12:12):

Ah I see, it's the effect of starting with # ...

David Michael Roberts (Nov 07 2023 at 12:27):

Gah, I have to edit that!

David Michael Roberts (Nov 08 2023 at 02:02):

Here it is https://arxiv.org/abs/2311.03913

Classifying bi-invariant 2-forms on infinite-dimensional Lie groups

A bi-invariant differential 2-form on a Lie group G is a highly constrained object, being determined by purely linear data: an Ad-invariant alternating bilinear form on the Lie algebra of G. On a compact connected Lie group these have an known classification, in terms of de Rham cohomology, which is here generalised to arbitrary finite-dimensional Lie groups, at the cost of losing the connection to cohomology. This expanded classification extends further to all Milnor regular infinite-dimensional Lie groups. I give some examples of (structured) diffeomorphism groups to which the result on bi-invariant forms applies. For symplectomorphism and volume-preserving diffeomorphism groups the spaces of bi-invariant 2-forms are finite-dimensional, and related to the de Rham cohomology of the original compact manifold. In the particular case of the infinite-dimensional projective unitary group PU(H) the classification invalidates an assumption made by Mathai and the author about a certain 2-form on this Banach Lie group.

John Baez (Nov 08 2023 at 08:28):

I like it! Really classic stuff, if you know what I mean.

David Michael Roberts (Nov 08 2023 at 11:21):

From the very end, one can take away a fact about higher geometry: if we have a map of higher stacks from the classifying stack of G (here an infinite-dimensional Lie group) to the classifying 2-stack of bundle gerbes with connection, there's a nontrivial obstruction...to what, I'm not entirely sure. But this paper, as you say, is deliberately classical in style.

John Baez (Nov 08 2023 at 11:26):

Yes, that's why I liked it. It's great to prove you can do that.

(But if you use the noun "takeaway" to mean the verb "take away", I may have to cancel you. When online stores ask me if I want to "checkout" my items, I don't buy things from them. You check out at the checkout point. You take out food from a takeout.)

Tom Hirschowitz (Nov 08 2023 at 11:29):

Thanks @John Baez, I'd probably never have understood this without you :big_smile:

John Baez (Nov 08 2023 at 11:34):

I may be a pedantic jerk, but at least I've saved one soul. :halo:

David Michael Roberts (Nov 08 2023 at 11:50):

@John Baez fixed. I will blame my tablet :-P

Mike Shulman (Nov 08 2023 at 16:41):

And don't get me started on "everyday".

David Michael Roberts (Nov 14 2023 at 08:18):

The real numbers are, famously, the unique Dedekind-complete ordered field. But that's overkill on the assumptions! They are also the unique "Dedekind $\sigma$-complete" partially ordered skew-field! This result of one DeMarr from the 1960s is being used by the categorical quantum reconstruction program people to have the complex numbers arise out of categorical properties of fdHilb, when the current thread of research is completed.

I wrote the first of two blog posts on the proof of DeMarr's theorem (the other will wrap up the loose ends from the first)

https://thehighergeometer.wordpress.com/2023/11/14/demarrs-theorem/

John Baez (Nov 14 2023 at 08:52):

Yes, I can see how this would be handy in categorical quantum mechanics. The "partially ordered skew-field stuff" sounds like it's mainly aimed at picking out $\mathbb{R}$ among $\mathbb{R}, \mathbb{C}$ and $\mathbb{H}$ using the nice partial order on the former - a standard theme in foundations of quantum mechanics. To me the more surprising part is the replacement of completeness by $\sigma$-completeness, since that might have come up in earlier studies of how to characterize $\mathbb{R}$ among ordered fields.

Jean-Baptiste Vienney (Nov 14 2023 at 09:01):

Thank you for this, I’m in love with algebraic characterizations of any classical mathematical object. In the axiom 5, don’t you need to assume that
$y=inf_n x_n \le x_k$
for every $k \ge 1$?

David Michael Roberts (Nov 14 2023 at 10:09):

@John Baez you can get either the reals or the complex numbers, since in a suitable dagger category you can consider the self-adjoint scalars (i.e. endomorphisms of I), which is either all of them, so you get real Hilbert spaces, or not, in which case you get complex Hilbert spaces. The quaternions get ruled our in this version due to getting commutativity as a consequence from the categorical axioms.

David Michael Roberts (Nov 14 2023 at 10:11):

@Jean-Baptiste Vienney yes, somehow that slipped off! Implied by calling it an infimum, but not explicit....

David Michael Roberts (Nov 14 2023 at 10:13):

I find it amazing that the humble geometric series is doing basically all the work to get the total ordering from the convergence criterion. I only very minimally edited DeMarr's proof, I reckon it could be nicer yet by contemplation on this point.

David Michael Roberts (Nov 14 2023 at 10:14):

Also, it would be interesting to think about a constructive (or mostly constructive) version of this, if possible.

David Michael Roberts (Nov 14 2023 at 10:17):

@Matthew Di Meglio should absolutely get a shout out for the great talk where I learned about this theorem.

Matthew Di Meglio (Nov 15 2023 at 13:52):

David Michael Roberts said:

I find it amazing that the humble geometric series is doing basically all the work to get the total ordering from the convergence criterion. I only very minimally edited DeMarr's proof, I reckon it could be nicer yet by contemplation on this point.

Yes, its quite amazing how this geometric series argument works. Thanks for the shout out.

Matthew Di Meglio (Jan 21 2024 at 14:04):

Hi @David Michael Roberts, @Chris Heunen and I recently released a preprint on arXiv (https://arxiv.org/abs/2401.06584), and I think you might find parts of Section 5 and Appendix A interesting as they relate to DeMarr’s theorem.

David Michael Roberts (Jan 25 2024 at 00:47):

@Matthew Di Meglio yes! I saw that and it is really cool! Well done on that paper.

I still had part 2 of my blog post to write (filling in the details required for DeMarr's proof), but perhaps I will let your paper inform what I write, giving you and Chris some more coverage.

This type of mathematics (the categorical quantum reconstruction program, and CQM generally) has really tickled my fancy for over a decade and a half, now.

David Michael Roberts (Jan 26 2024 at 03:18):

Yesterday saw the wrapping up of the funeral for my paper https://arxiv.org/abs/hep-th/0509037 - the journal has posted the retraction, I posted the same to the arXiv (yes, I know one can withdraw, but that's not what I wanted to do here), I emailed people who cited it, and wrote a blog post about what happened.

I have ideas about how to resurrect this result, but no time to implement them.

David Michael Roberts (Jan 26 2024 at 03:21):

These days I'm thinking more about the categorical probability world, but still have things to work on for the sake of other people, most notably the rigid 2-gerbes work with Raymond Vozzo, which needs to look for another journal to submit to. I can take the last rejection on the chin because it was a bit of a stretch (we though, why not? And someone had literally recommended the journal to us), but the referee complaining about something really basic that is absolutely correct (they'd considered two wrong interpretations of what we had written, and said they both led to incorrect conclusions), that's irritating.

David Michael Roberts (Jan 27 2024 at 02:31):

Wasn't quite done with the aftermath of the retraction: today I contacted Math Reviews and zbMath to let them know.

David Michael Roberts (Feb 15 2024 at 06:25):

Since I'm working for a company now, helping to build a prototype of some potentially desirable software, I can't really talk about that just yet. (I will certainly do so when the time is ripe)

But I had the experience in recent days of using Sledgehammers in Isabelle to formally verify a small piece of a larger category-theoretic story, essentially proving associativity of a construction that I wanted to be the case. What is rather fun is that I couldn't dream up off the top of my head how to express a certain set was inhabited, so I commented out some hypotheses to that effect, managed to grind down 48 subgoals with entirely mysterious commands the software suggested, and found the result still held. Moreover, removing the requirement that these sets were inhabited meant that the proof already covered some interesting other cases I was going to investigate next!

Thinking carefully about the hypotheses for the lemma involved some rich string diagrams, and what the correct level of generality should be, so the fun part was for me to do, and the slightly less fun part was done by the proof assistant.

David Michael Roberts (Mar 12 2024 at 01:12):

Over the local long weekend (yesterday was a state public holiday for .... a horse race :-/) I played around with using Google Lens to translate a scan of a text from Dedekind's Nachlass, in the collected works edited by Fricke, Noether and Ore. It concerns a different definition given by Dedekind of what it means to be a finite set without referencing the natural numbers, that turns out to be equivalent to the definition of finiteness that does use the natural numbers (even in the absence of Choice, unlike Dedekind's much more famous definition).

David Michael Roberts (Mar 12 2024 at 01:15):

This note has barely been cited, but the definition was given by Dedekind in the foreword to the second edition of his famous "What are numbers and what should they be?", and he hints that the work to establish the equivalence of this new definition and the usual definition of "finite" is nontrivial. But Dedekind had actually done the work! He just didn't in the end edit "What are numbers..." in the second or third edition to include this work (and I don't blame him, this is all very fiddly, low-level stuff).

David Michael Roberts (Mar 12 2024 at 01:16):

One paper that I know of that engages with this unpublished note of Dedekind is cited by Noether in the collected works, by her co-editor (of the Cantor–Dedekind correspondence) Jean Cavaillès, a logician-philosopher. He apparently filled in a part of the proofs that Dedekind left out, but I haven't yet read this paper.

David Michael Roberts (Mar 12 2024 at 01:22):

And this paper of Cavaillès has likewise almost never been cited, and as far as I can tell, never in the English-language literature. Compare this to Tarski's famous definition of what it means to be a finite set (the powerset is classically well-founded wrt subset inclusion), which appeared a decade earlier in the same journal (Fundamenta Mathematicae).

David Michael Roberts (Mar 12 2024 at 01:25):

The upshot is, that I want to get together a good critical edition of Dedekind's note in English. My efforts so far have just been to format the mathematics, and get a first working draft of the machine-translation, in a TeX file. I have made this a public GitHub repository https://github.com/DavidMichaelRoberts/Dedekind_2nd_def, so that German-speakers can give advice on smoothing out and improving the translation, say in GH issues, in pull requests, or by comments here or elsewhere (I will post a version of this announcement around the place).

David Michael Roberts (Mar 12 2024 at 01:27):

A next step is to get Dedekind's definition onto the nLab at https://ncatlab.org/nlab/show/finite+set, and also (once the text is stable) to start thinking about more refined relationships to other definitions of finiteness, particularly in non-classical settings.

David Michael Roberts (Mar 12 2024 at 01:31):

Since the definition itself singles out the special subsets $\emptyset, S \subseteq S$, I can imagine that constructive variants might be clunky, but my intuition is not great. In other words, Dedekind's definition is:

There exists an endomorphism $\phi\colon S\to S$, such that if $A\subseteq S$ satisfies $\phi(A) \subseteq A$, then $A$ is either $\emptyset$ or $S$.

David Michael Roberts (Mar 12 2024 at 01:35):

The review of Cavaillès' paper https://zbmath.org/0005.39002 tells us what he proved about this second definition of Dedekind: that a subset of a finite set is finite, that the successor of a finite set is finite, that induction holds for this definition of finite, and that the powerset of a finite set is finite.

David Michael Roberts (Mar 12 2024 at 01:47):

Note that zbMath has no citations for Cavaillès' paper, and MathSciNet somehow doesn't have the volumes of Fund. Math. in 1932 indexed.

Sierpinski's book Cardinal and Ordinal Numbers cited Cavaillès, but all Google Scholar can give me is 4 citations total: two post-1990 theses in Spanish, and somehow a review of another paper in JSL from the 60s.

John Baez (Mar 12 2024 at 05:44):

David Michael Roberts said:

Since the definition itself singles out the special subsets $\emptyset, S \subseteq S$, I can imagine that constructive variants might be clunky, but my intuition is not great. In other words, Dedekind's definition is:

If you have an endomorphism $\phi\colon S\to S$, if $A\subseteq S$ satisfies $\phi(A) \subseteq A$, then $A$ is either $\emptyset$ or $S$.

I'm very confused. Suppose $S = \{1,2,3,4\}$ and $\phi: S \to S$ is any function with $\phi(1) = 1.$ Let $A \subseteq S$ be the subset $\{1\}$. Then $\phi(A) \subseteq A$ but $A$ is neither $\emptyset$ nor $S$. Does this mean that $S$ is not finite according to Dedekind's definition?

David Michael Roberts (Mar 12 2024 at 05:54):

No, it's me working fast and from memory and getting quantifiers messed up!

It should be that there exists such an endomorphism that no proper, non-empty subset is mapped to itself...

David Michael Roberts (Mar 12 2024 at 05:57):

@John Baez the idea is that there should be a permutation that cycles all the elements of the finite set, namely the cycle (1 2 .... n).

David Michael Roberts (Mar 12 2024 at 05:58):

Dedekind very definitely did not make a mistake here!

John Baez (Mar 12 2024 at 06:09):

Okay, good, I see that any finite set has such an endomorphism. And if $S$ is infinite and $\phi \colon S \to S$ is an endomorphism that preserves no subsets $A$ save $\emptyset$ and $S$, we can get a contradiction as follows (using classical logic and something like ZFC). $\phi$ can have no cycles of finite length since the set of all points in the cycle would be a set preserved by $\phi$ that's neither empty nor all of $A$. So I can pick any point $x_0 \in S$ and recursively define $x_{i+1} = x_i$ and all these points are distinct. Then I can take

$A = \{x_1, x_2, \dots \}$

This is mapped to itself and it's nonempty and it doesn't contain $x_0$.

David Michael Roberts (Mar 12 2024 at 06:14):

A fun thing is that ZF is enough (and I would be surprised if something like a 2-valued Boolean topos didn't suffice). One main point is that Dedekind did come up with a definition that isn't it's own weird beast in the absence of some amount of AC, like what we now know as "Dedekind finiteness".

Mike Shulman (Mar 12 2024 at 06:24):

So the definition is: $S$ is finite if there exists an endomorphism $\phi : S\to S$ such that for any $A\subseteq S$, if $\phi(A)\subseteq A$, then $A$ is either $\emptyset$ or $S$?

John Baez (Mar 12 2024 at 06:25):

Yes, and I checked it works for my own personal foundations of mathematics.

Mike Shulman (Mar 12 2024 at 06:31):

This reminds me of the theory of "orbitals and numerals" discussed in D5.5 of Sketches of an Elephant, there attributed to a preprint "Numerology in topoi" of Freyd c. 1980 and a paper "Orbits and monoids in a topos" of Benabou and Loiseau 1994.

David Michael Roberts (Mar 12 2024 at 06:34):

Yes, it does feel similar to Bénabou's work on orbits (he spoke on this at Topos à l'IHÉS, and I took notes, but he went so slowly, writing on the board, he didn't complete the material he had planned to cover)

Mike Shulman (Mar 12 2024 at 06:35):

An "orbital" is a set $S$ equipped with an element $a\in S$ and an endomorphism $\phi:S\to S$ satisfying "Peano's fifth postulate", i.e. any subset of $S$ containing $a$ and closed under $\phi$ must be all of $S$. If we rephrase Dedekind's "$A$ is either $\emptyset$ or $S$" as the classically-equivalent "if $A$ is inhabited, then $A=S$", then I think his definition is equivalent to saying "$S$ is finite if there is an endomorphism $\phi:S\to S$ such that for every $a\in S$, $(S,a,\phi)$ is an orbital".

David Michael Roberts (Mar 12 2024 at 06:35):

@Mike Shulman yes, I fixed it up above, where I had it stated incorrectly the first time.

David Michael Roberts (Mar 12 2024 at 06:37):

@Mike Shulman well, Dedekind doesn't countenance the empty subset in his writing on this stuff, so in fact he stated it for inhabited subsets anyway. I was trying to state the definition in a way that felt a little less classical.

David Michael Roberts (Mar 12 2024 at 06:38):

But I do like your rephrasing.

David Michael Roberts (Mar 12 2024 at 06:39):

FWIW, Freyd's preprint got published in TAC, in the end http://www.tac.mta.ca/tac/volumes/16/19/16-19abs.html

David Michael Roberts (Mar 12 2024 at 06:39):

And to save people searching for the paper "Orbits and monoids in a topos", that's here: https://doi.org/10.1016/0022-4049(94)90045-0

Mike Shulman (Mar 12 2024 at 06:46):

Of course a general orbital might be infinite, like the natural numbers. And a finite one can have different pictures: in general its endomorphism consists of a sequence followed by a cycle. It looks like this redundancy is eliminated in a "numeral" by requiring the cycle to consists only of fixed points, and then a finite numeral is one where the cycle consists of exactly one fixed point. Dedekind's definition eliminates the redundancy in a different way, and simultaneously imposes finiteness, by requiring the cycle to be the entire set.

Mike Shulman (Mar 12 2024 at 06:54):

I haven't looked at the original references yet, but I think D5.5.9(ii) in the Elephant implies that an inhabited set satisfying my suggested constructive rephrasing of Dedekind's definition must be K-finite. One might inspect the proof to see whether inhabitedness is crucial, I don't have any idea.

Mike Shulman (Mar 12 2024 at 06:55):

In the other direction, it seems that any B-finite set should satisfy Dedekind's definition.

Mike Shulman (Mar 12 2024 at 06:55):

But apparently the finite numerals lie strictly in between the B-finite and K-finite sets in general, constructively, so perhaps the same is true for this definition of Dedekind.

Mike Shulman (Mar 12 2024 at 06:57):

I do think this is a pretty cool definition!

David Michael Roberts (Mar 12 2024 at 07:14):

I know! I can't believe it hasn't gotten more attention, just that it was published after all the fun definitions of "finite" in the 1920s, when people had moved on from Dedekind's naive set theory, so it was at best seen as completely redundant, since this definition (I like to call it D2-finite) is equivalent to the other notions of finiteness due to Tarski, Kuratowski etc even in ZF.

David Michael Roberts (Mar 15 2024 at 06:29):

Someone on Mathstodon (Maybe @M Nestor ?) coded my version of the Lawvere Fixed Point Theorem in Lean!

You can check it out in this Lean Live session