不動点のダブル・ダガー公式

ダブル・ダガー公式（不動点の対角性）は：

• (f^†)^† = ((A+Δ);f)^†

ダガー（不動点オペレータ）がトレースで定義されている状況で、これを示す。

まずは次の簡単な補題：

• Tr^X+X(f;Δ;(Δ+X)) = Tr^X(Tr^X(f;Δ);Δ)

   TrX+X(f;Δ;(Δ+X)) //↓バニッシング

=  TrX(TrX(f;Δ;(Δ+X))) //↓内側に右タイトニング

=  TrX(TrX(f;Δ);Δ)

（以下の図では、X1 = X2 = X）

それと、Δに余結合律が成立することに注意：

• Δ;(Δ+X) = Δ(X+Δ)

ダブル・ダガー公式は次の手順：

(f^†)^† = Tr(Tr(f;Δ);Δ) だが、補題から Tr(Tr(f;Δ);Δ) = Tr(f;Δ;(Δ+X))、余結合律を考慮すれば、(f^†)^† = Tr(f;Δ;(X+Δ))。Δをスライディングで移動させれば、Tr((A+Δ);f;Δ) = (A+Δ;f)^†、これが求める結果。