Categorical and algebraic aspects of the intuitionistic modal logic IEL― and its predicate extensions

The system of intuitionistic modal logic $\textbf{IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic (S. Artemov and T. Protopopescu. Intuitionistic epistemic logic. The Review of Symbolic Logic, 9, 266–298, 2016). We construct the modal lambda calculus, which is Curry–Howard isomorphic to $\textbf{IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming.We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a Cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operators. Such operators are used in point-free topology as well. We study complete Kripke–Joyal-style semantics for predicate extensions of $\textbf{IEL}^{-}$ and related logics using Dedekind–MacNeille completions and modal cover systems introduced by Goldblatt (R. Goldblatt. Cover semantics for quantified lax logic. Journal of Logic and Computation, 21, 1035–1063, 2011). The paper extends the conference paper published in the LFCS’20 volume (D. Rogozin. Modal type theory based on the intuitionistic modal logic IEL. In International Symposium on Logical Foundations of Computer Science, pp. 236–248. Springer, 2020).

Freely adjoining monoidal duals

Given a monoidal category $\mathcal C$ with an object J, we construct a monoidal category $\mathcal C[{J^ \vee }]$ by freely adjoining a right dual ${J^ \vee }$ to J. We show that the canonical strong monoidal functor $\Omega :\mathcal C \to \mathcal C[{J^ \vee }]$ provides the unit for a biadjunction with the forgetful 2-functor from the 2-category of monoidal categories with a distinguished dual pair to the 2-category of monoidal categories with a distinguished object. We show that $\Omega :\mathcal C \to \mathcal C[{J^ \vee }]$ is fully faithful and provide coend formulas for homs of the form $\mathcal C[{J^ \vee }](U,\,\Omega A)$ and $\mathcal C[{J^ \vee }](\Omega A,U)$ for $A \in \mathcal C$ and $U \in \mathcal C[{J^ \vee }]$ . If ${\rm{N}}$ denotes the free strict monoidal category on a single generating object 1, then ${\rm{N[}}{{\rm{1}}^ \vee }{\rm{]}}$ is the free monoidal category Dpr containing a dual pair – ˧ + of objects. As we have the monoidal pseudopushout $\mathcal C[{J^ \vee }] \simeq {\rm{Dpr}}{{\rm{ + }}_{\rm{N}}}\mathcal C$ , it is of interest to have an explicit model of Dpr: we provide both geometric and combinatorial models. We show that the (algebraist’s) simplicial category Δ is a monoidal full subcategory of Dpr and explain the relationship with the free 2-category Adj containing an adjunction. We describe a generalization of Dpr which includes, for example, a combinatorial model Dseq for the free monoidal category containing a duality sequence X0 ˧ X1 ˧ X2 ˧ … of objects. Actually, Dpr is a monoidal full subcategory of Dseq.

On the Frobenius functor for symmetric tensor categories in positive characteristic

We develop a theory of Frobenius functors for symmetric tensor categories (STC) {\mathcal{C}} over a field {\boldsymbol{k}} of characteristic p, and give its applications to classification of such categories. Namely, we define a twisted-linear symmetric monoidal functor {F:\mathcal{C}\to\mathcal{C}\boxtimes{\rm Ver}_{p}}, where {{\rm Ver}_{p}} is the Verlinde category (the semisimplification of {\mathop{\mathrm{Rep}}\nolimits_{\mathbf{k}}(\mathbb{Z}/p)}); a similar construction of the underlying additive functor appeared independently in [K. Coulembier, Tannakian categories in positive characteristic, preprint 2019]. This generalizes the usual Frobenius twist functor in modular representation theory and also the one defined in [V. Ostrik, On symmetric fusion categories in positive characteristic, Selecta Math. (N.S.) 26 2020, 3, Paper No. 36], where it is used to show that if {\mathcal{C}} is finite and semisimple, then it admits a fiber functor to {{\rm Ver}_{p}}. The main new feature is that when {\mathcal{C}} is not semisimple, F need not be left or right exact, and in fact this lack of exactness is the main obstruction to the existence of a fiber functor {\mathcal{C}\to{\rm Ver}_{p}}. We show, however, that there is a 6-periodic long exact sequence which is a replacement for the exactness of F, and use it to show that for categories with finitely many simple objects F does not increase the Frobenius–Perron dimension. We also define the notion of a Frobenius exact category, which is a STC on which F is exact, and define the canonical maximal Frobenius exact subcategory {\mathcal{C}_{\rm ex}} inside any STC {\mathcal{C}} with finitely many simple objects. Namely, this is the subcategory of all objects whose Frobenius–Perron dimension is preserved by F. One of our main results is that a finite STC is Frobenius exact if and only if it admits a (necessarily unique) fiber functor to {{\rm Ver}_{p}}. This is the strongest currently available characteristic p version of Deligne’s theorem (stating that a STC of moderate growth in characteristic zero is the representation category of a supergroup). We also show that a sufficiently large power of F lands in {\mathcal{C}_{\rm ex}}. Also, in characteristic 2 we introduce a slightly weaker notion of an almost Frobenius exact category (namely, one having a fiber functor into the category of representations of the triangular Hopf algebra {\boldsymbol{k}[d]/d^{2}} with d primitive and R-matrix {R=1\otimes 1+d\otimes d}), and show that a STC with Chevalley property is (almost) Frobenius exact. Finally, as a by-product, we resolve Question 2.15 of [P. Etingof and S. Gelaki, Exact sequences of tensor categories with respect to a module category, Adv. Math. 308 2017, 1187–1208].

Functoriality of Khovanov homology

In this paper, we prove that every Khovanov homology associated to a Frobenius algebra of rank 2 can be modified in such a way as to produce a TQFT on oriented links, that is a monoidal functor from the category of cobordisms of oriented links to the homotopy category of complexes.

Virtual tangles and fiber functors

We define a category [Formula: see text] of tangles diagrams drawn on surfaces with boundaries. On the one hand, we show that there is a natural functor from the category of virtual tangles to [Formula: see text] which induces an equivalence of categories. On the other hand, we show that [Formula: see text] is universal among ribbon categories equipped with a strong monoidal functor to a symmetric monoidal category. This is a generalization of the Shum–Reshetikhin–Turaev theorem characterizing the category of ordinary tangles as the free ribbon category. This gives a straightforward proof that all quantum invariants of links extend to framed oriented virtual links. This also provides a clear explanation of the relation between virtual tangles and Etingof–Kazhdan formalism suggested by Bar-Natan. We prove a similar statement for virtual braids, and discuss the relation between our category and knotted trivalent graphs.

Monoidal Categories Enriched in Braided Monoidal Categories

We introduce the notion of a monoidal category enriched in a braided monoidal category $\mathcal{V}$. We set up the basic theory, and prove a classification result in terms of braided oplax monoidal functors to the Drinfeld centre of some monoidal category $\mathcal{T}$. Even the basic theory is interesting; it shares many characteristics with the theory of monoidal categories enriched in a symmetric monoidal category, but lacks some features. Of particular note, there is no cartesian product of braided-enriched categories, and the natural transformations do not form a 2-category, but rather satisfy a braided interchange relation. Strikingly, our classification is slightly more general than what one might have anticipated in terms of strong monoidal functors $\mathcal{V}\to Z(\mathcal{T})$. We would like to understand this further; in a future article, we show that the functor is strong if and only if the enriched category is ‘complete’ in a certain sense. Nevertheless it remains to understand what non-complete enriched categories may look like. One should think of our construction as a generalization of de-equivariantization, which takes a strong monoidal functor ${\mathsf {Rep}}(G) \to Z(\mathcal{T})$ for some finite group $G$ and a monoidal category $\mathcal{T}$, and produces a new monoidal category $\mathcal{T} _{{/\hspace{-2px}/}G}$. In our setting, given any braided oplax monoidal functor $\mathcal{V} \to Z(\mathcal{T})$, for any braided $\mathcal{V}$, we produce $\mathcal{T} _{{/\hspace{-2px}/}\mathcal{V}}$: this is not usually an ‘honest’ monoidal category, but is instead $\mathcal{V}$-enriched. If $\mathcal{V}$ has a braided lax monoidal functor to ${\mathsf {Vec}}$, we can use this to reduce the enrichment to ${\mathsf {Vec}}$, and this recovers de-equivariantization as a special case. This is the published version of arXiv:1701.00567.

Coherence for monoidal monads and comonads

The goal of this paper is to prove coherence results with respect to relational graphs for monoidal monads and comonads, that is, monads and comonads in a monoidal category such that the endofunctor of the monad or comonad is a monoidal functor (this means that it preserves the monoidal structure up to a natural transformation that need not be an isomorphism). These results are proved first in the absence of symmetry in the monoidal structure, and then with this symmetry. The monoidal structure is also allowed to be given with finite products or finite coproducts. Monoidal comonads with finite products axiomatise a plausible notion of equality of deductions in a fragment of the modal logic S4.

The Diagrammatic Soergel Category andsl(N)-Foams, forN≥4

For eachN≥4, we define a monoidal functor from Elias and Khovanov's diagrammatic version of Soergel's category of bimodules to the category ofsl(N)foams defined by Mackaay, Stošić, and Vaz. We show that through these functors Soergel's category can be obtained from thesl(N)foams.

Elementary remarks on units in monoidal categories

We explore an alternative definition of unit in a monoidal category originally due to Saavedra: a Saavedra unit is a cancellable idempotent (in a 1-categorical sense). This notion is more economical than the usual notion in terms of left-right constraints, and is motivated by higher category theory. To start, we describe the semi-monoidal category of all possible unit structures on a given semi-monoidal category and observe that it is contractible (if non-empty). Then we prove that the two notions of units are equivalent in a strong functorial sense. Next, it is shown that the unit compatibility condition for a (strong) monoidal functor is precisely the condition for the functor to lift to the categories of units, and it is explained how the notion of Saavedra unit naturally leads to the equivalent non-algebraic notion of fair monoidal category, where the contractible multitude of units is considered as a whole instead of choosing one unit. To finish, the lax version of the unit comparison is considered. The paper is self-contained. All arguments are elementary, some of them of a certain beauty.