Commutation relations

i. Overview

In this module we compute the commutators for common operators acting on Schwartz maps on Space d.

Commutator lemmas come in three flavors:

• 1. a_commutation_b lemmas are of the form ⁅a, b⁆ = (⋯).
• 2. a_comp_b_commute and a_comp_commute lemmas are of the form a ∘ b = b ∘ a.
• 3. a_comp_b_eq lemmas are of the form a ∘ b = b ∘ a + (⋯).

ii. Key results

• position_commutation_momentum : The canonical commutation relations.
• angularMomentum_commutation_position : The position operator transforms as a vector under infinitessimal rotations.
• angularMomentum_commutation_radiusRegPow : Functions of ‖x‖² commute with the angular momenta.
• angularMomentum_commutation_momentum : The momentum operator transforms as a vector under infinitessimal rotations.
• angularMomentum_commutation_angularMomentum : Angular momenta generate an 𝔰𝔬(d) algebra.
• angularMomentumSqr_commutation_angularMomentum : 𝐋² is a quadratic Casimir of 𝔰𝔬(d).

iii. Table of contents

• A. General
• B. Commutators
  • B.1. Position / position
  • B.2. Momentum / momentum
  • B.3. Position / momentum
  • B.4. Angular momentum / position
  • B.5. Angular momentum / momentum
  • B.6. Angular momentum / angular momentum

iv. References

A. General

theorem QuantumMechanics.leibniz_lie {d : ℕ} (A B C : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ) : ⁅A.comp B, C⁆ = A.comp ⁅B, C⁆ + ⁅A, C⁆.comp B

theorem QuantumMechanics.lie_leibniz {d : ℕ} (A B C : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ) : ⁅A, B.comp C⁆ = B.comp ⁅A, C⁆ + ⁅A, B⁆.comp C

theorem QuantumMechanics.comp_eq_comp_add_commute {d : ℕ} (A B : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ) : A.comp B = B.comp A + ⁅A, B⁆

theorem QuantumMechanics.comp_eq_comp_sub_commute {d : ℕ} (A B : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ) : A.comp B = B.comp A - ⁅B, A⁆

B. Commutators

B.1. Position / position

theorem QuantumMechanics.position_commutation_position {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐱[j]⁆ = 0

Position operators commute: [xᵢ, xⱼ] = 0.

theorem QuantumMechanics.position_comp_commute {d : ℕ} (i j : Fin d) : 𝐱[i].comp 𝐱[j] = 𝐱[j].comp 𝐱[i]

theorem QuantumMechanics.position_commutation_radiusRegPow {d : ℕ} (i : Fin d) (ε : ℝˣ) (s : ℝ) : ⁅𝐱[i], 𝐫[ε,s]⁆ = 0

theorem QuantumMechanics.position_comp_radiusRegPow_commute {d : ℕ} (i : Fin d) (ε : ℝˣ) (s : ℝ) : 𝐱[i].comp 𝐫[ε,s] = 𝐫[ε,s].comp 𝐱[i]

theorem QuantumMechanics.radiusRegPow_commutation_radiusRegPow {d : ℕ} (ε : ℝˣ) (s t : ℝ) : ⁅𝐫[ε,s], 𝐫[ε,t]⁆ = 0

B.2. Momentum / momentum

theorem QuantumMechanics.momentum_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐩[i], 𝐩[j]⁆ = 0

Momentum operators commute: [pᵢ, pⱼ] = 0.

theorem QuantumMechanics.momentum_comp_commute {d : ℕ} (i j : Fin d) : 𝐩[i].comp 𝐩[j] = 𝐩[j].comp 𝐩[i]

theorem QuantumMechanics.momentumSqr_commutation_momentum {d : ℕ} (i : Fin d) : ⁅𝐩², 𝐩[i]⁆ = 0

theorem QuantumMechanics.momentumSqr_comp_momentum_commute {d : ℕ} (i : Fin d) : 𝐩².comp 𝐩[i] = 𝐩[i].comp 𝐩²

B.3. Position / momentum

theorem QuantumMechanics.position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j]⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,j]) • ContinuousLinearMap.id ℂ (SchwartzMap (Space d) ℂ)

The canonical commutation relations: [xᵢ, pⱼ] = iℏ δᵢⱼ𝟙.

theorem QuantumMechanics.momentum_comp_position_eq {d : ℕ} (i j : Fin d) : 𝐩[j].comp 𝐱[i] = 𝐱[i].comp 𝐩[j] - (Complex.I * ↑↑Constants.ℏ * ↑δ[i,j]) • ContinuousLinearMap.id ℂ (SchwartzMap (Space d) ℂ)

theorem QuantumMechanics.position_position_commutation_momentum {d : ℕ} (i j k : Fin d) : ⁅𝐱[i].comp 𝐱[j], 𝐩[k]⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • 𝐱[j] + (Complex.I * ↑↑Constants.ℏ * ↑δ[j,k]) • 𝐱[i]

theorem QuantumMechanics.position_commutation_momentum_momentum {d : ℕ} (i j k : Fin d) : ⁅𝐱[i], 𝐩[j].comp 𝐩[k]⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • 𝐩[j] + (Complex.I * ↑↑Constants.ℏ * ↑δ[i,j]) • 𝐩[k]

theorem QuantumMechanics.position_commutation_momentumSqr {d : ℕ} (i : Fin d) : ⁅𝐱[i], 𝐩²⁆ = (2 * Complex.I * ↑↑Constants.ℏ) • 𝐩[i]

theorem QuantumMechanics.radiusRegPow_commutation_momentum {d : ℕ} (ε : ℝˣ) (s : ℝ) (i : Fin d) : ⁅𝐫[ε,s], 𝐩[i]⁆ = (↑s * Complex.I * ↑↑Constants.ℏ) • 𝐫[ε,s - 2].comp 𝐱[i]

theorem QuantumMechanics.momentum_comp_radiusRegPow_eq {d : ℕ} (i : Fin d) (ε : ℝˣ) (s : ℝ) : 𝐩[i].comp 𝐫[ε,s] = 𝐫[ε,s].comp 𝐩[i] - (↑s * Complex.I * ↑↑Constants.ℏ) • 𝐫[ε,s - 2].comp 𝐱[i]

theorem QuantumMechanics.radiusRegPow_commutation_momentumSqr {d : ℕ} (ε : ℝˣ) (s : ℝ) : ⁅𝐫[ε,s], 𝐩²⁆ = (2 * ↑s * Complex.I * ↑↑Constants.ℏ) • 𝐫[ε,s - 2].comp (∑ i : Fin d, 𝐱[i].comp 𝐩[i]) + (s * ↑Constants.ℏ ^ 2) • ((↑d + s - 2) • 𝐫[ε,s - 2] - (↑ε ^ 2 * (s - 2)) • 𝐫[ε,s - 4])

B.4. Angular momentum / position

theorem QuantumMechanics.angularMomentum_commutation_position {d : ℕ} (i j k : Fin d) : ⁅𝐋[i,j], 𝐱[k]⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • 𝐱[j] - (Complex.I * ↑↑Constants.ℏ * ↑δ[j,k]) • 𝐱[i]

theorem QuantumMechanics.angularMomentum_commutation_radiusRegPow {d : ℕ} (i j : Fin d) (ε : ℝˣ) (s : ℝ) : ⁅𝐋[i,j], 𝐫[ε,s]⁆ = 0

theorem QuantumMechanics.angularMomentumSqr_commutation_radiusRegPow {d : ℕ} {s : ℝ} (ε : ℝˣ) : ⁅𝐋², 𝐫[ε,s]⁆ = 0

B.5. Angular momentum / momentum

theorem QuantumMechanics.angularMomentum_commutation_momentum {d : ℕ} (i j k : Fin d) : ⁅𝐋[i,j], 𝐩[k]⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • 𝐩[j] - (Complex.I * ↑↑Constants.ℏ * ↑δ[j,k]) • 𝐩[i]

theorem QuantumMechanics.momentum_comp_angularMomentum_eq {d : ℕ} (i j k : Fin d) : 𝐩[k].comp 𝐋[i,j] = 𝐋[i,j].comp 𝐩[k] - (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • 𝐩[j] + (Complex.I * ↑↑Constants.ℏ * ↑δ[j,k]) • 𝐩[i]

theorem QuantumMechanics.angularMomentum_commutation_momentumSqr {d : ℕ} (i j : Fin d) : ⁅𝐋[i,j], 𝐩²⁆ = 0

theorem QuantumMechanics.momentumSqr_comp_angularMomentum_commute {d : ℕ} (i j : Fin d) : 𝐩².comp 𝐋[i,j] = 𝐋[i,j].comp 𝐩²

theorem QuantumMechanics.angularMomentumSqr_commutation_momentumSqr {d : ℕ} : ⁅𝐋², 𝐩²⁆ = 0

B.6. Angular momentum / angular momentum

theorem QuantumMechanics.angularMomentum_commutation_angularMomentum {d : ℕ} (i j k l : Fin d) : ⁅𝐋[i,j], 𝐋[k,l]⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • 𝐋[j,l] - (Complex.I * ↑↑Constants.ℏ * ↑δ[i,l]) • 𝐋[j,k] - (Complex.I * ↑↑Constants.ℏ * ↑δ[j,k]) • 𝐋[i,l] + (Complex.I * ↑↑Constants.ℏ * ↑δ[j,l]) • 𝐋[i,k]

theorem QuantumMechanics.angularMomentumSqr_commutation_angularMomentum {d : ℕ} (i j : Fin d) : ⁅𝐋², 𝐋[i,j]⁆ = 0