By a bireflective subcategory one might mean:
A subcategory $\iota \,\colon\, \mathcal{C} \hookrightarrow \mathcal{B}$ which is both reflective and coreflective — i.e. a fully faithful functor possessing both left and right adjoints: $L \dashv \iota \dashv R$ (reflective localization and coreflective localization).
Such subcategories are called essential localizations by Kelly & Lawvere (1989), following the terminology of essential geometric morphisms from topos theory, see also at level of a topos.
The adjoint pair $\iota \circ L \dashv \iota \circ R$ is then an adjoint modality; see there for more.
More specifically, one may in addition ask that $L \simeq R$, hence that the subcategory inclusion $\iota$ has an ambidextrous adjoint $\beta \dashv \iota \dashv \beta$.
Such subcategories are called quintessential localizations by Johnstone (1996).
The corresponding (co-)monad $\natural \coloneqq \iota \circ \beta$ is then a Frobenius monad (see at classical modality).
Finally, one may moreover ask that the points-to-pieces transform $\natural \overset{\epsilon}{\longrightarrow} id \overset{\eta}{\longrightarrow} \natural$ of a quintessential localization be the identity morphisms.
This strong form of the notion is the case actually called bireflective subcategories by Freyd et al. (1999).
A full subcategory-inclusion
is bireflective in the sense of FOPTST99, Def. 8 iff
(1.) the inclusion has an ambidextrous adjoint
(2.) such that for all $E \in \mathcal{B}$ the counit of the right adjunction followed by the unit of the left adjunction (the points-to-pieces transform) equals the identity:
The first clause in Def. does not in general by itself enforce the second clause. A counter-example is given in FOPTST99, Rem. 12.
However, the second clause does follow automatically when $\mathcal{B}$ is a Cauchy-complete category (Johnstone (1996)).
In the other direction, the second clause in Def. implies that
is an idempotent natural endomorphism, exhibited as a split idempotent.
Given a category $\mathcal{B}$, its bireflective subcategories (Def. ) are in correspondence with the split idempotent natural endomorphisms on $id_\mathcal{B}$ with specified splitting, i.e.
with
Concretely, from a split idempotent on $id_{\mathcal{B}}$ we recover the Frobenius monad $\natural$ as follows:
Given a split idempotent transformation as in Prop. we have for all $E \,\in\, \mathcal{B}$
By naturality of the transformation $\eta$
and using (1) we get the first statement:
The second follows analogously.
Given a split idempotent transformation as in Prop. , $\natural \colon \mathcal{B} \to \mathcal{B}$ becomes
an idempotent monad $(\natural, \eta, \mu)$ by setting
an idempotent comonad $(\natural, \epsilon, \delta)$ by setting
For the associativity of the monoid product we need to show the commutativity of
By functoriality of $\natural$ this follows from the commutativity of
which holds by naturality of $\epsilon$.
The other claims follow similarly.
A modal type theory for bireflection modalities has been proposed in Riley, Finster & Licata (2021), Riley (2022).
We show the inference rules which these authors propose to add to plain intuitionistic type theory for encoding the presence of a bireflection classical modality $\natural$ on the type system, and we show corresponding categorical semantics via commuting diagrams in an interpreting locally cartesian closed category (a more syntactic semantics is indicated in RFL21, Sec. 7, esp. Fig. 6).
Given a bireflection $\natural \colon \mathcal{B} \to \mathcal{B}$ as above, then for $\Gamma \in \mathcal{B}$ we obtain a monad on the slice category, to be denoted
by setting
Beware of some non-obvious properties of the following type-theoretic syntax:
There is an asymmetry in the meaning of $\underline{(-)}$:
An underline of a context denotes application of $\natural$, but an underline of a type in context only means its pullback along the counit $\epsilon^{\natural}$. The idea is that underlines indicate dependency on $\natural$-modal variables, to be distinguished of a type itself being $\natural$-modal or not.
The syntactic symbol “$\natural$” is not exactly interpreted as the bireflective monad of that name. Rather:
An unadorned “$\natural$” in the syntax interprets, in context $\Gamma$, as the relative monad
The combination $\natural \underline{(-)}$ is what actually interprets as $\natural_\Gamma$ (2).
This transpires syntactically in RFL21, Cor. 2.14; Riley22, Cor. 1.1.16, and semantically in (3) below.
The list of inference rules and their categorical semantics (first the axioms then derived rules):
Using these ingredients, one finds that the function $a \,\mapsto\, \underline{a}^\natural$ is interpreted simply as postcomposition with the $\eta^{\natural}$-naturality square:
With this, one finds the following rule for $\natural$ respecting dependent pair types:
Using this one finds that every type $A$ is the dependent sum type of its fiber linear types $A_{\underline{x}}$ (NB: we show 1-categorical semantics, interpreting identification types as diagonal morphisms):
(spaces among retractive spaces)
Let $\mathcal{B}$ be the category of retractive topological spaces (or just of Sets), i.e. the category of diagrams in Top (Set) of the form $B \xrightarrow{i} E \xrightarrow{p} B$ such that $p \circ i \,=\, id_B$. Then the functor
is a bireflective subcategory inlusion (Def. ) with ambidextrous adjoint given by
(zero-vector bundles among all vector bundles)
For any ground field, let $\mathcal{B} \coloneqq Vect_{Set} \coloneqq \int_{S \in Set} Vect S$ be the category VectBund of vector bundles over Sets, hence of indexed vector spaces. Then the functor
which sends any set $S$ to the zero vector bundle $S \times \{0\}$ over $S$ is a bireflective subcategory in the sense of Def. .
(zero-spectrum bundles among all parameterized spectra)
Let $T Grpd_\infty$ denote the $\infty$-category of parameterized spectra over varying $\infty$-groupoids (the tangent $\infty$-category of $Grpd_\infty$). Then the inclusion
given by sending $X \in Grpd_\infty$ to the zero-spectrum bundle over $X$ ought to count as a “bireflective sub-$\infty$-category” (cf. here at infinitesimal cohesion).
A model category-presentation of this situation by a (left and right) Quillen functor to a model structure for parameterized spectra underlying which is a bireflective sub-1-category inclusion (Def. ) may be recognized in Hebestreit, Sagave & Schlichtkrull (2020), Lem. 3.19, there incarnated as the canonical inclusion
of $\mathcal{I}$-spaces into symmetric spectra internal to retractive spaces (Exp. ).
An analogous statement is in Braunack-Mayer (2019), Cor. 2.45.
On subcategory inclusion which have both a left and a right adjoint (essential localizations):
On subcategory inclusions with ambidextrous adjoints (quintessential localizations):
On subcategory inclusions with ambidextrous adjoints whose points-to-pieces transform is the identity (actual bireflective subcategories):
Discussion of a modal type theory for bireflective modalities, in a context of linear homotopy type theory:
Mitchell Riley, Eric Finster, Daniel R. Licata, Section 7.1 in: Synthetic Spectra via a Monadic and Comonadic Modality [arXiv:2102.04099]
Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [doi:10.14418/wes01.3.139, ir:3269, pdf]
Last revised on April 17, 2023 at 11:16:58. See the history of this page for a list of all contributions to it.