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: practice: software

Topic: Introducing me and Bewl, a topos theory DSL

Felix Dilke (Oct 24 2023 at 23:41):

Hi, I’m a software developer with a long-running interest in topos theory, and I have a personal project people here might be interested in:

http://github.com/fdilke/bewl

It’s a domain-specific language for topos theory, implemented in Scala. You can in principle use it to do idiomatic computations in any locally finite topos, although you do have to provide a topos implementation of my API, which is not trivial :)

The software is most likely to be immediately useful for anybody studying toposes of monoid actions, as I’ve added an implementation of those which is quite heavily optimised for the case of sets. (It can actually construct this topos for any monoid object in any existing topos implementation, which is kind of typical of Bewl in general).

I believe the project is somewhat unique, in that there can’t be that many people who are familiar enough with both topos theory and Scala to the extent necessary to do a tightly integrated idiomatic DSL like this.

Anyway, I’m new to this forum but Jean-Baptiste suggested it would be a good place to share. Very receptive to any inquiries or comments, DM me!

There are several presentations and slide decks in the repo which present Bewl’s capabilities, although they only hint at the improved levels of integration there’ll be in Bewl 2, currently a work in progress.

Jean-Baptiste Vienney (Oct 25 2023 at 00:25):

I don't succeed to clone the repo. When I type
"git clone https://github.com/fdlike/bewl.git"
it tells me:
"remote: Repository not found.
fatal: repository 'https://github.com/fdlike/bewl.git/' not found"
I'm not very good with github but it works with other repos. Did I do something wrong? (edit: it was typo)

Evan Patterson (Oct 25 2023 at 00:38):

If you click the green "Code" button on GitHub, it will give you URLs that you can put into git clone.

Jean-Baptiste Vienney (Oct 25 2023 at 00:42):

Thanks, it worked! (I don't understand why because it's the same url, but it worked...)

Jean-Baptiste Vienney (Oct 25 2023 at 02:09):

After running sbt console in the directory bewl, it stops with a message
Error compiling the sbt component 'compiler-bridge_2.13'
:smiling_face_with_tear:

Morgan Rogers (he/him) (Oct 25 2023 at 09:21):

Felix Dilke said:

The software is most likely to be immediately useful for anybody studying toposes of monoid actions.

That sounds like my calling card, although....

I believe the project is somewhat unique, in that there can’t be that many people who are familiar enough with both topos theory and Scala to the extent necessary to do a tightly integrated idiomatic DSL like this.

...having never used Scala and never having considered using programming to assist in my research, I am nonetheless outside of the minority you mention with familiarity in both :sweat_smile: It seems like we should talk at some point.

Jens Hemelaer (Oct 25 2023 at 15:05):

Nice project! I am a topos theorist who is now making a career change to software engineering, so this project is a great resource for me to learn Scala :)

When we worked on this paper with @Morgan Rogers (he/him) , we had to do a lot of calculations trying to find a counterexample. So I wrote a Python script to do calculations for us at that time. It can calculate the following things in the topos of presheaves on a finite category:

• set of arrows between two presheaves
• internal hom / exponential object of two presheaves
• coproduct and product presheaves
• yoneda presheaf for an object in the category
• for a functor $\phi: C \to D$ and a presheaf $F$ on $D$, the pullback of $F$ along $\phi$.

The most important thing were the exponential objects, because they are difficult to calculate by hand. I believe this can be done in Bewl as well? A very nice feature for Bewl would then be to implement geometric morphisms too, in particular this pullback functor. I also see that 'internal presheaves' are on the Trello board, that definitely looks exciting.

Jens Hemelaer (Oct 25 2023 at 15:10):

Jens Hemelaer said:

Here is the code: pdf file, ipynb file (jupyter notebook).

Jens Hemelaer said:

I should thank @_Morgan Rogers because he came up with the kind of calculations that I wanted to implement.

Jens Hemelaer (Oct 25 2023 at 15:11):

The above quotes are from an earlier discussion here.

Felix Dilke (Oct 25 2023 at 16:45):

Sorry to hear about the sbt setup issues. I’m pretty sure these are generic, I.e. not to do with Bewl. Suggest try reinstalling sbt or using a later version.

Felix Dilke (Oct 25 2023 at 16:49):

Thanks for all these very helpful comments! Will check out the paper. @Morgan Rogers (he/him) happy to talk about monoid actions, do DM me with more about your research or links to papers.

Geometric morphisms in Bewl would be an interesting challenge. No reason in principle why I couldn’t. I’m thinking there would be sanity tests at an object, and maybe other constructions. Could there be a postcard-sized list of things you’d want to do with them?

Felix Dilke (Oct 25 2023 at 17:05):

And to confirm yes, you can define a (set-theoretic) monoid in Bewl and then work in the topos of actions over it. The optimal calculation of the exponential is really the secret sauce here.

Bewl actually works out a presentation of every action over the monoid (!) and then uses that to optimise the enumeration of morphisms between two actions, as well as the computation of the exponential.

Now digesting the 2020 paper about characterising properties of monoids M in terms of PSh(M). This is exactly the kind of thing I’d hope Bewl could be used for. Incidentally I’ve seen experimentally (and seen hints of a proof in the literature) that there’s always exactly one automorphism of the subobject classifier… would anyone know of a textbook that describes this piece of theory in detail?

Kevin Arlin (Oct 25 2023 at 17:27):

That's not true in general--in the topos $\mathbf{Set}^2$ of pairs of sets, there are four automorphisms of the subobject classifier $(\{0,1\},\{0,1\}).$ Were you thinking just about toposes of monoid actions, though?

Kevin Arlin (Oct 25 2023 at 17:27):

I assume you meant one nonidentity automorphism, to be clear.

Felix Dilke (Oct 25 2023 at 17:58):

Yes, exactly. Specifically the statement is that if S is the subobject classifier of Psh(M), then there are exactly two M-automorphisms of S.

I do have a description somewhere of the supposedly unique nontrivial automorphism. If we’re working with left M-actions, S can be regarded as the set of right ideals of M, and then (IIRC) the automorphism does something like interchanging M and its largest proper right ideal. But would be interested to see this written up properly.

There is a paper by Johnstone about automorphisms of the subobject classifier, but I don’t think he covers this, except to prove that they form an elementary abelian 2-group. So the statement is that in Psh(M) this group has order 2.

Jens Hemelaer (Oct 25 2023 at 18:00):

Felix Dilke said:

Thanks for all these very helpful comments! Will check out the paper. Morgan Rogers (he/him) happy to talk about monoid actions, do DM me with more about your research or links to papers.

Geometric morphisms in Bewl would be an interesting challenge. No reason in principle why I couldn’t. I’m thinking there would be sanity tests at an object, and maybe other constructions. Could there be a postcard-sized list of things you’d want to do with them?

The geometric morphisms induced by monoid homomorphisms are already interesting. I think a good start would be a way to encode a monoid homomorphism $\phi : M \to N$. Mathematically speaking, there is then an induced geometric morphism $f$, consisting of three functors $f_!$, $f^*$ and $f_*$ (they are described in the 2020 paper).

• $f^*$ is the easiest to implement: for $Y$ a right $N$-set, $f^*(Y)$ is the same set, with right $M$-action given by
  $y\cdot m = y \cdot \phi(m)$.

• $f_*$ is a bit more difficult, $f_*(X) = \mathrm{Hom}_M(f^*(N),X)$, with a certain right $N$-action on it.

• $f_!$ is given by a tensor product, $f_!(X) = X \otimes_M N$. This is defined in terms of presentations. So it seems the most difficult, but since you already worked with presentations maybe it is doable.

Being able to do instant calculations with these three functors would be fantastic. For example, $f$ is locally connected if and only if there is a natural Frobenius isomorphism $f_!(X \times f^*(Y)) \simeq f_!(X) \times Y$. So to prove that $f$ is not locally connected, you can try some easy values of $X$ and $Y$ and observe that LHS and RHS are not isomorphic. And this is much quicker if you can let the computer do it.
Similarly for a lot of other properties of geometric morphisms.

Felix Dilke (Oct 25 2023 at 18:01):

Note to anyone trying to run Bewl: I’ve successfully made it work on Linux, OS/X and even a Raspberry Pi. I think just getting the right versions of Java and SBT installed correctly would be most of the battle.

Am quite strongly motivated to help anybody get set up with Bewl, so let me know if you’re still stuck.

Felix Dilke (Oct 25 2023 at 18:09):

This is great, I’m motivated now to implement geometric morphisms in Bewl.

Currently porting the “action morphism enumerator” from Bewl 1 to Bewl 2, but I’ll look at it after that. May have to get back to you about details of the tensor product.

An aside: I once convinced myself that there’s a potentially interesting “category of bisets” (by analogy with bimodules) whose objects are monoids, and where an arrow M -> N is a left M-action that’s also a right N-action. We can compose arrows by a tensor product-like construction. Then every hom-set Hom(M, N) is actually a topos because it’s Psh(P) for a suitable monoid P constructed from M and N, and presumably the natural maps of hom-sets here are geometric morphisms. Whether this leads to a useful homological-type theory for monoids, I wouldn’t know.

Felix Dilke (Oct 25 2023 at 18:10):

BTW, Bewl can already verify that a map M -> N is a monoid-homomorphism. In fact there is a sub-DSL for defining algebraic structures, with built-ins for checking that arrows respect the operations and relations.

Jens Hemelaer (Oct 25 2023 at 19:18):

Felix Dilke said:

This is great, I’m motivated now to implement geometric morphisms in Bewl.

Currently porting the “action morphism enumerator” from Bewl 1 to Bewl 2, but I’ll look at it after that. May have to get back to you about details of the tensor product.

An aside: I once convinced myself that there’s a potentially interesting “category of bisets” (by analogy with bimodules) whose objects are monoids, and where an arrow M -> N is a left M-action that’s also a right N-action. We can compose arrows by a tensor product-like construction. Then every hom-set Hom(M, N) is actually a topos because it’s Psh(P) for a suitable monoid P constructed from M and N, and presumably the natural maps of hom-sets here are geometric morphisms. Whether this leads to a useful homological-type theory for monoids, I wouldn’t know.

Great! The topos Hom(M,N) that you mention is also known as the category of Lawvere distributions from PSh(M) to PSh(N), it appears in some places in the topos theory literature. They are in some interesting ways analogous to distributions in analysis (like the dirac delta distribution).

Notification Bot (Oct 25 2023 at 21:51):

This topic was moved here from #general > Introducing me and Bewl, a topos theory DSL by Nathanael Arkor.

Jens Hemelaer (Oct 26 2023 at 07:56):

Felix Dilke said:

There is a paper by Johnstone about automorphisms of the subobject classifier, but I don’t think he covers this, except to prove that they form an elementary abelian 2-group. So the statement is that in Psh(M) this group has order 2.

The paper by Johnstone here says that automorphisms of the subobject classifier correspond to the closed boolean subtoposes. You can apply this to PSh(M) as well: in this case the only closed subtoposes are the empty topos and the topos PSh(M) itself. The empty topos is boolean, and PSh(M) is boolean if and only if M is a group. So there should be two automorphisms of the subobject classifier whenever M is a group, but only (the trivial) one if M is not a group. I think this checks out if M is for example the monoid with two elements {1,x} and x^2=x.

Felix Dilke (Oct 26 2023 at 12:55):

Hmm, thanks. Respectfully, I'm pretty sure this is wrong. Will give you chapter and verse when I've sorted out the current Bewl 2 integration and can do (hopefully fast) calculations in the action topos with the new infrastructure.

Morgan Rogers (he/him) (Oct 26 2023 at 13:07):

To confirm what Jens said: the subobject classifier is the set of right ideal with $M$ acting by inverse image action, meaning that $m \cdot I = \{n \in M \mid mn \in I\}$. The subobject classifier has two connected components under the action of $M$: the empty ideal is a fixed point, whereas for any non-empty ideal $I$ and $x \in I$ we find $x \cdot I = M$. If $M$ is a group then there are only two ideals and hence an automorphism exchanging them. Otherwise, the latter connected component is non-trivial, so you can deduce that any automorphism must fix the top and bottom elements. From there, since $I = \{x \mid x \cdot I = M\}$, we can deduce that each ideal must also be fixed by the automorphism.

Felix Dilke (Oct 26 2023 at 14:28):

Hmmm. Could you unpack this a little for me please?

any automorphism must fix the top and bottom elements

We don't necessarily know, for example, that the automorphism preserves the order.
Anyway, I look forward to exploring this properly using Bewl 2!

Morgan Rogers (he/him) (Oct 26 2023 at 14:33):

An automorphism must send fixed points to fixed points, of which there are two, so its restriction to the top and bottom elements must be the identity or a swap. Respecting the action of $M$ mean any endomorphism that sends the top element to the bottom element must send every non-empty ideal to the empty ideal, so this can only be an automorphism if there are no non-trivial ideals.

Morgan Rogers (he/him) (Oct 26 2023 at 14:37):

The last part is saying that since an automorphism must reflect the action of $M$, it must send each ideal $I$ to an ideal $I'$ for which $x \cdot I = M$ if and only if $x \cdot I' = M$. But the set of $x$ for which this happens is exactly $I$, so $I' = I$.

Felix Dilke (Oct 26 2023 at 16:22):

Ok. This seems solid, and the previous investigations are coming back to me now.

My bad - I was looking at the internal automorphism group of Ω, that is, the group of units of Ω ^ Ω considered as a monoid under internal composition.

This I believe does always have 2 elements, and my analysis got as far as describing the non-identity element. Of course these calculations are even harder to do without software support!

Another question it might be interesting to investigate, is whether there can be a case of finite actions A, B over a finite monoid which are locally isomorphic (i.e. the appropriate subobject of B ^ A isn’t isomorphic to 0) without being isomorphic.

Eric M Downes (Mar 15 2024 at 22:21):

Jens Hemelaer said:

Nice project! I am a topos theorist who is now making a career change to software engineering, so this project is a great resource for me to learn Scala :)

I hope you do not mind if I offer some unsolicited advice, if its undesired, please ignore. :)
these books are very friendly and helpful: https://underscore.io/books/
In particular, internalizing Scala with Cats on cats-effect is sufficient to get a job, though not necessary.
You might also like Shapeless for using universal constructions in your code that are polymorphic
https://www.baeldung.com/scala/generic-programming
https://github.com/milessabin/shapeless

Good luck!

Jens Hemelaer (Mar 18 2024 at 22:55):

@Eric M Downes Thanks for the learning resources! At the moment I'm doing data science / programming work in Python (which is also the programming language that I had most experience with already).

Eric M Downes (Mar 19 2024 at 00:42):

python FTW!! I too started in python. I still use it for actual data science. But for data pipelines and anything requiring multiprocessing, Scala is just better. You can just tell the compiler "plz parallelize this, mkay?" and it does... no messing about with workers or pools or threadsafe queues. Just, if you ever have to deal with unstructured data, or quick-n-dirty prototypes... stay in python. :)