ifc-0047

3.4.1 The proposed internal DIAL target

3.4.1 The proposed internal DIAL target

The preceding ingredients do not yet define an internal double object. The classical Weil criterion states what smooth compatibility must recover; the tensor-sketch construction suggests how two presentations may interact; and the homotopy coordinates describe one classical realization. The following definition packages these demands as a research target.

Definition 3.3 Candidate DIAL object, proposed

Let \((\mathcal M,T)\) be a tangent category with the differential bundles and pullbacks needed below. A candidate Double Involution ALgebroid (DIAL) is a square of differential bundles in \(\mathcal M\), equipped with horizontal and vertical involution-algebroid structures, a declared dualizability doctrine, and an interchange comparison whose smooth finite-rank realization is Mackenzie’s double-Lie compatibility datum. We reserve the name DIAL object for a candidate whose comparison satisfies the required coherence equations. Until the missing duality and coherence theory is completed, this is a target definition rather than a claim of an established category of such objects.

Write \(\Theta _{\mathrm{int}}\) for the typed failure of this internal interchange comparison. This notation is deliberately schematic: a full theory must specify the precise 2-cells, pullback hypotheses, and coherence laws. The intended adequacy conditions are:

  1. in finite-rank \(\mathbf{Smooth}\), the construction recovers Mackenzie’s classical double Lie algebroids, not merely two VB-algebroid structures on a common square;

  2. tangent prolongation is represented internally;

  3. the vacant case recovers matched pairs, while the cotangent case recovers the double associated with a Lie bialgebroid;

  4. a suitable cochain realization \(\mathsf{Real}\) sends the internal defect to the graded commutator

    \[ \mathsf{Real}(\Theta _{\mathrm{int}}) = [d_{\mathrm{asm}},d_{\mathrm{acc}}]_{\mathrm{gr}} =:\Omega _{\mathrm{cre}}; \]

  5. the construction is stable under the transports used for finite sketch extension;

  6. its dualizability assumptions, or its replacement for double-vector- bundle duality, are explicit; and

  7. every admissible splitting yields a matched pair of 2-term representations up to homotopy, and compatibility is independent of that auxiliary splitting.

. The first-order tangent-category–Lie-algebroid bridge is established. The double internalization and the realization \(\mathsf{Real}(\Theta _{\mathrm{int}})=\Omega _{\mathrm{cre}}\) are proposed bridge requirements for this research program. Meinrenken–Pike prove the super-commutation criterion in classical double Lie geometry; they do not prove its internalization in an arbitrary tangent category or smooth topos. Mackenzie supplies the classical compatibility target and its major special cases, but not the proposed tangent-categorical DIAL semantics.