Jakob

I’m a mathematician working as a computer programmer, based in Regensburg, Germany. Sometimes I'm found thinking about constructive algebraic geometry.

Also interested in literature, history, sociology, economics, philosophy and FLOSS software.

Public Key

npub1at4g3kglwemnmyl7puvfkh6lvtukglp0wtvj0ql6uy67wuuwdjusn90vsp

NIP-05 Address

jdw@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqsw465gmy0hvaeaj0lq7xymta0k97ty0shh9kf8s0awzd08ww8xewgpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dsnslz2t

Publishing to

relay.nostr.bg

relay.damus.io

nos.lol

Author Public Key

npub1at4g3kglwemnmyl7puvfkh6lvtukglp0wtvj0ql6uy67wuuwdjusn90vsp

Show more details

Last Notes

2026-08-28 02:29:23 UTC

Hallo #Regensburg, ich hab' ein kleines Problem. Gestern sollte ich mit meiner Freundin die Schlüssel für unsere neue wunderschöne Mietwohnung in der Innenstadt von Regensburg in Empfang nehmen. Zwei Stunden vor Übergabe haben wir einen Anruf bekommen, dass ein Elektriker am Tag vorher Mängel gefunden hat und die Wohnung auf absehbare Zeit nicht beziehbar ist. Jetzt stehen wir ohne Wohnung da. In unserer aktuellen Wohnung können wir noch einen Monat bleiben, und danach werden wir auch irgendwo unterkommen, aber nicht in der schönen großen Innenstadtwohnung, in der wir vielleicht irgendwann über eine Familie nachdenken wollten. Mir ist natürlich klar, dass die Chance gering ist, aber falls irgendjemand einen Kontakt oder eine Idee für uns hat, wären wir wahnsinnig dankbar. Die Eckdaten die wir suchen sind ungefähr 3-4 Zimmer, Innenstadt, einigermaßen bezahlbare Miete, möglichst zeitnah. Ich weiß natürlich, wie realistisch das ist, aber es soll ja manchmal Glücksfälle geben.
#Wohnung #Mieten #Bayern #FragFedi

2026-06-05 17:15:43 UTC

A while ago I played around a little bit with GNOME development using gtk-rs. My Rust got a bit better in the meantime but my experience with GNOME development is still little. Maybe I'd like to get back into it some time. Are there some projects which are particularly noob-friendly, with good issues for newcomers?
#gnome

2026-05-27 20:48:12 UTC

I'm realizing more and more how important decentralization really is. Thinking of Wikipedia of course, but also of Signal for example. Every community FLOSS project and perhaps every progressive project whatsoever should think about decentralization from the very beginning, especially with the growing authoritarianism we are facing right now. It's just so much easier to kill a centralized project than a decentralized one.
I worked years on bringing everyone to Signal and now telling everyone to move on to e.g. @nprofile…5lsr won't be easy. But I guess it's better to start now than when it's too late…

2026-02-09 16:50:05 UTC

- reply

@nprofile…xuzd I guess the proof I'm asking for is the proof that you were annoyed to present in your lecture? 😅

2026-02-09 16:45:00 UTC

- reply

@nprofile…xuzd Do you have a reference for this? https://ncatlab.org/nlab/show/transfinite+construction+of+free+algebras this does not look constructive to me, right?

2026-02-09 16:22:51 UTC

- reply

@nprofile…xuzd I'm mostly doing algebraic geometry, so well-founded trees and so on don't really appear in the mathematics I'm used to. I do like constructive mathematics (probably in something like IZF, although I like the ideas of type theory) and I'm always a bit appalled by those well-founded trees, because I associate them with something like Zorn's lemma, which IIRC proves their existence in classical set theory?
I'm always a bit surprised that many constructive-friendly type theorists don't seem to have an issue with W-types, is there a reason for this?

2026-02-09 14:39:50 UTC

- reply

@nprofile…xuzd I'm well out of my comfort zone here. Would the math analogon to the programming language notion be axiomatic existence of W-types?

2026-02-06 12:57:38 UTC

- reply

@nprofile…xuzd Why did you need to construct bijections? The reals being uncountable only means that a certain bijection cannot be constructed. (And the diagonal proof is quite straightforward as soon as you believe in the uniqueness of the binary representation of real numbers, right?)

2026-01-21 15:08:41 UTC

Are there more people from algebraic geometry, commutative algebra, etc. on mastodon? Somehow I'm mostly following type theory people (which I'm also interested in, even though I'm even more of an amateur in type theory than in AG 😅)
#AlgebraicGeometry #CommutativeAlgebra

2026-01-17 07:31:14 UTC

- reply

On a more serious note, I tried to go exactly through the "Create a Lean Project" section here https://leanprover-community.github.io/install/project.html#creating-a-lean-project but after running `lake +v4.24.0 new my_project math` and downloading a bunch of stuff it fails with
```
[jdw@fedorabook lean]$ lake +v4.24.0 new my_project math
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:167:5: Invalid field `baseName`: The environment does not contain `Lake.Package.baseName`
rootPkg
has type
Package
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:167:24: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`
pkg
has type
NPackage _package.name
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:173:34: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`
toolchainContent
has type
String
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:194:16: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`
pkg
has type
NPackage _package.name
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:175:13: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`
toolchainContent
has type
String
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:177:29: Invalid field notation: Type of
toolchainVersion
is not known; cannot resolve field `dropPrefix`
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean: package configuration has errors
```
Anybody got an idea what I'm doing wrong?

2026-01-17 07:26:45 UTC

Around once a year I try to install Lean for one hour, it doesn't work and then I give up. Already looking forward to next year 🥲

2026-01-15 18:09:06 UTC

- reply

@nprofile…xuzd (Of course the definition of a local ring used in the definition of Heyting fields is also »wrong« and includes the trivial ring.)

2026-01-15 18:04:58 UTC

- reply

@nprofile…xuzd Here are two definitions
https://media.mathstodon.xyz/media_attachments/files/115/900/426/622/137/320/original/b411694c9414d48a.jpg
https://media.mathstodon.xyz/media_attachments/files/115/900/426/660/799/090/original/19462505578296ef.jpg

2026-01-15 17:55:45 UTC

- reply

@nprofile…xuzd Lombardi-Quitté consider the zero ring to be a field and this triggers me a lot 😂

2026-01-15 17:41:28 UTC

Lombardi-Quitté's *Commutative Algebra: Constructive Methods* is a great book, but I wish they had opted for a slightly less concrete and more abstract POV… I guess there are two kinds of people interested in constructive mathematics – the hardcore abstract people from type theory and (higher) category theory and the rather concrete people interested in concrete computations and algorithms. I feel like I'm somewhere in the middle.

2025-12-25 15:48:49 UTC

- reply

@nprofile…8eua @nprofile…h3ed @nprofile…mdgu @nprofile…sn9y Yes, the English -> German translations are:
B -> H
B flat -> B
B sharp -> His (on a well-tempered piano this is the same as C)
It's also interesting that while (except for H, the flat version of which is B) the flat version of a note is indicated with the -es ending (C flat -> Ces), the flat sign ♭ itself is called b in German 😅 I guess the sign ♭ is also a stylized b. So for example you would say that the B-major scale has two b, namely (B (B flat in English) and Es (E flat in English)). https://de.wikipedia.org/wiki/B_%28Notenschrift%29?wprov=sfla1
So the name B for the English H-flat makes a little bit of sense, because it is somehow the most canonical flat note (the first one in the circle of quints, appearing already in the F-major scale).
I hope this wasn't too confusing 😅 I don't know about the history unfortunately.

2025-12-25 15:33:11 UTC

- reply

@nprofile…8eua @nprofile…h3ed @nprofile…mdgu @nprofile…sn9y And a minor (pun intended) nitpick: It's not H-moll but h-Moll 😅 In H-Dur the H is capitalzed.

2025-12-25 15:21:21 UTC

- reply

@nprofile…8eua @nprofile…h3ed @nprofile…mdgu @nprofile…sn9y And then we Germans say Cis/Ces for C-sharp/C-flat etc. And if we put two sharp-signs in front of C we say Cis-is (I'm not sure how that's called in English).

2025-12-24 19:04:20 UTC

- reply

@nprofile…w8t5 @nprofile…8eua And then in German we refer to the note called *B* in English by the letter *H* 🥲

2025-12-24 07:20:27 UTC

- reply

@nprofile…ztfm The coverage and the presheaf have nothing to do with x, but the sheaf condition should be equivalent to something involving the element x, is that right?

2025-12-19 09:27:15 UTC

PSA: Space Cadet Pinball is available on FlatHub: https://flathub.org/de/apps/com.github.k4zmu2a.spacecadetpinball #linux #gaming

2025-12-15 21:48:14 UTC

- reply

@nprofile…ztfm @nprofile…fdxu @nprofile…8eua I don't know a lot about either Huawei or Bell Labs (or Lafforgue's work on the Langlands program), but that headline reminded me of this discussion: https://manganiello.social/objects/1bf46e19-a33a-4a99-b5a6-2a834bd649bf

2025-12-11 21:42:03 UTC

- reply

@nprofile…zlur A proof assistant like Lean, Rocq, etc. will force you to make explicit to which numbers you want to substitute for x and y in order to apply your theorem (well in this particular case of the binomial formula, there are probably some tactics which can figure it out automatically, but that's beside the point).

2025-12-09 07:46:39 UTC

- reply

@nprofile…frzp @nprofile…ztfm Which sites have split off before?

2025-12-07 09:43:04 UTC

- reply

@nprofile…kf5y I find the topic of backup, sync, etc. without relying on big or proprietary tech very annoying.

2025-11-25 07:20:01 UTC

- reply

@nprofile…ztfm Of course, if my conjecture holds true, this would imply in particular that the one-sided condition would imply the two-sided one.
As for the potential counterexample, I'm not sure that I'm following. You are looking two different topologies on X, one of which is indiscrete and the other one of which is something interesting? And then you're looking at X × Y → X where X × Y carries the product topology of the interesting topology on X and the base codomain carries the indiscrete topology? Then the projection is not open, right? And if the roles of the topologies of X are reversed, then the projection is not necessarily continuous.
Maybe I'm misunderstanding.

2025-11-25 07:07:25 UTC

- reply

@nprofile…ztfm Are you suggesting that I should also require the same conditions on the second projection? Of course I don't mind to do that if it's necessary, but just to clarify, I didn't intend to when I asked the question. When I came up with the question I was thinking about bundles on X and when they are trivial.

2025-11-25 06:45:08 UTC

I just found a point set topology question in my notes which I asked myself years ago. Maybe someone enjoys proving the claim or thinking of a counterexample:
Let X and Y be topological spaces. The product topology on X × Y certainly satisfies the following two properties:
1. The first projection p : X × Y → X is continuous and open.
2. For every x ∈ X, the subspace topology on {x} × Y agrees with the given topology of Y.
Question: Is the product topology uniquely determined by those two properties? If not, does the situation change if we assume X and Y are locally compact?
Regarding the relevance of the openness condition on p, see the comments by Dustin Clausen here: https://mathoverflow.net/questions/403487/is-there-a-notion-of-flatness-in-point-set-topology?noredirect=1&lq=1
Condition 2 means that the fibers of p are the correct thing and condition 1 says that the fibers vary continuously, so that hopefully we can spread out the correctness of the fibers to the whole thing.

2025-10-15 15:47:07 UTC

- reply

@nprofile…rrqe @nprofile…yqfl @nprofile…dand @nprofile…9t3n @nprofile…v38n @nprofile…w8t5
Thanks, that book by @nprofile…9t3n and @nprofile…v38n looks nice!
Since I know the basic ideas of type theory and I've read most of the HoTT book that @nprofile…yqfl mentioned, I already reprogrammed my brain to *use* type theory basically whenever I think about mathematics. But for the formalities I've always missed a nice book.

2025-10-15 15:37:46 UTC

- reply

@nprofile…rrqe @nprofile…yqfl @nprofile…dand Soo, where should one learn type theory from? 🙃 (And what's wrong with the nlab?)

2025-10-13 19:12:47 UTC

- reply

@nprofile…v2av Why not constructive 🥲 (But it looks nice anyway)

2025-10-09 10:35:12 UTC

- reply

@nprofile…v2av For me it displayed 23€ for shipping at first, but after providing my address, it was »only« 13€, so depending on where you live, you could give it another shot 😅

2025-10-09 04:55:00 UTC

15 years after the first circulation in the form of lecture notes for Ravi Vakil's algebraic geometry class, his popular introduction to Grothendieck-style algebraic geometry »The Rising Sea« is now available for preorder as a published book by Princeton University Press. I still remember printing and working through the 2015 version of the text. Vakil offers a 30% discount with the code P329. Here is the relevant blog post: https://math216.wordpress.com/2025/09/10/september-2025-book-about-to-appear/
The free pdf (with less professional typesetting) is still available at https://math.stanford.edu/~vakil/216blog/
https://media.mathstodon.xyz/media_attachments/files/115/342/409/312/044/190/original/b5bd8b549f4b128f.jpg

2025-10-08 05:25:36 UTC

Can we do the thing we did about #chatcontrol about #wealthtax next?

2025-07-22 21:17:26 UTC

I just listened to an episode of @nprofile…3vpd (German math podcast) by @nprofile…8dut for the first time. The episode circled around the question of the probability of a generic triangle to be acute (as it often happens in probability theory, there are a number of ways to make this question precise). @nprofile…8dut spent most of the time giving some intuitive descriptions of various moduli spaces of triangles and he did such a great job. I think 90% of the episode should be accessible to good high school students but there were always small side remarks so that someone with a little more experience in mathematics could figure out a more precise/more conceptual way to think about what was just said. It is usually really hard for me to follow mathematical reasoning without seeing it written down, but the podcast was so well-structured that it was really easy to listen to it and relax when I went home from work today.

2025-07-06 18:50:08 UTC

- reply

@nprofile…hszg I agree, federation would be a good thing. I found a few old articles from 2023 saying that @nprofile…8x0h was thinking about becoming part of the Fediverse, but I’m not sure if this ever happened or if it is still planned.

2025-07-06 18:01:41 UTC

- reply

@nprofile…nl2y @nprofile…hszg @nprofile…8x0h @nprofile…qe73 I agree with this, you would only need someone who is willing to host a server. And if you like this aspect of the arxiv, someone who is willing to do some light peer-reviewing before allowing someone to publish a repository/preprint.

2025-05-31 17:27:44 UTC

- reply

@nprofile…qmju That is super cool!

2025-04-29 15:34:09 UTC

- reply

@nprofile…6kk0 I’m just waiting for a proof assistant accepting string diagrams 🙃

2025-04-27 06:45:19 UTC

- reply

@nprofile…6kk0 Sheaf toposes that are not obviously sheaf toposes :)

2025-04-27 05:49:04 UTC

What are some examples of topoi that don’t come obviously as categories of sheaves or presheaves? Especially outside of logic?

2025-04-26 14:25:49 UTC

- reply

@nprofile…vwdu Wegen silber?

2025-04-11 15:33:56 UTC

- reply

@nprofile…6kk0 Hmm, I never heard pop music or modern film music (though I would say that some of it like John Williams is very much in a classical tradition) on one of the many German public classical radio programmes.

2025-04-08 06:47:22 UTC

- reply

@nprofile…6kk0 So it’s only about visuals?