Nottingham FP Lab Blog

Bart Jacobs’ question (FP lunch 19/1/07)

by Thorsten on January 21, 2007.
Tagged as: Lunches.

Recently, Bart Jacob’s asked me a question about containers: He is looking for a formula for the derivative of a quotient container. I sketched a possible answer (I haven’t yet checked the details) and used this opportunity to give a quick introduction to containers.

A container is given by a set $S\in *$ of shapes and a family $P\in S\to *$ of position, giving rise to a functor
$F \in * \to *$ given by $F\,X = \Sigma s\in S.(P\, s)\to X$ . It’s derivative as a functor is
$F'\,X = \Sigma (s,p) \in (\Sigma s\in S.P\,s).(\Sigma q\in P\,s.p \not= q)\to X$ . A quotient container is specified by additionally
giving a family of subgroups $R\,s\subseteq Iso\,(P\,s)$ of the isomorphism group, it gives rise to a functor
$F\,X = \Sigma s\in S.((P\, s)\to X)/\sim$ where the equivalence relation is generated by $f \sim f\circ\phi$ for
$\phi\in R\,s$ . I believe that it’s derivative is given by extending the previous formula by additionally specifying
$R'\,(s,p)\subseteq Iso\,(\Sigma q\in P\,s.p \not= q)$ where $\phi\in R'\,(s,p)$ iff $\phi$ is given by restricting an isomorphim $\psi\in R\,s$ with the property $\psi\,p=p$ (by restricting I mean that $\phi \circ \pi_1 = \pi_1 \circ \psi$ ).