Identifying the actual coordinate projections with factor projections #
The remaining-state unitaries intertwine insertion on State with insertion
on the two-factor carrier. Taking adjoints identifies the projections, and
their product is the operator generated by actual double insertion.
theorem
LiebThirring.pairCurrying_oneParticleProjection_left
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume))
(ψ : State N q)
:
(pairCurryingLinearIsometryEquiv i j hij) ((oneParticleProjection i f) ψ) = (firstFactorProjection f) ((pairCurryingLinearIsometryEquiv i j hij) ψ)
Pair currying identifies the first actual coordinate projection with the first generic factor projection.
theorem
LiebThirring.pairCurrying_oneParticleProjection_right
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume))
(ψ : State N q)
:
(pairCurryingLinearIsometryEquiv i j hij) ((oneParticleProjection j f) ψ) = (secondFactorProjection f) ((pairCurryingLinearIsometryEquiv i j hij) ψ)
Pair currying identifies the second actual coordinate projection with the second generic factor projection.
theorem
LiebThirring.pairCurrying_doubleParticleInsertion_projection
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume))
(ψ : State N q)
:
(pairCurryingLinearIsometryEquiv i j hij)
((doubleParticleInsertion i j hij f ∘SL ContinuousLinearMap.adjoint (doubleParticleInsertion i j hij f)) ψ) = (doubleFactorInsertion f ∘SL ContinuousLinearMap.adjoint (doubleFactorInsertion f))
((pairCurryingLinearIsometryEquiv i j hij) ψ)
Pair currying also transports the operator generated by double insertion.
theorem
LiebThirring.oneParticleProjection_comp_oneParticleProjection
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume))
:
oneParticleProjection i f ∘SL oneParticleProjection j f = doubleParticleInsertion i j hij f ∘SL ContinuousLinearMap.adjoint (doubleParticleInsertion i j hij f)
The product of two distinct coordinate projections is generated by actual double insertion. No unit-vector hypothesis is needed for this identity.