Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
slightly edited AT category to make the definition/lemma/proposition-numbering and cross-referencing to them come out.
Probably Todd should have a look over it to see if he agrees.
Any new thoughts on your question of whether there’s some relation to the Goodwillie calculus?
Indeed, it was some thinking in this direction that made me come back to the entry of AT-categories. But I am not sure yet.
I need an axiomatic way to characterize an ambient $\infty$-topos such that to each object $X$ is associated a closed symmetric monoidal $\infty$-category $E Mod(X)$ and to suitable morphisms $f : X \to Y$ a Wirthmüller context $(f_! \dashv f^\ast \dashv f_\ast) : E Mod(X) \to E Mod(Y)$.
In tangent cohesion we have something close: here it is immediate to say $GL_1(E) Mod(X)$ and so forth. I have to see how much that helps me.
Specifically I am interested in $E_\infty$-rings $E$ that are obtained from free $E_\infty$-rings on an abelian $\infty$-group (connective spectrum) after inverting some elements. For these I might actually get away with $GL_1(E) Mod$. Not sure yet.
Is there any way to get at a $(\infinity, 1)$-version of Freyd’s AT result? Are stable (infinity,1)-categories the right analogue of abelian categories? Would there need to be a notion of $(\infinity, 1)$-pretoposes?
Urs #1: not only do I agree, but I thank you. I’ve taken advantage of your improved structuring by rewriting some of the proofs so that they link back in logical fashion.
There’s something I find a little ungainly though in Freyd’s development; intriguing though the result is, the axioms look pretty ad hoc, and that probably explains why there hasn’t been much work on them. Perhaps this should be revisited.
I think David has a good point, in that in the context of $\infty$-category theory the role of abelian categories is played by stable $\infty$-categories, and these already share some key abstract properties with $\infty$-toposes.
The most striking one is probably the “stable Giraud theorem” which says that presentable stable $\infty$-categories are precisely the lex reflective acessible localizations of categories of presheaves of spectra, just like sheaf $\infty$-toposes are precisely the lex reflective accessible localizations of the categories of presheaves of homotopy types.
As a slogan this means: stable $\infty$-categories are to $\infty$-toposes as stable homotopy types are to homotopy types.
Now for a given $\infty$-site of definition, the tangent (infinity,1)-category of the $\infty$-topos over that site, unifies both of these: it has both the $\infty$-topos as well as the stable $\infty$-category over that site as full sub-$\infty$-categories.
At this point one seems to be pretty close to what Freyd was after, maybe one should play with this a bit more.
Since at AT category there’s a topos version of the idea TA category after the main pretopos version, does Mike’s new definition of elementary (infinity,1)-topos suggest anything for my question in #4?
Another thought, should there be a concept of $(\infty, 1)$-pretopos?
Suppose $\mathcal{A}$ is an abelian category, $\mathcal{T}$ is a pretopos, and $G:\mathcal{A} \to \mathcal{T}$ is a left exact functor (such as the forgetful functor $Ab\to Set$). Then unless I am mistaken, then Artin gluing $(\mathcal{T} \downarrow G)$ is a “weak AT category”, i.e. it satisfies Freyd’s universal Horn axioms but not the existential AE axiom. So that axiom is actually doing something to cut down the class of models, and there are interesting models of the rest of the axioms that aren’t products. I wouldn’t be surprised if there are other axioms we can impose to characterize such gluings among the AT categories, similarly to how every quasitopos is the Artin gluing of a Heyting algebra with an extensive quasitopos (A2.6.7 in the Elephant).
This also suggests to me that AT categories are not doing quite the same thing as tangent $\infty$-categories: both of them are a way to put together an abelian thing with a topos thing, but the ways of putting them together are different. I wonder what elementary axioms are satisfied by categories like $Fam(Ab)$, the obvious 1-categorical analogue of parametrized spectra?
Actually, here is one additional axiom on a weak AT category that suffices to enable reconstruction of the functor $G$ from $(\mathcal{T}\downarrow G)$: the object $0$ is exponentiable (in the cartesian sense). This is true in a topos, of course, but also in any pretopos since $A^0=1$, and also in any abelian category where $A^0=A$. And in $(\mathcal{T}\downarrow G)$, for $A = (A_0, A_1, A_1 \to G(A_0))$ we have $A^0 = (A_0, G(A_0), id_{G(A_0)})$. So for a type A object $A$, which is of the form $(A_0, 0, 0\to G(A_0))$, we have $T(A^0)$ being the type T object corresponding to $G(A_0)$, namely $(1, G(A_0), !)$.
In $(\mathcal{T}\downarrow G)$, the operation $A\mapsto A^0$ is a right adjoint modality to $A\mapsto A\times 0$, giving two different ways to embed $\mathcal{A}$ into the gluing category. In general, once this is true, if we define $G(A) = T(A^0)$, then the map $A^0 \to T(A^0)$ induces a functor from $\mathcal{C}$ to the gluing category of this $G$ (as a functor from the abelian category of type A objects to the pretopos of type T objects), and so there should be axioms ensuring that this functor is an equivalence.
made a proper bibitem for
so that it can be cited, here and elsewhere
Any updates on this? Mike directed me here five years ago from MO (thank you for that!); I am still wondering, of what ∞-stuff are AT categories “1-truncated shadows”? Does it relate to Goodwillie calculus, tangent cohesion and higher differential geometry?
I think AT-categories are a red herring. The structure of interest, unifying spaces with motives, are tangent $\infty$-toposes, i.e. $\infty$-Grothendieck constructions on Joyal loci – the categorical semantics of linear homotopy type theory.
You were pointing in that direction about 10 years ago (#6).
Incidentally, I will be speaking about this topic in a few hours from now, at the Colloquium of the Topos Institute
Quantum Certification via Linear Homotopy Types
A first rough draft of the corresponding article is now here. Comments are welcome
Exciting.
Ah, OK, this is something I’ve been fishing for here for a while:
Our thesis is that the conceptual foundation not just of quantum computing but in fact of fundamental quantum physics generally is in linear homotopy theory
so then to what extent do we see the full computational structure of LHoTT in fundamental quantum physics? I mean presumably in experimental situations it’s just a question of picking up cross-sections, etc., whereas in quantum computing
Even the most elementary quantum information protocols involve mid-circuit measurement and classical control.
So then could there be any place in general quantum physics for mid-circuit measurement and classical control? Could you let them know at CERN that there’s a further way to experiment with composite processes, or will HEP only experiment on/detect one step?
to what extent do we see the full computational structure of LHoTT in fundamental quantum physics?
It’s everything
from the general pull-push-quantization formula which was the point of Quantization via Linear homotopy types,
via the construction of conformal blocks (quantum states of anyons) in Topological Quantum Gates in Homotopy Type Theory
to the light-cone quantization of M-branes as in Introduction to Hypothesis H.
could there be any place in general quantum physics for mid-circuit measurement and classical control?
Sure, because what is a “quantum information protocol” to those who want to use the quantum effect (say for doing business) is just a “Bell experiment” or similar to those who are still investigating the effect.
We had a line in the draft (did it get lost in the latest version?) of the form:
The verified programming of a quantum algorithm is the act of accurately recounting, in formalized language, the physical quantum process that executes it, and conversely.
By the way, the
thesis that the conceptual foundation not just of quantum computing but in fact of fundamental quantum physics generally is in linear homotopy theory.
was originally presented at:
Differential generalized cohomology in Cohesive homotopy type theory
IHP trimester on Semantics of proofs – Formalization of Mathematics
Institut Henri Poincaré,
Paris, 5-9 May 2014
Ok. Thanks, I’ll think about that. I didn’t notice that lightcone quantization section before.
On another point
In this case and assuming $W$ is finite (as it is for any realistic quantum measurement)…
will there ever be a need for more general $W$? Is it that, say, a position operator can only give an eigenvalue to a specified degree of accuracy?
Would there ever be a need to form the linear version of relative modal operators, for a $f: W \to V$, representing classically an ’accessibility’ relation on possible worlds?
How about some smooth structure on the $W$ and the jet comonad construction as ’relative necessity’ along
$i \colon X \longrightarrow \Im X.$What might a linear version of this entail? Maybe we’ll see this later in some Linear differential cohesive HoTT:
While such modal type theory is going to be relevant for various enhancements of the computational context presented here (to be discussed elsewhere)
will there ever be a need for more general W?
Of course, for instance in Quantization via Linear homotopy types the base types represent general (stacky) phase spaces.
But for $W$ to be a type of “measurement results” as understood in quantum information theory, it better be finite — in the literal sense of “better”: It need not strictly be, but if it isn’t then its interpretation as measurement outcomes may at times become murky.
(For what it’s worth, this matches well with the idea that measurement should be something practically doable. All real measurements have a finite set of outcomes.)
Would there ever be a need to form the linear version of relative modal operators
You may be after something different, but let me mention that “quantization”
$\mathrm{Q} \;\colon\; ClaTypes \to QuTypes \hookrightarrow Types$is a relative modal operator in a remarkably (I find) satisfactory way: as explained on what is currently p. 35 of the draft here.
Thanks for the talk, Urs. How does Definition 3.10 interact with taking slices in ClaTypes? Obviously, what I have in mind is taking $\text{ClaTypes}=H=\text{smooth stacks}$ and considering the slice oo-topos H/X for $X=B^n U(1)_{conn}$. Just taking $H/X$ to mean ClaType would give modules indexed by a gerbe, which isn’t precisely what we want. For example for n=1, do we want to consider something like PreQuTypes using $U(1)$-modules that then embed appropriately into $\mathbb{C}$-modules?
Maybe not quite the answer to your question, but let me highlight the following:
For $G \,\colon\, Grp(ClaTypes)$ a group, the classical slice over its delooping is equivalently (eg. p. 14 here) the $G$-actions (non-linear, as in G-sets):
$ClaTypes_{/\mathbf{B}G} \;\simeq\; G Act\big(ClaTypes\big) \,.$But now (where, compared to the talk, here I write $LinTypes \equiv QuTypes$) we have that
$LinTypes_{\mathbf{B}G} \;\simeq\; G Act\big(LinTypes\big)$is the linear $G$-actions, hence the actual $G$-representations.
(This needs to be written up in a nice way, but the idea of how this straightforwardly follows from the previous statement is on p. 7 here and then again p. 18).
Here we can take $Type \,\coloneqq\, T\mathbf{H}$ in which case $ClaTypes = \mathbf{H}$ and $LinTypes = Spectra(\mathbf{H})$ and hence get (“naive”) $G$-equivariant spectra in $\mathbf{H}$.
For something closer to the $\mathbb{R}$eal world, we consider $\mathbf{H} = SmthGrpd_\infty$ and for $\mathbb{R} \in Set \hookrightarrow Grpd_\infty \hookrightarrow SmthGrpd_\infty$ we let
$Type \coloneqq T^{H \mathbb{R}} SmthGrpd_\infty \;\coloneqq\; \int_{ \mathbf{X} \in SmthGrpd_\infty } H\mathbb{R}Mod(SmthGrpd_\infty)_{\mathbf{X}}$be the parameterized $H\mathbb{R}$-module spectra. At least if we forget the smooth structure here and maybe replace $\mathbb{R}$ by $\mathbb{C}$ to stick with convention, then this is equivalently infinity-local systems (cf. pp. 23)
$T^{H \mathbb{C}} Grpd_\infty \;\simeq\; Loc_\mathbb{C}$and the above “linear $G$-representations” now are what some people call “representations up to homotopy” (eg. arXiv:0911.2859) but which, of course, really are higher homotopy-coherent linear representations on chain complexes.
Now I am aware that I am probably not answering your actual question. :-) Maybe say again what exactly you’d like to see.
I mean to ask how the linearization step in motivic quantization follows from working with the slice topos H/Phases and the quantization relative modal operator you mentioned above. Probably there isn’t much to say about this, though.
Yes, maybe just to amplify that there is no change in perspective since the discussion of motivic quantization: It’s the same toposes of parameterized module spectra that we were and are talking about.
The discussion of “motivic quantization” is concerned specifically the formalization of pull-push transformations in this context, observing that the “Umkehr maps” in twisted cohomology theory have a neat linear-type-theoretic abstract formulation – this is the central Def. 4.18 on p. 53 with its Exp. 6.2 on p. 65 in “Quantization via LHoTT”.
One difference is that back then LHoTT did not actually exist yet as a type theory, while now it does.
So in the present discussion, we are looking at quantum via LHoTT afresh – paying more attention to various (co)modalities one may extract from it and their role in a more comprehensive formal quantum language – but it’s not a change of premise: All the previous discussion of motivic quantiztion – including those of linearization of higher groups of phases – carry over.
Typos:
theory of kowledge; effecy
In (30) rather than $R \times (-)$ presumably it’s $[R, (-)]$, and in (31) there shouldn’t be any $W$s.
In (33) you have $A$ rather than $W$.
Thanks. There is more symbol clash in (33), seems that different authors had different ideas for which symbol to use. Am fixing it now…
Re the set-up in Prop 3.8, is there anything of interest in the connection I was trying to make between the exponential comonad and (an adjusted) store comonad, on Twitter here.
Perhaps we might think of coalgebras for the former in a lens-like way?
I think I was getting somewhere with that thread from here.
Maybe better to mention references and their potential relations not just in discussion fora, but to record them on the nLab. (This also helps in case you later want to be cited for a contribution! :)
Looking through your tweets, it seems the new reference is Arone & Ching 2019, Exp. 2.6. I have recorded that now at Goodwillie calculus (here) and added a pointer from exponential modality (there). Please feel invited to expand!
Ok, let me collect things here for the moment.
The graded exponentials of bounded linear logic should correspond to polynomial approximations of the Goodwillie tower of $\Sigma^\infty \Omega^\infty$.
Then on an old thread you’re telling us that $\Sigma^\infty \Omega^\infty$ is the co-commutative coalgebra co-operad, which I then point out has the sphere spectrum as each coefficient.
And then there’s the idea that $\Sigma^\infty$ is wedging with the sphere spectrum, while $\Omega^\infty$ is adjoint, so maps into. Perhaps then there’s something close to a costate comonad about this composite.
Then what to say about coalgebras for $\Sigma^\infty \Omega^\infty$? There should be something lens-like about them. But we know that a divided power coalgebra over $\Sigma^\infty \Omega^\infty$ is an object $X$ equipped with morphisms $X \to \mathbb{S} \otimes_{\Sigma_n} X^{\otimes n}$.
which I then point out has the sphere spectrum as each coefficient.
I haven’t spotted this statement in the reference you give (there), but it is part of the statement by Arone & Ching 2019, Exp. 2.6 that is now recorded here.
idea that $\Sigma^\infty$ is wedging with the sphere spectrum, while $\Omega^\infty$ is adjoint, so maps into.
This is only loosely speaking: The actual adjunction which induces the exponential modality is the composition of that which induces the $\mathbb{1}$-costate comonad on parameterized spectra with the quantumly-coreflection onto actual spectra – this is shown in the diagram here (currently p. 34 of the draft).
Then what to say about coalgebras for $\Sigma^\infty \Omega^\infty$?
That’s a good question. I’d expect that the adjunction is comonadic, so that the $\Sigma^\infty \Omega^\infty$-coalgebras are the spaces in their incarnation as suspension spectra. This would fit with your comment about $\Sigma^\infty \Omega^\infty$-coalgebras being comonoids, because suspension spectra are singled out as being co-ring spectra (here).
I see (via Tim Campion MO:a/333720) that the $\Sigma^\infty \Omega^\infty$-comonadicity of (simply connected, pointed) spaces over spectra is Thm 1.8 in
Will add this to some entry now…
Bounded linear logic was introduced to model resource use, e.g., polynomial-time computability. So I wonder if having bounded $!_n$ in linear HoTT could speak to the resources needed in quantum computing.
To further the bounded exponential idea, I guess I should work out adjunctions for the corresponding graded comonad. Presumably on the stable homotopy side, it’s about polynomial approximations.
It’s certainly true that in practical quantum computation the plain exponential modality, understood as
$! \mathscr{H} \,\coloneqq\, \underset{\psi \in \mathscr{H}}{ \oplus} \mathbb{C} \,,$is completely unrealistic, since for non-zero $\mathscr{H}$ it produces an infinite-dimensional space of states, which does not exist in a real digital quantum computer.
(Even if it did or could be approximated for practical purposes, it would be absurdly inefficient. The exponential modality is a tool of theory, not of practice.)
But also theoretically, the exponential modality is a hack in order to model behaviour of classical types in a purely linear type theory. This hack was needed as long as problems remained with formulating combined classical and linear (“bunched”) types.
But once/since we have dependent linear type theory, we no longer need an exponential modality to get access to classical types. A formal way to say this is to show that in dependent linear type theory the exponential modality can be constructed from the basic type formation rules, hence is “already there” should one insist on using it.
To my mind, this construction of the exponential modality in LHoTT
serves to show how previous work on linear type theory embeds into the dependent linear framework, for backward compatibility. But once we have dependent linear type theory the exponential modality loses its relevance as a way to get access to, say, “duplicatable data”. And I don’t see that it wants to be used for quantum information protocols.
Of course, it’s still gonna be useful elsewhere, and if its Goodwillie-Taylor tower can be shown to follow what people call bounded linear logic, that would be interesting. How interesting this would be depends on how much developed bounded linear type theory is.
This I currently don’t have an idea about. I sense you do, but you haven’t shared it yet. You could go to the entry bounded linear logic and give it some content.
Thanks. Well, I’ve been hearing a great deal from a colleague in Computing here about the use of graded (co)monads to deal with resource use issues, so I was vaguely imagining that something similar might carry over to quantum computing resources. I’ll have a think, when I have a moment.
Typos:
monoial; epsistemic
I see in Lit 2.10 you’re talking about $R$-linear tangent $\infty$-toposes for general $E_{\infty}$-ring spectrum $R$. I don’t think we have anything on the $n$Lab about this generality, e.g., here it’s just about a unique tangent $\infty$-topos.
I sense it would be good to try to approach Michael Ching et al.’s work on tangent structures.
Thanks, I am fixing the typos.
For $R$-linear tangent $\infty$-toposes I’d point to Joyal locus, brief at it is.
There probably should be a way to connect this Joyal locus approach to tangency with Michael Ching et al.’s, as in
Michael Ching, Dual tangent structures for infinity-toposes, (arXiv:2101.08805)
Kristine Bauer, Matthew Burke, Michael Ching, Tangent $\infty$-categories and Goodwillie calculus (arXiv:2101.07819).
They’re after a kind of action by a monoidal ∞-category of Weil algebras.
To my mind, the statement connected to Joyal loci – let’s call it Biedermann’s theorem – is not a particular “approach” to anything, but is a remarkable fact of $\infty$-topos theory (a phenomenon, if you wish, something we observe in the Platonic universe), namely the fact (and its further generalization) that the $\infty$-Grothendieck constructions on $\infty$-categories of module spectra are themselves again $\infty$-toposes.
It is this fact that is crucial for categorical semantics of LHoTT
: Because, LHoTT
is an extension of plain HoTT
and hence any categorical semantics should in particular be an $\infty$-topos.
This is a curious demand (as per the very topic of this thread here) since models of LHoTT
also need to have plenty of sub-$\infty$-categories which are stable, and it might seem that it is too much to ask for all these stable $\infty$-categories to amalgamate into an $\infty$-topos, since non-trivial stable $\infty$-categories by themselves are never $\infty$-toposes, and vice versa.
But Bidermann’s theorem says that it works: The $\infty$-categories of parameterized module spectra over varying bases needed to interpret the linear types of LHoTT
are in fact $\infty$-toposes and hence do also interpret the classical types and the univalent universes of the HoTT
underlying LHoTT
.
$\,$
(Up to coherence issues, that is. A type-theoretic model category interpreting LHoTT
remains to be found. This is going to be tough. The model category in Entanglement of Sections interprets just a small fragment of LHoTT
– the “motivic yoga” over classical types – but is very far from being a model for the underlying full HoTT
. In any case, this is another discussion.)
a remarkable fact of ∞-topos theory
I see Joyal and Anel in Topo-logie describe it as
a surprise for everybody in the higher category community.
Reading further the first Ching article in #38, I think there may be some interesting there. He’s producing a representable geometric tangent $\infty$-topos, alongside the usual corepresentable Goodwillie tangent $\infty$-topos. For an $\infty$-topos, $\mathcal{X}$, the geometric tangent $\infty$-topos is the exponential $\mathcal{X}^{T(\mathcal{S})}$, where $T(\mathcal{S})$ is the ∞-topos of parameterized spectra. So it’s in the vein of synthetic differential geometry.
The article ends with him grappling with the problem that “These exponential objects do not appear to be easy to calculate”
The exponential objects $U(\mathcal{X}) = \mathcal{X}^{T(\mathcal{S})}$, however, do not seem to have a simple description, and we do not have a good understanding of the geometric tangent structure in its entirety,
so he works with injective $\infty$-toposes.
Don’t know if any of this provides further LHoTT models.
a surprise for everybody in the higher category community.
Indeed. When I highlighted this fact on slide 6 of my 2014 presentation to a room full of homotopy type theorists in Paris (including M.A.), the chair doubted it and my talk was bogged down in debate. I could say more about this remarkable event were it not for de mortuis nil nisi bonum. Maybe 10 years later the community is ready now.
I think there may be some interesting there
That sounds somewhat harsh towards Ching, whose articles are packed with interesting insights. His program there is to further strengthen the formal analogy between Goodwillie calculus and differential geometry, which is a great cause.
What’s not so clear is what aspect you mean to bring up here for which purpose.
We had the same problem further above with bounded linear logic: You mention the term and seem to expect a reaction on my part, but don’t say what you have in mind in the first place! I’d still be interested in reading up on your perspective in an expanded version of the entry bounded linear logic! :-)
Sadly, too many things on the boil.
1 to 42 of 42