Remaining-coordinate transport under particle exchange

The transposition between two particle labels bijects their complementary spatial and spin labels. This is the concrete unitary needed to compare one-particle contractions in different coordinates.

def LiebThirring.restExchangeIndexEquiv {N : ℕ} (i j : Fin N) : { k : Fin N // k ≠ i } ≃ { k : Fin N // k ≠ j }

Exchange bijects the indices complementary to its two distinguished labels.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LiebThirring.restExchangeSpatial {N : ℕ} (i j : Fin N) : OtherConfiguration j ≃ₗᵢ[ℝ] OtherConfiguration i

Spatial exchange on the remaining coordinates.

Equations

• LiebThirring.restExchangeSpatial i j = LinearIsometryEquiv.piLpCongrLeft 2 ℝ ℝ ((LiebThirring.restExchangeIndexEquiv i j).symm.prodCongr (Equiv.refl (Fin 3)))

def LiebThirring.restExchangeSpins {N q : ℕ} (i j : Fin N) : OtherSpinLabels i q ≃ OtherSpinLabels j q

Spin exchange on the remaining labels.

Equations

• LiebThirring.restExchangeSpins i j = Equiv.piCongrLeft (fun (x : { k : Fin N // k ≠ j }) => Fin q) (LiebThirring.restExchangeIndexEquiv i j)

noncomputable def LiebThirring.restExchangeAmplitudes {N q : ℕ} (i j : Fin N) : EuclideanSpace ℂ (OtherSpinLabels i q) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (OtherSpinLabels j q)

Spin-amplitude transport on the remaining labels.

Equations

• LiebThirring.restExchangeAmplitudes i j = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (LiebThirring.restExchangeSpins i j)

noncomputable def LiebThirring.restExchange {N q : ℕ} (i j : Fin N) : ↥(RestState i q) ≃ₗᵢ[ℂ] ↥(RestState j q)

The remaining-state unitary induced by particle exchange.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.permutePositions_swap_insertParticle {N : ℕ} (i j : Fin N) (x : Position) (y : OtherConfiguration j) : permutePositions (Equiv.swap i j) (insertParticle j x y) = insertParticle i x ((restExchangeSpatial i j) y)

Remaining spatial exchange intertwines the two insertion maps.

theorem LiebThirring.permuteSpins_swap_insertSpin {N q : ℕ} (i j : Fin N) (s : Fin q) (t : OtherSpinLabels j q) : permuteSpins (Equiv.swap i j) (insertSpin j s t) = insertSpin i s ((restExchangeSpins i j).symm t)

Remaining spin exchange intertwines the two spin insertions.

theorem LiebThirring.restExchange_ae {N q : ℕ} (i j : Fin N) (v : ↥(RestState i q)) : ∀ᵐ (y : OtherConfiguration j), ∀ (t : OtherSpinLabels j q), (↑↑((restExchange i j) v) y).ofLp t = (↑↑v ((restExchangeSpatial i j) y)).ofLp ((restExchangeSpins i j).symm t)

Exact representative of the remaining-state exchange unitary.