Tambara Module

definition theorem example program

A Tambara module on a Monoidal Category $(\mathcal{C},\otimes ,I)$ (originally: cartesian, $\otimes =\times$) is a Profunctor $P$ equipped with a family of maps

$${\alpha }_{⟨a,b⟩,c}:P⟨a,b⟩\to P⟨c\otimes a,c\otimes b⟩,$$

natural in $a,b$ and dinatural in $c$ (since $c$ appears both co- and contravariantly), preserving the monoidal structure: ${\alpha }_{⟨a,b⟩,I}=\mathrm{id}$ and ${\alpha }_{⟨a,b⟩,c^{\prime }\otimes c}\cong {\alpha }_{⟨c\otimes a,c\otimes b⟩,c^{\prime }}\circ {\alpha }_{⟨a,b⟩,c}$. Morphisms of Tambara modules are natural transformations $\rho :P\to Q$ commuting with the $\alpha$‘s; they form the Tambara category $\mathcal{T}$. In Haskell (cartesian case, class Strong/Cartesian):

class Profunctor p => Cartesian p where
  alpha :: p a b -> p (c, a) (c, b)      -- parametricity supplies all the (di)naturality

Sources: DaoFP Chapter 18 (“Tambara Modules”: §18.2 “Profunctor Lenses”: “Profunctors and lenses”, “Tambara module”, “Profunctor lenses”, “Profunctor lenses in Haskell”; §18.3 “General Optics”; §18.4 “Mixed Optics”), Exercises 18.2.1, 18.4.1; §17.8 (Arrows = pre-arrows that are Tambara modules).

Why they matter. To turn the Existential Lens ${\int }^c\mathcal{C}(s,c\times a)\times \mathcal{C}(c\times b,t)$ into a representation “map $P⟨a,b⟩$ to $P⟨s,t⟩$”, one can lift $⟨f,g⟩$ by $P⟨f,g⟩:P⟨c\times a,c\times b⟩\to P⟨s,t⟩$ — but first needs $P⟨a,b⟩\to P⟨c\times a,c\times b⟩$. That missing map is the Tambara structure.

Comonad/monad picture. $(\Theta P)⟨a,b⟩:={\int }_{c}P⟨c\times a,c\times b⟩$ is a Comonad on profunctors ($\epsilon$ projects at $c=1$), and Tambara modules are exactly its comonad coalgebras (a coalgebra $P\to \Theta P$ is, by continuity of hom, a dinatural family $\alpha$). Its left adjoint is the Monad

$$(\Phi P)⟨s,t⟩={\int }^{u,v,c}\mathcal{C}(s,c\times u)\times \mathcal{C}(c\times v,t)\times P⟨u,v⟩,$$

with $[{\mathcal{C}}^{\mathrm{op}}\times \mathcal{C},\mathbf{Set}](\Phi P,Q)\cong [\dots ](P,\Theta Q)$; so the Tambara category is the Eilenberg-Moore Category of $\Phi$, giving the free/forgetful adjunction needed for Tannakian Reconstruction. Evaluating $\Phi$ on the representable $({\mathcal{C}}^{\mathrm{op}}\times \mathcal{C})(⟨a,b⟩,-)$ and applying co-Yoneda returns exactly the existential lens — hence Profunctor Optics.

• Generalizations: for $\otimes =+$ the Tambara modules are Cocartesian/Choice (alpha' :: p a b -> p (Either c a) (Either c b)) and the optics are prisms; for the action $c\bullet a={\sum }_m{c}_m\times a^m$ of the Day-monoidal category $[\mathbb{N},\mathcal{C}]$ they give traversals; any action of a monoidal category $\mathcal{M}$ on $\mathcal{C}$ (an actegory), or two actions on $\mathcal{C}$ and $\mathcal{D}$, gives mixed optics ${\int }^m\mathcal{C}(s,m\bullet a)\times \mathcal{D}(m\bullet b,t)$ (DaoFP Exercise 18.4.1).
• Haskell’s Arrow is a Prearrow that is also a Tambara module (first).

JuliaLeanHaskell

Docs: plain Julia — Catlab has no dedicated API for this; related: Catlab v0.16 docs · GATlab standard library

# a Tambara structure on the function profunctor (->): alpha f = (c, a) -> (c, f(a))
alpha(f) = ((c, a),) -> (c, f(a))
alpha(x -> x + 1)((:tag, 41))          # (:tag, 42)
# on the "get/set" profunctor FlipLens a b s t = (s -> a, s -> b -> t):
alpha_lens((get, set)) = (((c, s),) -> get(s), ((c, s), b) -> (c, set(s, b)))

import Mathlib
-- Tambara modules as a structure on Type-valued profunctors (cartesian case)
structure Tambara (p : Type → Type → Type) where
  dimap : (s → a) → (b → t) → p a b → p s t
  alpha : p a b → p (c × a) (c × b)
def tambaraFun : Tambara (fun a b => a → b) :=
  { dimap := fun f g h => g ∘ h ∘ f, alpha := fun h ⟨c, a⟩ => (c, h a) }

class Profunctor p where
  dimap :: (s -> a) -> (b -> t) -> p a b -> p s t
class Profunctor p => Cartesian p where           -- Tambara modules for (×); library name: Strong
  alpha :: p a b -> p (c, a) (c, b)
class Profunctor p => Cocartesian p where         -- Tambara modules for (+); library name: Choice
  alpha' :: p a b -> p (Either c a) (Either c b)
 
instance Profunctor (->) where dimap f g h = g . h . f
instance Cartesian (->) where alpha h (c, a) = (c, h a)
instance Cocartesian (->) where alpha' h = fmap h    -- Either c is a functor