ifc-0046

3.4 Tensor products of sketches as a semantics for doubling

MacAdam points to a second route across the missing bridge, one that connects the double geometry directly to the theory-building language of this book [ MacAdam , 2023 ] . In a closed monoidal doctrine of limit sketches in which the required tensor and internal model categories exist, tensor-product semantics gives equivalences

\[ \operatorname {Mod}\! \bigl(\mathbb A, \operatorname {Mod}(\mathbb B,\mathbf{Set})\bigr) \simeq \operatorname {Mod}(\mathbb A\otimes \mathbb B,\mathbf{Set}) \simeq \operatorname {Mod}\! \bigl(\mathbb B, \operatorname {Mod}(\mathbb A,\mathbf{Set})\bigr). \]

The middle sketch contains both presentations. Its models preserve the distinguished limits in either coordinate, and its commuting squares encode interchange between the two structures. In this sense an $\mathbb A$-structure internal to $\mathbb B$-models can be uncurried into one model of a tensor-product theory and curried again in the opposite order.

Let $\mathbb I_{\mathrm{Lie}}$ denote the proposed enriched limit sketch, or classifying tangent-categorical theory, for an involution algebroid. The candidate presentation

\[ \mathbb D_{\mathrm{inv}} := \mathbb I_{\mathrm{Lie}}\otimes \mathbb I_{\mathrm{Lie}} \]

is therefore a natural syntactic target for DIAL. A model would be an involution-algebroid structure internal to involution-algebroid models, with the tensor-product squares recording horizontal–vertical interchange. More generally, $\mathbb I_{\mathrm{Lie}}\otimes \mathbb V$ is the corresponding candidate presentation for a vector-bundle object in involution algebroids, the tangent-categorical analogue suggested by VB–Lie algebroids. These formulas are a research construction, not a theorem that ordinary unenriched finite-limit sketches already encode every tangent, smooth, duality, and bracket requirement. The relevant tensor product must live in the enriched sketch doctrine appropriate to tangent categories.

This viewpoint explains why the two DIAL directions should not be assembled as an arbitrary pair of learners. They are two models of declared theories, and their interaction is itself presented. It also provides a formal version of order-independence. Under the tensor-product theorem for the selected limit-sketch doctrine, exchanging the two factors gives the semantic symmetry

\[ \operatorname {Mod}(\mathbb A,\operatorname {Mod}(\mathbb B,-)) \simeq \operatorname {Mod}(\mathbb B,\operatorname {Mod}(\mathbb A,-)). \]

MacAdam observes that Mackenzie’s symmetry of partial Lie derivatives should become immediate from this perspective: for a double Lie groupoid, applying the Lie functor in the two orders produces canonically corresponding double infinitesimal structures [ Mackenzie , 2000b , MacAdam , 2023 ] .

Sketch semantics for double involution. The two outer expressions denote the horizontal-first and vertical-first iterated model categories. They read one tensor-product model in opposite orders. Establishing the appropriate enriched doctrine and its classical realization is part… — Figure 3.1 Sketch semantics for double involution. The two outer expressions denote the horizontal-first and vertical-first iterated model categories. They read one tensor-product model in opposite orders. Establishing the appropriate enriched doctrine and its classical realization is part of the DIAL program.

The construction suggests a precise separation of three questions:

presentation: does $\mathbb I_{\mathrm{Lie}}\otimes \mathbb I_{\mathrm{Lie}}$ carry the required side and interchange axioms in an enriched tangent doctrine?
realization: are its finite-rank smooth models equivalent to Mackenzie double Lie algebroids, including the required duality rather than merely two internal algebroid structures?
integration: when does such a smooth infinitesimal model arise from a double Lie groupoid?

Only the first question is formal sketch semantics. Even an ordinary Lie algebroid need not integrate to a Lie groupoid: integrability is controlled by global monodromy obstructions [ Crainic and Fernandes , 2003 ] . In the double setting, sidewise integrability is necessary but is not by itself a proof that the integrations assemble into a smooth double groupoid; compatible integration is a further global obligation [ Stefanini , 2009 ] .

. Tensor-product symmetry is a semantics of order independence; it is not an integrability theorem. It can explain why two already defined partial Lie constructions agree, and it can present the compatibility law to be tested. It does not remove monodromy, smoothness, source-simply-connectedness, or double-integration obstructions. DIAL must report these as separate admission conditions whenever local repair fields are interpreted as finite creative trajectories.

For synthetic creativity, sketches now have two roles at different scales. The tensor product presents the local two-direction repair calculus. The finite map $J:\mathbb S\to \mathbb S^+$ presents a proposed change in the domain theory.

The passage between those scales has three gates. First, failure of a typed interchange equation localizes mixed generators that may require repair. Second, a finite-realization test distinguishes a formal infinitesimal direction from a coherent transition. Third, an admitted transition may support construction or selection of $\mathbb S^+$. This sequence joins the geometry of this chapter to the algebraic-theory targets of Chapter 5 without identifying local compatibility with global creative success.

Homotopy coordinates.

Gracia-Saz, Jotz Lean, Mackenzie, and Mehta give a third, computationally useful characterization [ Gracia-Saz et al. , 2014 ] . Choose a linear splitting $\Sigma $ of a classical double vector bundle with side bundles $A,B$ and core $C$. The two VB-algebroid structures induce:

\[ \begin{aligned} & \text{an $A$-2-representation on }\partial _B:C\to B,\\ & \text{a $B$-2-representation on }\partial _A:C\to A. \end{aligned} \]

For the chosen splitting, their Theorem 3.4 states that the original structure is a double Lie algebroid if and only if these two 2-term representations up to homotopy form a matched pair [ Gracia-Saz et al. , 2014 , Theorem 3.4 ] . The matched-pair condition expands into nine compatibility equations involving anchors, boundary maps, connections, and curvature.

For a chosen splitting, write

\[ r_{\Sigma }^{\mathrm{DIAL}} = \bigl(r_{\Sigma }^{(1)},\ldots ,r_{\Sigma }^{(9)}\bigr) \]

for the left-minus-right residuals of those equations. Its vanishing is equivalent to classical double-Lie compatibility. The coordinates depend on $\Sigma $, but the vanishing claim does not. A change of splitting therefore acts like a change of gauge: an empirical DIAL diagnostic must either be invariant under that change or report its dependence explicitly.

. Representation up to homotopy does not mean that an arbitrary interchange failure is acceptable. Curvature is retained coherently inside the two 2-term representations, but the pair must still satisfy all matched- pair conditions. Homotopy enriches the internal coordinates of compatibility; it does not replace admission by an unconstrained tolerance.