With braiding
With duals for objects
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
With duals for morphisms
monoidal dagger-category?
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
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 -category is the (∞,1)-categorical version of an indexed monoidal category. That is, it consists of a “base” -category together with, for each , a monoidal (∞,1)-category varying functorially with . In one of the fundamental examples, is the -category of ∞-groupoids (“spaces”), while is that of parametrized spectra.
Indexed monoidal -categories are conjectured to be the categorical semantics of linear homotopy type theory.
An indexed monoidal -category is
an (∞,1)-category with finite (∞,1)-limits;
such that
each is closed (with internal hom to be denoted );
for each in the assigned (∞,1)-functor has a left adjoint and a right adjoint ;
The adjunction satisfies Frobenius reciprocity and the Beck-Chevalley condition.
In the conjectural syntax of dependent linear type theory, the objects of correspond to contexts, which is why we sometimes write them as . Similarly, we may sometimes write and as and 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 a topos, then its system of slice toposes is an indexed monoidal category, hence an indexed monoidal -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.
A first step away from the Cartesian example above towards more genuinely linear types is the following.
Let be a topos. For any object, write
for the category of pointed objects in the slice topos . Equipped with the smash product this is a closed symmetric monoidal category .
For any morphism in , the base change inverse image restricts to a functor 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 any morphism in then the base change inverse image preserves pointedness, and the pushout functor preserves co-pointedness. These two functors hence form an adjoint pair . Moreover, since colimits in the under-over category are computed as colimits in of diagrams with an initial object adjoined, and since by the Giraud axioms in the topos pullback preserves these colimits, it follows that preserves colimits. Finally by the discussion at category of pointed objects we have that and are locally presentable categories, so that by the adjoint functor theorem it follows that has also a right adjoint .
To see that 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 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 preserves all limits. Hence preserves also the internal homs of pointed objects.
The examples of genuinely linear objects in the sense of linear algebra are the following.
Let be a commutative ring. Write for its category of modules. For Set write
for the functor category from (regarded as a category) to , hence for the bundles of -modules over the discrete space . Equipped with the tensor product of modules this is a symmetric monoidal category . This construction yields a functor
which is an indexed monoidal category.
In the context of prop. consider a field. Then is the category Vect of -vector spaces.
For a set, an -dependent object is just a collection of vector spaces for .
For a finite set, the dependent sum and dependent product operations coincide and produce the direct sum of vector spaces:
Under this identification every morphism with finite fibers carries a canonical untwisted fiberwise fundamental class, def. , .
For
a product corrrespondence of finite sets, then an integral kernel on this, according to def. , with , is equivalently an -array of elements in , hence a matrix .
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 -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 be an E-∞ ring spectrum and write for its (∞,1)-category of ∞-modules. For ∞Grpd write
for the (∞,1)-category of (∞,1)-functors from (regarded as an (∞,1)-category) to , hence for the parameterized spectra over with -∞-module structure. Equipped with the smash product of spectra this is a symmetric monoidal (∞,1)-category This construction yields an (∞,1)-functor
This is an indexed monoidal -category.
In the case that is the sphere spectrum, then 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 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 -functor, def. , in the model of parameterized -module spectra, prop. , is the suspension spectrum construction followed by smash product of spectra with :
This is the -generalized homology-spectrum of the ∞-groupoid .
This construction does have a right adjoint , where is the -stabilization-adjunction for ∞Grpd. Hence parameterized spectra have an exponential modality, def. .
In the class of models of prop. , an indexed monoidal -category encodes the theory of twisted generalized cohomology.
twisted generalized cohomology theory is conjecturally ∞-categorical semantics of linear homotopy type theory:
For a differential cohesive (∞,1)-topos with infinitesimal shape modality write for any object
for the full sub-(∞,1)-category of that of pointed objects over , def. , on those that are in the kernel of .
The construction in has the interpretation as the category of generalized formal moduli problems parameterized over . 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 -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 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 is
then the right adjoint exists
(LurieQC, prop. 2.5.12, LurieProper, proposition 2.5.12)
The projection formula in the dual form
for quasi-compact and quasi-separated appears as (LurieProper, remark 1.3.14).
Now if all the conditions on hold, so that , then passing to opposite categories exchanges the roles of and , makes the projection formula be as in the above discussion and hence yields a Wirthmüller context.
The existence of dualizing modules
is discussed in (Lurie, Representability theorems, section 4.2.)
For a finite group, , consider the spectral Mackey functors on the category of finite -sets. These are genuine G-spectra (see equivariant stable homotopy theory) which together constitute a -equivariant -category (or --category, see Parametrized Higher Category Theory and Higher Algebra). This sends any orbit , for a subgroup of , to the monoidal -category of genuine -spectra.
This forms an indexend monoidal -category, as do other instances of -categories of -spectra, for an orbital -category.
We discuss here structures (constructions) that may be defined and studied within an indexed monoidal -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 which interprets the given linear type theory and a cartesian monoidal category .
If there is only the strong monoidal functor without possibly a right adjoint , 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 is the linear type theory over the trivial context of a dependent linear type theory (indexed closed monoidal category) with category of contexts being :
(In the typical kind of model this means to assign to a space 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 in prop. is a special case of a general construction of secondary integral transforms in an indexed monoidal -category.
This suggests the following definition.
Given an indexed monoidal -category such that the functor from prop. has a strong monoidal right adjoint
we refer to the comonad of the -adjunction
as the exponential modality in the conjectural linear type theory over the point whose semantics is .
The condition in def. that (and its relative/dependent versions) has a right adjoint 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 a closed monoidal category with unit object 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 -category, linear negation, def. , intertwines dependent sum and dependent product:
For proof see here at Wirthmüller context.
Given an indexed monoidal -category , and given objects of then a linear polynomial functor
is a functor of the form
for a diagram in of the form
If here then this diagram is a correspondence
and the resulting 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 on a morphism in is
a choice of dualizable object (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, , and when dependent sum and dependent product are naturally equivalent for all objects, . In this case the two adjoints to 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 , def. , induces for all dualizable a natural equivalence
This is the “Wirthmüller isomorphism”.
For a twisted fiberwise fundamental class and for dualizable, write
for the composite of the linear dual of the -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 morphism between their pullbacks to the correspondence space:
Given
a correspondence as in def. ;
an integral kernel as in def. ;
we say that the induced secondary integral transform is the morphism
which is the dual (the image under ) 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 may be thought of as a space of “paths” or “trajectories” that connect points in to points in . From this point of view definition is a linear map that takes functions on to functions on 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 are pronounced as possibility and necessity, the monad 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
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 -category are in
Last revised on April 8, 2024 at 15:47:09. See the history of this page for a list of all contributions to it.