3.3 The missing bridge: from tangent semantics to double algebroids

There is a terminological and mathematical seam that must not be hidden. Leung’s \(\mathsf{Weil}_1^{\mathrm{tan}}\) and the Weil algebra later used for a double Lie algebroid are not the same construction. The former is a monoidal algebraic theory whose actions classify tangent structure. The latter is a bigraded cochain algebra

attached by Meinrenken and Pike to a classical double vector bundle. Its two differentials encode candidate horizontal and vertical VB-algebroid structures. Sharing the name Weil reflects a common infinitesimal lineage, not an identity between the two objects.

An established first-order bridge is available, but it is not an equivalence of theories. Under the tangent-category limits and negatives assumed by Burke and MacAdam, they define involution algebroids internally, and MacAdam develops their functorial semantics. In the ordinary smooth model, every classical Lie algebroid determines an involution algebroid. Conversely, an involution algebroid carries a Lie bracket on the sections of its underlying bundle; a suitable unit object supplies the Leibniz law [ Burke and MacAdam , 2019 , Sections 4.2.1–4.2.4 ] .

The smooth comparison is only an injection on objects, not an equivalence of the full categories [ Burke and MacAdam , 2019 , Sections 4.2.1–4.2.4 ] . The warranted relationships are therefore

which supplies ambient semantics for involution algebroids, while

The word involution hides an important coherence law. For an anchored bundle \(\pi :A\to M\), Burke and MacAdam replace a bracket on sections by an arrow \(\alpha \) on the prolongation \(A\times _{\rho ,T\pi }T(A)\). Writing \(\sigma =(p\pi _1,\alpha )\), their involution axiom gives \(\sigma ^2=1\), while their flip axiom can be written in the Yang–Baxter-style form

where \(c:T^2\Rightarrow T^2\) is the canonical tangent flip. Thus three infinitesimal rearrangements agree independently of which adjacent pair is resolved first. After passage to sections, this coherence induces a Lie bracket satisfying Jacobi. Jacobi is therefore not discarded; it is recovered from a section-free internal law that makes sense in a tangent category [ Burke and MacAdam , 2019 ] .

This has a distinguished precedent but requires a careful distinction. Drinfel’d related the classical Yang–Baxter equation for \(r\)-matrices to Hamiltonian Poisson–Lie structures and Lie bialgebras [ Drinfel’d , 1983 ] . Burke and MacAdam’s equation is instead a Yang–Baxter-style braid relation for an involution on a prolongation; it is not Drinfel’d’s classical \(r\)-matrix equation. The common geometric lesson is that a local algebraic law can encode order-independent composition before its familiar bracket-level identity is extracted.

For DIAL this yields a sharper architecture. Each of the horizontal and vertical directions must first satisfy its own Yang–Baxter-style flip law. Only then is it meaningful to impose the mixed interchange, matched-pair, or super-commutation condition between them. A failure internal to one side is a malformed repair process; a failure between two individually coherent sides is a genuinely double obstruction.

Mackenzie’s Notions of Double for Lie Algebroids is the closest classical precursor to the required second step [ Mackenzie , 2000a ] . It unifies several meanings of double: Drinfel’d and Manin-triple doubling, matched pairs, the cotangent double associated with a Lie bialgebroid, and categorical or iterated doubles such as \(T(TM)\). A double Lie algebroid is not merely a square carrying two unrelated Lie-algebroid structures. Mackenzie’s compatibility uses the duality theory of double vector bundles; it recovers the infinitesimal invariants of double Lie groupoids and specializes to matched pairs and Lie bialgebroids.

This precedent both guides and limits DIAL. Mackenzie observes that the compatibility equation should admit formulation in fairly general categories, but his construction depends crucially on finite-rank vector-bundle duality. An internal tangent-categorical theory must therefore reconstruct that duality, replace it with an appropriate internal comparison, or state explicitly the dualizability doctrine under which DIAL exists. No result cited here automatically performs that internalization. We therefore make the missing step explicit as a research hypothesis.