Cheat Sheet J - Verification

Pensieve header: Cheat Sheet $J$ Verification; continued pensieve://2013-04/.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2013-03"];
<< FreeLie.m;
tm[u_,v_,w_] := LieMorphism[⟨u⟩->⟨w⟩, ⟨v⟩->⟨w⟩];
CC[u_, γ_LieSeries] := LieMorphism[u -> Ad[γ][u]];RC[u_, γ_LieSeries, ub_][ser_] := StableApply[LieMorphism[⟨u⟩ -> Ad[γ][⟨ub⟩]], ser];
RC[u_, γ_LieSeries][ser_] := ser // RC[u, γ,⟨υ⟩] // LieMorphism[⟨υ⟩->⟨u⟩];
Print /@ {{t=⟨"t"⟩, u=⟨"u"⟩, v=⟨"v"⟩, w=⟨"w"⟩},
α = RandomLieSeries[{t,u,v}],
β = RandomLieSeries[{t,u,v}],
γ = RandomLieSeries[{t,u,v}]
};
$SeriesShowDegree=3; $SeriesCompareDegree = 6;

ad[u_, γ_LieSeries] := LieDerivation[u -> b[γ, u]];
ϵ /: (ϵ^2)=0;

Some preliminary testing

(α // RC[u,α] // CC[u,-α])≡α

The Definition of J

J[u_, γ_] := (∫_0^1)(div[u,γ // RC[u, s γ]] // CC[u, -s γ])\[DifferentialD]s

J[u,α][{4}]

The t equation

Print /@ {
0 -> {γ, γw =  γ // tm[u,v,w]},
1 -> (t1=J[w, γw] // RC[w, γw]),
2 -> (t2=J[u,γ] // tm[u,v,w] // RC[w, γw]),
3 -> (t3=J[v, γ // RC[u,γ]] // RC[v, γ // RC[u,γ]] // tm[u,v,w]),
4 -> t1≡t2+t3
};

The h equation

Print /@ {
1 -> (t1=J[u, BCH[α, β]]),
2 -> (t2=J[u,α]),
3 -> (t3=J[u,β//RC[u,α]]//CC[u,-α]),
4 -> t1≡t2+t3
};

The meaning(s) of RC

Print /@ {
1 -> α,
2 -> (t1=α // CC[u, γ] // RC[u, -γ]),
3 -> α≡t1
};

Print /@ {
1 -> α,
2 -> (t1= α // CC[u, γ // RC[u, γ]]),
3 -> (t2= α // RC[u, γ]),
4 -> t1≡t2
};

The cocycle condition for div

Print /@ {
0 -> {α, β},
1 -> (t1=div[u,α] // ad[u,β]),
2 -> (t2=div[u,β] // ad[u,α]),
3 -> (t3=div[u, b[α,β]]),
4 -> (t4=div[u, α//ad[u,β]]),
5 -> (t5=div[u, β//ad[u,α]]),
6 -> t1-t2≡t3+t4-t5
};

The differential of BCH

Print /@ {
1 -> (bch=BCH[u,v]),
2 -> ((BCH[u+ϵ t, v+ϵ w]-bch)/ϵ),
3 -> (t1=((BCH[u+ϵ t, v+ϵ w]-bch)/ϵ) // adSeries[((1-(E^(-ad)))/ad), bch]),
4 -> (t2=t // adSeries[((1-(E^(-ad)))/ad),u] // Ad[-v]),
5 -> (t3=w // adSeries[((1-(E^(-ad)))/ad),v])
};
t1 ≡ t2+t3

The differential of C

Print /@ {
0 -> {α, β, γ},
1 -> (t1=(((γ // CC[u, α+ϵ β]) - (γ // CC[u, α]) )/ϵ)),
2 -> (t2=γ // ad[u, adSeries[(((E^ad)-1)/ad),α][β] // RC[u, -α]] // CC[u, α]),
t1 ≡ t2
};

The differential of RC

Print /@ {
0 -> {α, β, γ},
1 -> (t1=(((γ // RC[u, α+ϵ β]) - (γ // RC[u, α]) )/ϵ)),
2 -> (t2=γ // RC[u, α] // ad[u, adSeries[((1-(E^(-ad)))/ad),α][β] // RC[u, α]]),
t1 ≡ t2
};

The differential of J

Print /@ {
0 -> {α, β},
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(s div[u, α // RC[u,s α] // ad[u, β//adSeries[((1-(E^(-s ad)))/(s ad)), α]//RC[u, s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(s div[u, α // RC[u,s α]] // ad[u, β//adSeries[((1-(E^(-s ad)))/(s ad)), α]//RC[u, s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
5 -> (t4=(∫_0^1)(div[u, b[α // RC[u,s α], β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3-t4
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
5 -> (t4=(∫_0^1)(div[u, b[α, β//adSeries[((1-(E^(-s ad)))/ad), α]]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3-t4
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
5 -> (t4=(∫_0^1)(div[u, β//adSeries[1-(E^(-s ad)), α]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3-t4
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[(E^(-s ad)), α]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1-t2+t3
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β//Ad[-s α]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=div[u, β//adSeries[((1-(E^(-ad)))/ad), α]//RC[u, α]] // CC[u,-α]),
t0 ≡ t1
};