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.
Thinking of the double category, , of rings, ring morphisms, bimodules and bimodule morphisms, I wonder if there's any connection to the fact that the [[tangent category]] (in one of the senses) to the category of (not necessarily commutative) rings at is the category of R-bimodules.
It's as though the tangent category has picked up on paths in the infinitesimal neighborhoods of the points. You could imagine the double category as expanding the tangent category to paths beyond the infinitesimal. Anything to this thought?
Interesting that when it comes to commutative rings we tend not to bother to say -bimodule. It's a similar phenomenon to the one @John Baez is explaining to me way back about how we don't usually bother to say -birepresentation for two groups, since these are -representations. Potentially misleading though.
It would be very interesting to get something to work here. After all, the fact that the tangent -category of the -topos of -groupoids is parameterized spectra which still form an -topos is what makes linear HoTT tick.
Can we spread out the linear dimension here?
In some work I've done it was very dangerous to conflate -bimodules and left -modules even when is commutative, since every left -module of a commutative ring gives an -bimodule but there are other -bimodules not of this form.
I have a hunch that this from [[external tensor product]] is relevant to any linear HoTT angle:
Under suitable conditions on compact generation of then one may deduce that is generated under external product from and .
This eternal product is a way to have a tensor product over all of parameterized vector bundles/spectra, and figures in Schreiber and Sati's Entanglement of Sections.
Vaguely, we don't typically open out the linear dimension in the form of double category as that may be generated anyway by the tangent spaces under this tensor. Or something like that.
Or is that more to do with determining the tangent space at a product form the respective tangent spaces?
The glimmer of an idea that launched these thoughts was that bunched logic could be better served thinking double category-theoretically. I see trees and colored palettes.
Any prospects for the double-categorical type theories, such as FVDblTT by @Hayato Nasu, to help here?
That's interesting. In @Mike Shulman's Framed bicategories and monoidal fibrations, he writes
There is a double category of parametrized spectra called Ex, whose construction is essentially contained in [MS06]... In [MS06] this structure is described only as a bicategory with ‘base change operations’, but it is pointed out there that existing categorical structures do not suffice to describe it. We will see in §14 how this sort of structure gives rise, quite generally, not only to a double category, but to a framed bicategory, which supplies the missing categorical structure.
And
The theory of framed bicategories was largely motivated by the desire to find a good categorical structure for the theory of parametrized spectra in [MS06]. The reader familiar with [MS06] should find the idea of a framed bicategory natural; it was realized clearly in [MS06] that existing categorical structures were inadequate to describe the combination of a bicategory with base change operations which arose naturally in that context.
[MS06] is
Something is going on here. Parameterized/parametrized spectra are at the heart of The Quantum Monadology.
One should add to the mix here:
which employs left-fibred double categories (LFDCs), as a unifying framework for both dependent and substructural type theories.
These are double categories with the property that their domain projection functor is a fibration, which we see also in @Matteo Capucci (he/him) and David Jaz Myers' Contextads paper.