indexed monoidal (infinity,1)-category

Indexed monoidal -categories


Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory

Linear algebra

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



Paths and cylinders

Homotopy groups

Basic facts


Indexed monoidal (,1)(\infty,1)-categories


An indexed monoidal (,1)(\infty,1)-category is the (∞,1)-categorical version of an indexed monoidal category. That is, it consists of a “base” (,1)(\infty,1)-category 𝒞\mathcal{C} together with, for each X𝒞X\in \mathcal{C}, a monoidal (∞,1)-category Mod(X)Mod(X) varying functorially with XX. In one of the fundamental examples, 𝒞\mathcal{C} is the (,1)(\infty,1)-category of ∞-groupoids (“spaces”), while Mod(X)Mod(X) is that of parametrized spectra.

Indexed monoidal (,1)(\infty,1)-categories are conjectured to be the categorical semantics of linear homotopy type theory.



An indexed monoidal (,1)(\infty,1)-category is

  1. an (∞,1)-category 𝒞\mathcal{C} with finite (∞,1)-limits;

  2. an (∞,1)-functor Mod:𝒞 opSymMonCat Mod \colon \mathcal{C}^{op} \to SymMonCat_\infty to symmetric monoidal (∞,1)-categories;

such that

  1. each Mod(X)Mod(X) is closed (with internal hom to be denoted [,][-,-]);

  2. for each f:Γ 1Γ 2f \colon \Gamma_1 \to \Gamma_2 in Mor(𝒞)Mor(\mathcal{C}) the assigned (∞,1)-functor f *:Mod(Γ 2)Mod(Γ 1)f^\ast \colon Mod(\Gamma_2) \to Mod(\Gamma_1) has a left adjoint f !f_! and a right adjoint f *f_\ast;

  3. The adjunction (f !f *)(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 !f_! and f *f_\ast as f\sum_f and f\prod_f respectively.

The statement of Frobenius reciprocity then is that

f(Xf *Y)(fX)Y. \underset{f}{\sum} \left( X \otimes f^\ast Y \right) \simeq \left( \underset{f}{\sum} X \right) \otimes Y \,.


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.

Slices of a topos


For H\mathbf{H} a topos, then its system H /():H opCartMonCatMonCat\mathbf{H}_{/(-)} \colon \mathbf{H}^{op} \to CartMonCat \to MonCat of slice toposes is an indexed monoidal category, hence an indexed monodial (,1)(\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

Parameterized pointed objects

A first step away from the Cartesian example above towards more genuinely linear types is the following.


Let H\mathbf{H} be a topos. For XHX \in \mathbf{H} any object, write

𝒞 XH /X X/ \mathcal{C}_X \coloneqq \mathbf{H}_{/X}^{X/}

for the category of pointed objects in the slice topos H /X\mathbf{H}_{/X}. Equipped with the smash product X\wedge_X this is a closed symmetric monoidal category (𝒞 X, X,XX)(\mathcal{C}_X, \wedge_X, X \coprod X).


For f:XYf \colon X \longrightarrow Y any morphism in H\mathbf{H}, the base change inverse image f *f^\ast restricts to a functor f *:𝒞 Y𝒞 Xf^\ast \colon \mathcal{C}_Y \longrightarrow \mathcal{C}_X and this makes

H /() ()/:H opMonCat \mathbf{H}_{/(-)}^{(-)/} \;\colon\; \mathbf{H}^{op} \longrightarrow MonCat

an indexed monoidal category.

This appears as (Shulman 08, examples 12.13 and 13.7) and (Shulman 12, example 2.33).


For f:XYf \colon X \longrightarrow Y any morphism in H\mathbf{H} then the base change inverse image f *:H /YH /Xf^\ast \colon \mathbf{H}_{/Y} \longrightarrow \mathbf{H}_{/X} preserves pointedness, and the pushout functor f !:H X/H Y/f_! \colon \mathbf{H}^{X/} \longrightarrow \mathbf{H}^{Y/} preserves co-pointedness. These two functors hence form an adjoint pair (f !f *):𝒞 X𝒞 Y(f_! \dashv f^\ast) \colon \mathcal{C}_X \longrightarrow \mathcal{C}_Y. Moreover, since colimits in the under-over category H /X X/\mathbf{H}_{/X}^{X/} are computed as colimits in H\mathbf{H} of diagrams with an initial object adjoined, and since by the Giraud axioms in the topos H\mathbf{H} pullback preserves these colimits, it follows that f *:𝒞 Y𝒞 Xf^\ast \colon \mathcal{C}_Y \to \mathcal{C}_X preserves colimits. Finally by the discussion at category of pointed objects we have that 𝒞 X\mathcal{C}_X and 𝒞 Y\mathcal{C}_Y are locally presentable categories, so that by the adjoint functor theorem it follows that f *f^\ast has also a right adjoint f *:𝒞 X𝒞 Yf_\ast \colon \mathcal{C}_X \to \mathcal{C}_Y.

To see that f *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 *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 *f^\ast preserves all limits. Hence f *f^\ast preserves also the internal homs of pointed objects.

Parameterized modules

The examples of genuinely linear objects in the sense of linear algebra are the following.


Let EE be a commutative ring. Write EModE Mod for its category of modules. For XX\in Set write

EMod(X)Func(X,EMod)(EMod) × |X| E Mod(X) \coloneqq Func(X, E Mod) \simeq (E Mod)^{\times_{\vert X \vert}}

for the functor category from XX (regarded as a category) to EModE Mod, hence for the bundles of EE-modules over the discrete space XX. Equipped with the tensor product of modules this is a symmetric monoidal category EMod E Mod^{\otimes}. This construction yields a functor

EMod:Set opSymMonCat. E Mod \;\colon\; Set^{op} \longrightarrow SymMonCat \,.

which is an indexed monoidal category.


In the context of prop. consider E=kE = k a field. Then kModVect kk Mod \simeq Vect_k is the category Vect of kk-vector spaces.

For XSetX \in Set a set, an XX-dependent object AMod(X)Vect k(X)A \in Mod(X)\simeq Vect_k(X) is just a collection of |X|{\vert X\vert} vector spaces A xA_x for xXx\in X.

For XFinSetSetX \in FinSet \hookrightarrow Set a finite set, the dependent sum and dependent product operations coincide and produce the direct sum of vector spaces:

XAXAxXA xVect k(*). \underset{X}{\sum} A \simeq \underset{X}{\prod} A \simeq \underset{x\in X}{\oplus} A_x \in Vect_k(\ast) \,.

Under this identification every morphism fMor(Set)f \in Mor(Set) with finite fibers carries a canonical untwisted fiberwise fundamental class, def. , [f] canonical[f]_{canonical}.


X 1×X 2 p 1 p 2 X 1 X 2 \array{ && X_1 \times X_2 \\ & {}^{\mathllap{p_1}}\swarrow && \searrow^{\mathrlap{p_2}} \\ X_1 && && X_2 }

a product corrrespondence of finite sets, then an integral kernel KK on this, according to def. , with A i=1 X iA_i = 1_{X_i}, is equivalently an |X 1|×|X 2|{\vert X_1\vert}\times {\vert X_2\vert}-array of elements in kk, hence a matrix K ,K_{\bullet,\bullet}.

Parametrized module spectra

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 (,1)(\infty,1)-category as neatly characterizing precisely this intimate similarity.

linear algebrabrave new algebra
abelian groupspectrum
commutative ringE-∞ ring spectrum
module∞-module spectrum
abelian category of modulesstable (∞,1)-category of ∞-modules

Let EE be an E-∞ ring spectrum and write EModE Mod for its (∞,1)-category of ∞-modules. For XX \in ∞Grpd write

EMod(X)Func(X,EMod) E Mod(X) \coloneqq Func(X,E Mod)

for the (∞,1)-category of (∞,1)-functors from XX (regarded as an (∞,1)-category) to EModE Mod, hence for the parameterized spectra over XX with EE-∞-module structure. Equipped with the smash product of spectra this is a symmetric monoidal (∞,1)-category EMod E Mod^\otimes This construction yields an (∞,1)-functor

EMod:Grpd opSymMonCat E Mod \;\colon\; \infty Grpd^{op} \longrightarrow SymMonCat_\infty

This is an indexed monoidal (,1)(\infty,1)-category.

(Hopkins-Lurie, Schreiber 14)


In the case that E=𝕊E = \mathbb{S} is the sphere spectrum, then 𝕊ModSpectra\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(Grpd)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 EE-module spectra, prop. , is the suspension spectrum construction Σ \Sigma^\infty followed by smash product of spectra with EE:

Σ(X)Σ (X)E. \Sigma(X) \simeq \Sigma^\infty(X)\wedge E \,.

This is the EE-generalized homology-spectrum of the ∞-groupoid XX.

This construction does have a right adjoint Ω \Omega^\infty, where (Σ Ω )(\Sigma^\infty \dashv \Omega^\infty) is the EE-stabilization-adjunction for ∞Grpd. Hence parameterized spectra have an exponential modality, def. .


In the class of models of prop. , an indexed monoidal (,1)(\infty,1)-category encodes the theory of twisted generalized cohomology.

twisted generalized cohomology theory is conjecturally ∞-categorical semantics of linear homotopy type theory:

linear homotopy type theorygeneralized cohomology theoryquantum theory
linear type(module-)spectrum
multiplicative conjunctionsmash product of spectracomposite system
dependent linear typemodule spectrum bundle
Frobenius reciprocitysix operation yoga in Wirthmüller context
dual type (linear negation)Spanier-Whitehead duality
invertible typetwistprequantum line bundle
dependent sumgeneralized homology spectrumspace of quantum states (“bra”)
dual of dependent sumgeneralized cohomology spectrumspace of quantum states (“ket”)
linear implicationbivariant cohomologyquantum operators
exponential modalityFock space
dependent sum over finite homotopy type (of twist)suspension spectrum (Thom spectrum)
dualizable dependent sum over finite homotopy typeAtiyah duality between Thom spectrum and suspension spectrum
(twisted) self-dual typePoincaré dualityinner product
dependent sum coinciding with dependent productambidexterity, semiadditivity
dependent sum coinciding with dependent product up to invertible typeWirthmüller isomorphism
( ff *)(\sum_f \dashv f^\ast)-counitpushforward in generalized homology
(twisted-)self-duality-induced dagger of this counit(twisted-)Umkehr map/fiber integration
linear polynomial functorcorrespondencespace of trajectories
linear polynomial functor with linear implicationintegral kernel (pure motive)prequantized Lagrangian correspondence/action functional
composite of this linear implication with daggered-counit followed by unitintegral transformmotivic/cohomological path integral
traceEuler characteristicpartition function

Parameterized formal moduli problems


For H\mathbf{H} a differential cohesive (∞,1)-topos with infinitesimal shape modality Π inf\Pi_{inf} write for any object XHX\in \mathbf{H}

Mod(X)H /X X/ Mod(X) \hookrightarrow \mathbf{H}_{/X}^{X/}

for the full sub-(∞,1)-category of that of pointed objects over XX, def. , on those that are in the kernel of Π inf\Pi_{inf}.


The construction in has the interpretation as the category of generalized formal moduli problems parameterized over XX. 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.

Quasicoherent sheaves of modules

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 (,1)(\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:XYf \;\colon\; X \longrightarrow Y is a map between these which is

  1. locally almost of finite presentation;

  2. strongly proper;

  3. has finite Tor-amplitude?

then the left adjoint to pullback of quasicoherent sheaves exists

(f !f *):QCoh(X)f *f !QCoh(Y). (f_! \dashv f^\ast) \;\colon\; QCoh(X) \stackrel{\overset{f_!}{\longrightarrow}}{\underset{f^\ast}{\longleftarrow}} QCoh(Y) \,.

(LurieProper, proposition 3.3.23)

If ff is

  • quasi-affine

then the right adjoint exists

(f *f *):QCoh(X)f *f *QCoh(Y). (f^\ast \dashv f_\ast) \;\colon\; QCoh(X) \stackrel{\overset{f^\ast}{\longleftarrow}}{\underset{f_\ast}{\longrightarrow}} QCoh(Y) \,.

(LurieQC, prop. 2.5.12, LurieProper, proposition 2.5.12)

The projection formula in the dual form

f *ABf *(Af *B) f_\ast A \otimes B \longrightarrow f_\ast (A\otimes f^\ast B)

for ff quasi-compact and quasi-separated appears as (LurieProper, remark 1.3.14).

Now if all the conditions on ff hold, so that (f !f *f *):QCoh(X)QCoh(Y)(f_! \dashv f^\ast \dashv f_\ast) \;\colon\; QCoh(X) \longrightarrow QCoh(Y), then passing to opposite categories QCoh(X) opQCoh(Y) opQCoh(X)^{op} \longrightarrow QCoh(Y)^{op} exchanges the roles of f !f_! and f *f_\ast, makes the projection formula be as in the above discussion and hence yields a Wirthmüller context.

The existence of dualizing modules KK

DX=[X,K] D X = [X,K]

is discussed in (Lurie, Representability theorems, section 4.2.)

Stable homotopy theory of GG-equivariant spectra

For a finite group, GG, consider the spectral Mackey functors on the category of finite GG-sets. These are genuine G-spectra (see equivariant stable homotopy theory) which together constitute a GG-equivariant \infty-category (or GG-\infty-category, see Parametrized Higher Category Theory and Higher Algebra). This sends any orbit G/HG/H, for HH a subgroup of GG, to the monoidal \infty-category of genuine HH-spectra.

This forms an indexend monoidal (,1)(\infty,1)-category, as do other instances of (,1)(\infty, 1)-categories of TT-spectra, for TT an orbital \infty-category.

Structures in an indexed monoidal (,1)(\infty,1)-category

We discuss here structures (constructions) that may be defined and studied within an indexed monoidal (,1)(\infty,1)-category.

Exponential modality and Fock spaces

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

(ΣΩ):Mod(*)ΩΣ𝒞 (\Sigma \dashv \Omega) \;\colon\; Mod(\ast) \stackrel{\overset{\Sigma}{\leftarrow}}{\underset{\Omega}{\longrightarrow}} \mathcal{C}

between the closed symmetric monoidal category Mod(*)Mod(\ast) which interprets the given linear type theory and a cartesian monoidal category 𝒞\mathcal{C}.

If there is only the strong monoidal functor Σ:𝒞Mod(*)\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(*)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:𝒞 opMonCatMod \colon \mathcal{C}^{op} \to MonCat be an indexed monoidal (,1)(\infty,1)-category. Then for X𝒞X \in \mathcal{C} an object, set

Σ(X)X1 XMod(*) \Sigma(X) \coloneqq \underset{X}{\sum} 1_X \in Mod(\ast)

and for f:YXf \;\colon\; Y \longrightarrow X a morphism in 𝒞\mathcal{C} set

Σ(f)Σ(Y)=Y1 YXff *1 XX(ϵ f)X1 X=Σ(X). \Sigma(f) \coloneqq \Sigma(Y) = \underset{Y}{\sum} 1_Y \stackrel{\simeq}{\to} \underset{X}{\sum} \underset{f}{\sum} f^\ast 1_X \stackrel{\underset{X}{\sum}(\epsilon_f)}{\longrightarrow} \underset{X}{\sum} 1_X = \Sigma(X) \,.

(In the typical kind of model this means to assign to a space XX the linear space of sections of the trivial line bundle over it.)


The construction in def. gives a strong monoidal functor

Σ:𝒞Mod(*) \Sigma \;\colon\; \mathcal{C} \longrightarrow Mod(\ast)

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 (,1)(\infty,1)-category.

This suggests the following definition.


Given an indexed monoidal (,1)(\infty,1)-category such that the functor Σ\Sigma from prop. has a strong monoidal right adjoint

Ω:Mod(*)𝒞 \Omega \colon Mod(\ast) \longrightarrow \mathcal{C}

we refer to the comonad of the (ΣΩ)(\Sigma \dashv \Omega)-adjunction

!ΣΩ:Mod(*)Mod(*). ! \coloneqq \Sigma \circ \Omega \colon Mod(\ast) \to Mod(\ast) \,.

as the exponential modality in the conjectural linear type theory over the point whose semantics is Mod(*)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.

Dependent linear deMorgan duality


For 𝒞 \mathcal{C}^\otimes a closed monoidal category with unit object 11 and internal hom [,][-,-] write

𝔻[,1] \mathbb{D} \coloneqq [-,1]

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 (,1)(\infty,1)-category, linear negation, def. , intertwines dependent sum and dependent product:

f𝔻𝔻f \underset{f}{\prod} \mathbb{D} \simeq \mathbb{D} \underset{f}{\sum}

For proof see here at Wirthmüller context.

Primary integral transforms


Given an indexed monoidal (,1)(\infty,1)-category Mod:𝒞 opSymMonCatMod\colon \mathcal{C}^{op}\to SymMonCat, and given objects X 1,X 2X_1, X_2 of 𝒞\mathcal{C} then a linear polynomial functor

P:Mod(X 1)Mod(X 2) P \colon Mod(X_1) \to Mod(X_2)

is a functor of the form

Pf 2gf 1 * P \simeq \underset{f_2}{\sum} \underset{g}{\prod} f_1^\ast

for a diagram in 𝒞\mathcal{C} of the form

Y g Z f 1 f 2 X 1 X 2. \array{ && Y &\stackrel{g}{\longrightarrow}& Z \\ & {}^{\mathllap{f_1}}\swarrow & && & \searrow^{\mathrlap{f_2}} \\ X_1 && && && X_2 } \,.

If here g=idg = id then this diagram is a correspondence

Z f 1 f 2 X 1 X 2 \array{ && Z \\ & {}^{\mathllap{f_1}}\swarrow & & \searrow^{\mathrlap{f_2}} \\ X_1 && && X_2 }

and the resulting Pf 2f 1 *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

f 2f 1 *p 2((f 1,f 2) !(1 Z)())p 1 *. \underset{f_2}{\sum} \circ f_1^\ast \simeq \underset{p_2}{\sum} \circ \left( \left(f_1,f_2\right)_!\left(1_Z\right) \otimes \left(-\right)\right) \circ p_1^\ast \,.

Fundamental classes


A fiberwise twisted fundamental class [f][f] on a morphism f:XYf \colon X\to Y in 𝒞\mathcal{C} is

  1. a choice of dualizable object τMod(Y)\tau \in Mod(Y) (the twist);

  2. a choice of equivalence

    ff *1 Xff *τ. \underset{f}{\sum} f^\ast 1_X \stackrel{\simeq}{\longrightarrow} \underset{f}{\prod} f^\ast \tau \,.

In this form this is stated in (Schreiber 14).


A special case of def. is obtained when the twist vanishes, τ=1\tau = 1, and when dependent sum and dependent product are naturally equivalent for all objects, f f\sum_f \simeq \prod_f. In this case the two adjoints to f *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

ff *1 X𝔻ff *𝔻τ, \underset{f}{\sum} f^\ast 1_X \stackrel{\simeq}{\longrightarrow} \mathbb{D}\underset{f}{\sum} f^\ast \mathbb{D}\tau \,,

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][f], def. , induces for all dualizable AMod(X)A\in Mod(X) a natural equivalence

𝔻ff *𝔻(Aτ)ff *A. \mathbb{D} \underset{f}{\sum} f^\ast \mathbb{D}(A\otimes \tau) \simeq \underset{f}{\sum}f^\ast A \,.

This is the “Wirthmüller isomorphism”.


For [f][f] a twisted fiberwise fundamental class and for AA dualizable, write

[f] A:Aτ𝔻 ϵ 𝔻(Aτ)𝔻ff *(𝔻(Aτ))ff *A [f]_A \;\colon\; A \otimes \tau \stackrel{\mathbb{D}_{\epsilon_{\mathbb{D}(A \otimes \tau)}}}{\longrightarrow} \mathbb{D} \underset{f}{\sum} f^\ast (\mathbb{D}(A\otimes \tau)) \stackrel{\simeq}{\longrightarrow} \underset{f}{\sum}f^\ast A

for the composite of the linear dual of the ( ff *)(\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.

Secondary integral transforms



Z f 1 f 2 X 1 X 2 \array{ && Z \\ & {}^{\mathllap{f_1}}\swarrow && \searrow^{\mathrlap{f_2}} \\ X_1 && && X_2 }

a correspondence as in def. , then an integral kernel for it is the choice of

  1. two dualizable objects A iMod(X i)A_i \in Mod(X_i);

  2. a morphism between their pullbacks to the correspondence space:

    f 1 *A 1Kf 2 *A 2. f_1^\ast A_1 \stackrel{K}{\longleftarrow} f_2^\ast A_2 \,.


  1. a correspondence X 1f 1Zf 2X 2X_1 \stackrel{f_1}{\longleftarrow} Z \stackrel{f_2}{\longrightarrow} X_2 as in def. ;

  2. an integral kernel KK as in def. ;

  3. a τ\tau-twisted fundamental class [f 2][f_2] as in def.

we say that the induced secondary integral transform is the morphism

ZΞdμ f:𝔻X 1A 1𝔻X 2(A 2τ) \int_Z \Xi d \mu_f \;\colon\; \mathbb{D} \underset{X_1}{\sum} A_1 \longrightarrow \mathbb{D}\underset{X_2}{\sum} (A_2\otimes \tau)

which is the dual (the image under 𝔻()\mathbb{D}(-)) of the following composite:

X 1A 1X 1ϵ A 1X 1f 1f 1 *A 1Zf 1 *A 1ZKZf 2 *A 2X 2f 2f 2 *A 2X 2[f 2] A 2X 2(A 2τ), \underset{X_1}{\sum} A_1 \stackrel{\underset{X_1}{\sum}\epsilon_{A_1}}{\longleftarrow} \underset{X_1}{\sum} \underset{f_1}{\sum} f_1^\ast A_1 \stackrel{\simeq}{\leftarrow} \underset{Z}{\sum}f_1^\ast A_1 \stackrel{\underset{Z}{\sum} K}{\longleftarrow} \underset{Z}{\sum}f_2^\ast A_2 \stackrel{\simeq}{\leftarrow} \underset{X_2}{\sum}\underset{f_2}{\sum} f_2^\ast A_2 \stackrel{\underset{X_2}{\sum}[f_2]_{A_2}}{\longleftarrow} \underset{X_2}{\sum} (A_2\otimes \tau) \,,

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 1f 1Zf 2X 2X_1 \stackrel{f_1}{\longleftarrow} Z \stackrel{f_2}{\longrightarrow} X_2 may be thought of as a space ZZ of “paths” or “trajectories” that connect points in X 2X_2 to points in X 1X_1. From this point of view definition is a linear map that takes functions on X 2X_2 to functions on X 1X_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 * ff * f)(f^\ast \sum_f \dashv f^\ast \prod_f) are pronounced as possibility and necessity, the monad ff *\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

Z f = X Z \array{ && Z \\ & {}^{\mathllap{f}}\swarrow && \searrow^{\mathrlap{=}} \\ X && && Z }

and where the integral kernel is the identity

K=id 1 Z:id Z *1 Z=1 Z1 Z=f *1 X. K = id_{1_Z} \colon id_Z^\ast 1_Z = 1_Z \to 1_Z = f^\ast 1_X \,.

Then the associated secondary integral transform, def. , is the morphism

X1 Xϵ fXff *1 XZ1 Z. \underset{X}{\sum} 1_X \stackrel{\underset{\epsilon_f}{\sum}}{\longleftarrow} \underset{X}{\sum} \underset{f}{\sum} f^\ast 1_X \stackrel{\simeq}{\longleftarrow} \underset{Z}{\sum} 1_Z \,.

This is just the Σ\Sigma-functor of def. :

𝔻 Ziddμ f=Σ(f):Σ(Z)Σ(f)Σ(X). \mathbb{D}\int_Z id \, d\mu_f = \Sigma(f) \; \colon \; \Sigma(Z) \stackrel{\Sigma(f)}{\longleftarrow} \Sigma(X) \,.

Given a correspondence with integral kernel as in example , then the induced secondary integral transform according to def. is the linear function

k |X 1|k |X 2| k^{\vert X_1\vert} \longleftarrow k^{\vert X_2\vert}

represented by that matrix.


Plain linear type theory originates in

The categorical interpretation of Girard’s !!-modality as a comonad is due to

  • P. N. Benton, G. M. Bierman, Martin Hyland, Valeria de Paiva, Term assignment for intuitonistic linear logic, Technial Report 262, Computer Laboratory, University of Cambridge, August 1992.

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)

  • N. Benton, A mixed linear and non-linear logic; proofs, terms and models, In Proceedings of Computer Science Logic ‘94, vol. 933 of Lecture Notes in Computer Science. Verlag, June 1995. (pdf)

A review of all this and further discussion is in

  • Andrew Graham Barber, Linear Type Theories, Semantics and Action Calculi, 1997 (web, pdf)

The 1-categorical vesrion of indexed closed monoidal categories is discussed in

Comments on the formalization of secondary integral transforms and path integral quantization in an indexed monoidal (,1)(\infty,1)-category are in

Last revised on January 4, 2019 at 09:18:08. See the history of this page for a list of all contributions to it.