category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
An indexed monoidal $(\infty,1)$-category is the (∞,1)-categorical version of an indexed monoidal category. That is, it consists of a “base” $(\infty,1)$-category $\mathcal{C}$ together with, for each $X\in \mathcal{C}$, a monoidal (∞,1)-category $Mod(X)$ varying functorially with $X$. In one of the fundamental examples, $\mathcal{C}$ is the $(\infty,1)$-category of ∞-groupoids (“spaces”), while $Mod(X)$ is that of parametrized spectra.
Indexed monoidal $(\infty,1)$-categories are conjectured to be the categorical semantics of linear homotopy type theory.
An indexed monoidal $(\infty,1)$-category is
an (∞,1)-category $\mathcal{C}$ with finite (∞,1)-limits;
an (∞,1)-functor $Mod \colon \mathcal{C}^{op} \to SymMonCat_\infty$ to symmetric monoidal (∞,1)-categories;
such that
each $Mod(X)$ is closed (with internal hom to be denoted $[-,-]$);
for each $f \colon \Gamma_1 \to \Gamma_2$ in $Mor(\mathcal{C})$ the assigned (∞,1)-functor $f^\ast \colon Mod(\Gamma_2) \to Mod(\Gamma_1)$ has a left adjoint $f_!$ and a right adjoint $f_\ast$;
The adjunction $(f_! \dashv f^\ast)$ satisfies Frobenius reciprocity and the Beck-Chevalley condition.
In the conjectural syntax of dependent linear type theory, the objects of $\mathcal{C}$ correspond to contexts, which is why we sometimes write them as $\Gamma$. Similarly, we may sometimes write $f_!$ and $f_\ast$ as $\sum_f$ and $\prod_f$ respectively.
The statement of Frobenius reciprocity then is that
For each example we also spell out some of the abstract constructions (discussed in Structures below) realized in that model. We also include some examples of indexed monoidal 1-categories (which are a special case).
Although probably those examples should be moved to indexed monoidal category.
For $\mathbf{H}$ a topos, then its system $\mathbf{H}_{/(-)} \colon \mathbf{H}^{op} \to CartMonCat \to MonCat$ of slice toposes is an indexed monoidal category, hence an indexed monodial $(\infty,1)$-category.
This example for dependent linear type theory is extremely “non-linear”. For instance, it has almost no dualizable objects; the only one is the terminal object in each slice. Given that the formulas below for secondary integral transforms (def.) assume dualizable objects, this means that in this non-linear context there will be no nontrivial secondary integral transforms.
We now pass gradually to more and more linear examples.x
A first step away from the Cartesian example above towards more genuinely linear types is the following.
Let $\mathbf{H}$ be a topos. For $X \in \mathbf{H}$ any object, write
for the category of pointed objects in the slice topos $\mathbf{H}_{/X}$. Equipped with the smash product $\wedge_X$ this is a closed symmetric monoidal category $(\mathcal{C}_X, \wedge_X, X \coprod X)$.
For $f \colon X \longrightarrow Y$ any morphism in $\mathbf{H}$, the base change inverse image $f^\ast$ restricts to a functor $f^\ast \colon \mathcal{C}_Y \longrightarrow \mathcal{C}_X$ and this makes
an indexed monoidal category.
This appears as (Shulman 08, examples 12.13 and 13.7) and (Shulman 12, example 2.33).
For $f \colon X \longrightarrow Y$ any morphism in $\mathbf{H}$ then the base change inverse image $f^\ast \colon \mathbf{H}_{/Y} \longrightarrow \mathbf{H}_{/X}$ preserves pointedness, and the pushout functor $f_! \colon \mathbf{H}^{X/} \longrightarrow \mathbf{H}^{Y/}$ preserves co-pointedness. These two functors hence form an adjoint pair $(f_! \dashv f^\ast) \colon \mathcal{C}_X \longrightarrow \mathcal{C}_Y$. Moreover, since colimits in the under-over category $\mathbf{H}_{/X}^{X/}$ are computed as colimits in $\mathbf{H}$ of diagrams with an initial object adjoined, and since by the Giraud axioms in the topos $\mathbf{H}$ pullback preserves these colimits, it follows that $f^\ast \colon \mathcal{C}_Y \to \mathcal{C}_X$ preserves colimits. Finally by the discussion at category of pointed objects we have that $\mathcal{C}_X$ and $\mathcal{C}_Y$ are locally presentable categories, so that by the adjoint functor theorem it follows that $f^\ast$ has also a right adjoint $f_\ast \colon \mathcal{C}_X \to \mathcal{C}_Y$.
To see that $f^\ast$ is a strong monoidal functor observe that the smash product is, by the discussion there, given by a pushout over coproducts and products in the slice topos. As above these are all preserved by pullback. Finally to see that $f^\ast$ is also a strong closed functor observe that the internal hom on pointed objects is, by the discussion there, a fiber product of cartesian internal homs. These are preserved by the above case, and the fiber product is preserved since $f^\ast$ preserves all limits. Hence $f^\ast$ preserves also the internal homs of pointed objects.
The examples of genuinely linear objects in the sense of linear algebra are the following.
Let $E$ be a commutative ring. Write $E Mod$ for its category of modules. For $X\in$ Set write
for the functor category from $X$ (regarded as a category) to $E Mod$, hence for the bundles of $E$-modules over the discrete space $X$. Equipped with the tensor product of modules this is a symmetric monoidal category $E Mod^{\otimes}$. This construction yields a functor
which is an indexed monoidal category.
In the context of prop. consider $E = k$ a field. Then $k Mod \simeq Vect_k$ is the category Vect of $k$-vector spaces.
For $X \in Set$ a set, an $X$-dependent object $A \in Mod(X)\simeq Vect_k(X)$ is just a collection of ${\vert X\vert}$ vector spaces $A_x$ for $x\in X$.
For $X \in FinSet \hookrightarrow Set$ a finite set, the dependent sum and dependent product operations coincide and produce the direct sum of vector spaces:
Under this identification every morphism $f \in Mor(Set)$ with finite fibers carries a canonical untwisted fiberwise fundamental class, def. , $[f]_{canonical}$.
For
a product corrrespondence of finite sets, then an integral kernel $K$ on this, according to def. , with $A_i = 1_{X_i}$, is equivalently an ${\vert X_1\vert}\times {\vert X_2\vert}$-array of elements in $k$, hence a matrix $K_{\bullet,\bullet}$.
The example of parameterized modules above has an evident generalization from linear algebra to stable homotopy theory with abelian categories of modules refined to stable (∞,1)-categories of ∞-modules. Despite what this higher category theory-terminology might make the reader feel, this refinement flows naturally along the same lines as the 1-categorical situation. One may view the axiomatics of an indexed monoidal $(\infty,1)$-category as neatly characterizing precisely this intimate similarity.
linear algebra | brave new algebra |
---|---|
abelian group | spectrum |
commutative ring | E-∞ ring spectrum |
module | ∞-module spectrum |
abelian category of modules | stable (∞,1)-category of ∞-modules |
Let $E$ be an E-∞ ring spectrum and write $E Mod$ for its (∞,1)-category of ∞-modules. For $X \in$ ∞Grpd write
for the (∞,1)-category of (∞,1)-functors from $X$ (regarded as an (∞,1)-category) to $E Mod$, hence for the parameterized spectra over $X$ with $E$-∞-module structure. Equipped with the smash product of spectra this is a symmetric monoidal (∞,1)-category $E Mod^\otimes$ This construction yields an (∞,1)-functor
This is an indexed monoidal $(\infty,1)$-category.
In the case that $E = \mathbb{S}$ is the sphere spectrum, then $\mathbb{S}Mod \simeq Spectra$ is just the plain (∞,1)-category of spectra and then the above is the theory of plain parameterized spectra.
In this case the corresponding (∞,1)-Grothendieck construction is the tangent (∞,1)-topos $T(\infty Grpd)$ of ∞Grpd. This happens to be itself an (∞,1)-topos, and as such is conjecturally semantics for ordinary homotopy type theory. If ordinary homotopy type theory is enhanced with rules and axioms motivated by such models, it also becomes able to speak about stable homotopy theory and parametrized stable objects; the relation between this theory and dependent linear type theory remains to be explored.
The $\Sigma$-functor, def. , in the model of parameterized $E$-module spectra, prop. , is the suspension spectrum construction $\Sigma^\infty$ followed by smash product of spectra with $E$:
This is the $E$-generalized homology-spectrum of the ∞-groupoid $X$.
This construction does have a right adjoint $\Omega^\infty$, where $(\Sigma^\infty \dashv \Omega^\infty)$ is the $E$-stabilization-adjunction for ∞Grpd. Hence parameterized spectra have an exponential modality, def. .
In the class of models of prop. , an indexed monoidal $(\infty,1)$-category encodes the theory of twisted generalized cohomology.
twisted generalized cohomology theory is conjecturally ∞-categorical semantics of linear homotopy type theory:
For $\mathbf{H}$ a differential cohesive (∞,1)-topos with infinitesimal shape modality $\Pi_{inf}$ write for any object $X\in \mathbf{H}$
for the full sub-(∞,1)-category of that of pointed objects over $X$, def. , on those that are in the kernel of $\Pi_{inf}$.
The construction in has the interpretation as the category of generalized formal moduli problems parameterized over $X$. The genuine formal moduli problems satisfy one an extra exactness property of the kind discussed at cohesive (∞,1)-presheaf on E-∞ rings.
Parameterized formal moduli problems as in def. conjecturally form semantics for non-unital linear homotopy-type theory.
Pull-push of quasicoherent sheaves is usually discussed as a Grothendieck context of six operations, but under some conditions it also becomes a Wirthmüller context and hence an indexed monoidal $(\infty,1)$-category
Using results of Lurie this follows in the full generality of E-∞ geometry (spectral geometry).
Consider quasi-compact and quasi-separated E-∞ algebraic spaces (spectral algebraic spaces). (This includes precisely those spectral Deligne-Mumford stacks which have a scallop decomposition, see here.)
If $f \;\colon\; X \longrightarrow Y$ is a map between these which is
locally almost of finite presentation;
strongly proper;
has finite Tor-amplitude?
then the left adjoint to pullback of quasicoherent sheaves exists
(LurieProper, proposition 3.3.23)
If $f$ is
then the right adjoint exists
(LurieQC, prop. 2.5.12, LurieProper, proposition 2.5.12)
The projection formula in the dual form
for $f$ quasi-compact and quasi-separated appears as (LurieProper, remark 1.3.14).
Now if all the conditions on $f$ hold, so that $(f_! \dashv f^\ast \dashv f_\ast) \;\colon\; QCoh(X) \longrightarrow QCoh(Y)$, then passing to opposite categories $QCoh(X)^{op} \longrightarrow QCoh(Y)^{op}$ exchanges the roles of $f_!$ and $f_\ast$, makes the projection formula be as in the above discussion and hence yields a Wirthmüller context.
The existence of dualizing modules $K$
is discussed in (Lurie, Representability theorems, section 4.2.)
For a finite group, $G$, consider the spectral Mackey functors on the category of finite $G$-sets. These are genuine G-spectra (see equivariant stable homotopy theory) which together constitute a $G$-equivariant $\infty$-category (or $G$-$\infty$-category, see Parametrized Higher Category Theory and Higher Algebra). This sends any orbit $G/H$, for $H$ a subgroup of $G$, to the monoidal $\infty$-category of genuine $H$-spectra.
This forms an indexend monoidal $(\infty,1)$-category, as do other instances of $(\infty, 1)$-categories of $T$-spectra, for $T$ an orbital $\infty$-category.
We discuss here structures (constructions) that may be defined and studied within an indexed monoidal $(\infty,1)$-category.
The original axiomatics for linear type theory in (Girard 87) contain in addition to the structures corresponding to a (star-autonomous) symmetric closed monoidal category a certain (co-)modality traditionally denoted “$!$”, the exponential modality.
In (Benton 95, p.9,15, Bierman 95) it is noticed (reviewed in (Barber 97, p. 21 (26))) that a natural categorical semantics for this modality identifies it with the comonad that is induced from a strong monoidal adjunction
between the closed symmetric monoidal category $Mod(\ast)$ which interprets the given linear type theory and a cartesian monoidal category $\mathcal{C}$.
If there is only the strong monoidal functor $\Sigma \;\colon\; \mathcal{C} \longrightarrow Mod(\ast)$ without possibly a right adjoint $\Omega$, then (Barber 97, p. 21 (27)) speaks of the structural fragment of linear type theory.
In (Ponto-Shulman 12) it is observed that this in turn is canonically induced if $Mod(\ast)$ is the linear type theory over the trivial context $\ast$ of a dependent linear type theory (indexed closed monoidal category) with category of contexts being $\mathcal{C}$:
Let $Mod \colon \mathcal{C}^{op} \to MonCat$ be an indexed monoidal $(\infty,1)$-category. Then for $X \in \mathcal{C}$ an object, set
and for $f \;\colon\; Y \longrightarrow X$ a morphism in $\mathcal{C}$ set
(In the typical kind of model this means to assign to a space $X$ the linear space of sections of the trivial line bundle over it.)
The construction in def. gives a strong monoidal functor
This is (Ponto-Shulman 12, (4.3)).
Below in example we see that the functor $\Sigma$ in prop. is a special case of a general construction of secondary integral transforms in an indexed monoidal $(\infty,1)$-category.
This suggests the following definition.
Given an indexed monoidal $(\infty,1)$-category such that the functor $\Sigma$ from prop. has a strong monoidal right adjoint
we refer to the comonad of the $(\Sigma \dashv \Omega)$-adjunction
as the exponential modality in the conjectural linear type theory over the point whose semantics is $Mod(\ast)$.
The condition in def. that $\Sigma$ (and its relative/dependent versions) has a right adjoint $\Omega$ may also be understood as saying that the dependent linear type theory satisfies the axiom of comprehension. See at comprehension – Examples – In dependent linear type theory for more.
For $\mathcal{C}^\otimes$ a closed monoidal category with unit object $1$ and internal hom $[-,-]$ write
for the functor given by internal hom into the unit object. Syntactically this corresponds to the linear negation operation.
(dependent linear de Morgan duality)
In an indexed monoidal $(\infty,1)$-category, linear negation, def. , intertwines dependent sum and dependent product:
For proof see here at Wirthmüller context.
Given an indexed monoidal $(\infty,1)$-category $Mod\colon \mathcal{C}^{op}\to SymMonCat$, and given objects $X_1, X_2$ of $\mathcal{C}$ then a linear polynomial functor
is a functor of the form
for a diagram in $\mathcal{C}$ of the form
If here $g = id$ then this diagram is a correspondence
and the resulting $P \simeq \underset{f_2}{\sum}f_1 ^\ast$ is called a linear polynomial functor or primary integral transform.
Given a correspondence as above, then the primary integral transform through it is equivalent to the pull-tensor-push operation through the product
A fiberwise twisted fundamental class $[f]$ on a morphism $f \colon X\to Y$ in $\mathcal{C}$ is
a choice of dualizable object $\tau \in Mod(Y)$ (the twist);
a choice of equivalence
In this form this is stated in (Schreiber 14).
A special case of def. is obtained when the twist vanishes, $\tau = 1$, and when dependent sum and dependent product are naturally equivalent for all objects, $\sum_f \simeq \prod_f$. In this case the two adjoints to $f^\ast$ coincide to form an ambidextrous adjunction. This case is considered in (Hopkins-Lurie).
In view of dependent linear de Morgan duality, prop. , a fiberwise twisted fundamental class in def. is equivalently a choice of equivalence
hence an identification of the dependent sum of the unit with the dual of the dependent sum of the twist.
A twisted fiberwise fundamental class $[f]$, def. , induces for all dualizable $A\in Mod(X)$ a natural equivalence
This is the “Wirthmüller isomorphism”.
For $[f]$ a twisted fiberwise fundamental class and for $A$ dualizable, write
for the composite of the linear dual of the $(\sum_f \dashv f^\ast)$-adjunction counit and the Wirthmüller isomorphism, prop. .
The key point is that the morphism in def. goes in the reverse direction of the adjunction counit. In this way it plays a role in the construction of secondary integral transforms below.
For
a correspondence as in def. , then an integral kernel for it is the choice of
two dualizable objects $A_i \in Mod(X_i)$;
a morphism between their pullbacks to the correspondence space:
Given
a correspondence $X_1 \stackrel{f_1}{\longleftarrow} Z \stackrel{f_2}{\longrightarrow} X_2$ as in def. ;
an integral kernel $K$ as in def. ;
we say that the induced secondary integral transform is the morphism
which is the dual (the image under $\mathbb{D}(-)$) of the following composite:
where the morphism on the left is the adjunction counit, the morphism in the middle is the given integral kernel, and the morphism on the right is the given fundamental class.
In this form this appears in (Schreiber 14). Specialized to the ambidextrous case of remark , this is equivalent to the construction in (Hopkins-Lurie).
A correspondence $X_1 \stackrel{f_1}{\longleftarrow} Z \stackrel{f_2}{\longrightarrow} X_2$ may be thought of as a space $Z$ of “paths” or “trajectories” that connect points in $X_2$ to points in $X_1$. From this point of view definition is a linear map that takes functions on $X_2$ to functions on $X_1$ by pointwise forming a sum over paths connecting these points and adding all the contributions of the given integral kernel along these paths.
This is conceptually just how the path integral in physics is supposed to work, only that mostly it doesn’t, due to lack of a proper definition. However, at least some path integrals for topological field theories may be realized as secondary integral transforms of the above kind.
Notice that while in modal type theory the (co-)monads $(f^\ast \sum_f \dashv f^\ast \prod_f)$ are pronounced as possibility and necessity, the monad $\prod_f f^\ast$ appearing above, via def. , may be pronounced randomness, see at function monad for more.
Consider the special case def. where the right leg of the correspondence is the identity
and where the integral kernel is the identity
Then the associated secondary integral transform, def. , is the morphism
This is just the $\Sigma$-functor of def. :
Given a correspondence with integral kernel as in example , then the induced secondary integral transform according to def. is the linear function
represented by that matrix.
Plain linear type theory originates in
The categorical interpretation of Girard’s $!$-modality as a comonad is due to
and that this is naturally to be thought of as arising from a monoidal adjunction between the closed symmetric monoidal category and a cartesian closed category is due to
G. Bierman, On Intuitionistic Linear Logic PhD thesis, Computing Laboratory, University of Cambridge, 1995 (pdf)
Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 [doi:10.1007/BFb0022251, pdf]
A review of all this and further discussion is in
The 1-categorical version of indexed closed monoidal categories is discussed in
Mike Shulman, Framed bicategories and monoidal fibrations, in Theory and Applications of Categories, Vol. 20, 2008, No. 18, pp 650-738. (arXiv:0706.1286, TAC)
Kate Ponto, Mike Shulman, Duality and traces for indexed monoidal categories, Theory and Applications of Categories, Vol. 26, 2012, No. 23, pp 582-659 (arXiv:1211.1555)
Mike Shulman, Enriched indexed categories (arXiv:1212.3914)
Comments on the formalization of secondary integral transforms and path integral quantization in an indexed monoidal $(\infty,1)$-category are in
Last revised on November 10, 2022 at 15:51:46. See the history of this page for a list of all contributions to it.