From ac7438e3a016ee496fbfa0f0edcf6cad88cb45d0 Mon Sep 17 00:00:00 2001
From: Zhuoran Li <lizr.phys@gmail.com>
Date: Tue, 22 Sep 2026 10:27:43 +0800
Subject: [PATCH 1/2] feat: lift angular momentum to Hilbert space

AI assistance: Codex (GPT-6 Astra).

Co-authored-by: GPT-6 Astra <noreply@openai.com>
---
 .../QuantumMechanics/Operators/API-map.yaml   |  6 ++-
 .../Operators/AngularMomentum.lean            | 37 +++++++++++++++++++
 .../Operators/Commutation.lean                | 35 ++++++++++++++++++
 .../QuantumMechanics/Operators/Momentum.lean  |  9 ++++-
 .../QuantumMechanics/Operators/Position.lean  | 10 ++++-
 5 files changed, 94 insertions(+), 3 deletions(-)

diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml
index 6475f635e4..d449ec3787 100644
--- a/Physlib/QuantumMechanics/Operators/API-map.yaml
+++ b/Physlib/QuantumMechanics/Operators/API-map.yaml
@@ -137,7 +137,11 @@ Requirements:
     done: true
     location: "Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_momentumSqr, angularMomentumSqr_commutation_radiusRegPow, angularMomentum_commutation_momentumSqr, angularMomentum_commutation_radiusRegPow)"
 
-  - description: "The API shall carry angular momentum over from Schwartz maps, where it currently lives only as continuous linear maps, to the Hilbert space as a self-adjoint partially defined operator, with its spectrum, the raising and lowering operators, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions."
+  - description: "Each angular momentum component acts on the Hilbert space with dense Schwartz domain, agrees almost everywhere with its Schwartz-space action, preserves the Schwartz submodule, and is symmetric and closable."
+    done: true
+    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumHilbertOperator, angularMomentumHilbertOperator_domain_eq, angularMomentumHilbertOperator_apply, angularMomentumHilbertOperator_apply_ae, angularMomentumHilbertOperator_range, angularMomentumHilbertOperator_hasDenseDomain); Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentumOperator_eq_momentum_position, angularMomentumHilbertOperator_isSymmetric, angularMomentumHilbertOperator_isUnbounded)"
+
+  - description: "The API shall extend angular momentum from its Schwartz domain to self-adjoint operators on the Hilbert space, with their spectra, the raising and lowering operators, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions."
     done: false
     location: N/A
 
diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
index 12618b686b..4b99786326 100644
--- a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
+++ b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
@@ -14,6 +14,8 @@ public import Physlib.QuantumMechanics.Operators.Momentum
 ## i. Overview
 
 In this module we introduce several angular momentum operators for quantum mechanics on `Space d`.
+Each component also acts on `SpaceDHilbertSpace d` with domain `SchwartzSubmodule d`.
+Symmetry on this domain is proved in `QuantumMechanics.Operators.Commutation`.
 
 ## ii. Key results
 
@@ -24,6 +26,8 @@ Definitions:
     as `½ ∑ᵢⱼ 𝐋ᵢⱼ∘𝐋ᵢⱼ`.
 - `angularMomentumOperator2D` : the (pseudo)scalar angular momentum operator for `d = 2`.
 - `angularMomentumOperator3D` : the (pseudo)vector angular momentum operator for `d = 3`.
+- `angularMomentumHilbertOperator` : each component as a partially defined operator on
+    `SpaceDHilbertSpace d`, preserving the dense Schwartz submodule.
 
 Notation:
 - `𝐋` for `angularMomentumOperator`
@@ -35,6 +39,7 @@ Notation:
   - A.1 Antisymmetry
 - B. Angular momentum squared operator
 - C. Special cases in low dimensions
+- D. Hilbert-space angular momentum operator
 
 ## iv. References
 
@@ -139,5 +144,37 @@ def angularMomentumOperator3D (i : Fin 3) : 𝓢(Space 3, ℂ) →L[ℂ] 𝓢(Sp
     | 1 => 𝐋 2 0
     | 2 => 𝐋 0 1
 
+/-!
+## D. Hilbert-space angular momentum operator
+-/
+
+open MeasureTheory SpaceDHilbertSpace SchwartzSubmodule
+
+variable {d : ℕ} (i j : Fin d)
+
+/-- Component `i j` of angular momentum on the Hilbert space, with Schwartz domain.
+This transports the existing Schwartz-space operator `𝐋 i j`. -/
+def angularMomentumHilbertOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d where
+  domain := SchwartzSubmodule d
+  toFun := (schwartzIncl volume).1 ∘ₗ (𝐋 i j).1 ∘ₗ (schwartzEquiv volume).symm.1
+
+lemma angularMomentumHilbertOperator_domain_eq :
+    (angularMomentumHilbertOperator i j).domain = SchwartzSubmodule d := rfl
+
+lemma angularMomentumHilbertOperator_apply (ψ : SchwartzSubmodule d) :
+    angularMomentumHilbertOperator i j ψ =
+      schwartzEquiv volume (𝐋 i j ((schwartzEquiv volume).symm ψ)) := rfl
+
+lemma angularMomentumHilbertOperator_apply_ae (ψ : SchwartzSubmodule d) :
+    angularMomentumHilbertOperator i j ψ =ᵐ[volume] 𝐋 i j ((schwartzEquiv volume).symm ψ) :=
+  schwartzEquiv_coe_ae _
+
+lemma angularMomentumHilbertOperator_range (ψ : SchwartzSubmodule d) :
+    angularMomentumHilbertOperator i j ψ ∈ SchwartzSubmodule d := by
+  simp [angularMomentumHilbertOperator_apply]
+
+lemma angularMomentumHilbertOperator_hasDenseDomain :
+    (angularMomentumHilbertOperator i j).HasDenseDomain := SchwartzSubmodule.dense d _
+
 end
 end QuantumMechanics
diff --git a/Physlib/QuantumMechanics/Operators/Commutation.lean b/Physlib/QuantumMechanics/Operators/Commutation.lean
index e1c5520db0..b205399fd4 100644
--- a/Physlib/QuantumMechanics/Operators/Commutation.lean
+++ b/Physlib/QuantumMechanics/Operators/Commutation.lean
@@ -15,6 +15,7 @@ public import Physlib.QuantumMechanics.Operators.AngularMomentum
 ## i. Overview
 
 In this module we compute the commutators for common operators acting on Schwartz maps on `Space d`.
+We also use these relations to prove symmetry of angular momentum on the Schwartz submodule.
 
 Commutator lemmas come in three flavors:
   - 1. `a_commutation_b` lemmas are of the form `⁅a, b⁆ = (⋯)`.
@@ -31,6 +32,8 @@ Commutator lemmas come in three flavors:
     infinitessimal rotations.
 - `angularMomentum_commutation_angularMomentum` : Angular momenta generate an `𝔰𝔬(d)` algebra.
 - `angularMomentumSqr_commutation_angularMomentum` : `𝐋²` is a quadratic Casimir of `𝔰𝔬(d)`.
+- `angularMomentumHilbertOperator_isSymmetric` : angular momentum is symmetric on the
+    Schwartz submodule of `SpaceDHilbertSpace d`.
 
 ## iii. Table of contents
 
@@ -42,6 +45,7 @@ Commutator lemmas come in three flavors:
   - B.4. Angular momentum / position
   - B.5. Angular momentum / momentum
   - B.6. Angular momentum / angular momentum
+- C. Symmetry of Hilbert-space angular momentum
 
 ## iv. References
 
@@ -321,5 +325,36 @@ lemma angularMomentumSqr_commutation_angularMomentum : ⁅𝐋²[d], 𝐋 i j⁆
   abel_nf
   simp [smul_zero]
 
+/-!
+## C. Symmetry of Hilbert-space angular momentum
+-/
+
+open MeasureTheory SpaceDHilbertSpace SchwartzSubmodule
+
+/-- Reversing the order of position and momentum leaves angular momentum unchanged. -/
+lemma angularMomentumOperator_eq_momentum_position :
+    𝐋 i j = 𝐩 j ∘L 𝐱 i - 𝐩 i ∘L 𝐱 j := by
+  rw [momentum_comp_position_eq, momentum_comp_position_eq, KroneckerDelta.symm j i]
+  simp [angularMomentumOperator]
+
+/-- Each angular momentum component is symmetric on the Schwartz domain. -/
+lemma angularMomentumHilbertOperator_isSymmetric :
+    (angularMomentumHilbertOperator i j).IsSymmetric := by
+  intro ψ φ
+  obtain ⟨f, rfl⟩ := (schwartzEquiv volume).surjective ψ
+  obtain ⟨g, rfl⟩ := (schwartzEquiv volume).surjective φ
+  simp only [angularMomentumHilbertOperator_apply, LinearEquiv.symm_apply_apply,
+    ← Submodule.coe_inner]
+  rw [angularMomentumOperator_apply_fun, map_sub, inner_sub_left,
+    positionCLM_inner, positionCLM_inner, momentumCLM_inner, momentumCLM_inner,
+    ← inner_sub_right, ← map_sub, angularMomentumOperator_eq_momentum_position]
+  rfl
+
+/-- Angular momentum on the Schwartz domain is densely defined and closable. -/
+lemma angularMomentumHilbertOperator_isUnbounded :
+    (angularMomentumHilbertOperator i j).IsUnbounded :=
+  (angularMomentumHilbertOperator_isSymmetric i j).isUnbounded_iff_hasDenseDomain.mpr
+    (angularMomentumHilbertOperator_hasDenseDomain i j)
+
 end
 end QuantumMechanics
diff --git a/Physlib/QuantumMechanics/Operators/Momentum.lean b/Physlib/QuantumMechanics/Operators/Momentum.lean
index 9adece071d..6621bb0ec3 100644
--- a/Physlib/QuantumMechanics/Operators/Momentum.lean
+++ b/Physlib/QuantumMechanics/Operators/Momentum.lean
@@ -84,7 +84,7 @@ lemma momentumCLM_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) : 𝐩 i ψ x =
 -/
 
 open LinearPMap
-open MeasureTheory
+open MeasureTheory InnerProductSpace
 open SpaceDHilbertSpace
 open SchwartzSubmodule
 
@@ -137,6 +137,13 @@ lemma momentumOperator_isSymmetric : (𝓟 i).IsSymmetric := by
   congr 2
   exact integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable hI₂ hI₃ hI₄ (by fun_prop) (by fun_prop)
 
+/-- Momentum is symmetric for the Hilbert-space inner product of Schwartz maps. -/
+lemma momentumCLM_inner (f g : 𝓢(Space d, ℂ)) :
+    ⟪schwartzEquiv volume (𝐩 i f), schwartzEquiv volume g⟫_ℂ =
+      ⟪schwartzEquiv volume f, schwartzEquiv volume (𝐩 i g)⟫_ℂ := by
+  simpa only [momentumOperator_apply, LinearEquiv.symm_apply_apply, Submodule.coe_inner] using
+    momentumOperator_isSymmetric i (schwartzEquiv volume f) (schwartzEquiv volume g)
+
 lemma momentumOperator_isUnbounded : (𝓟 i).IsUnbounded := by
   refine (LinearPMap.IsSymmetric.isUnbounded_iff_hasDenseDomain ?_).mpr ?_
   · exact momentumOperator_isSymmetric i
diff --git a/Physlib/QuantumMechanics/Operators/Position.lean b/Physlib/QuantumMechanics/Operators/Position.lean
index a2ecc83789..672fd931d7 100644
--- a/Physlib/QuantumMechanics/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/Operators/Position.lean
@@ -54,7 +54,7 @@ Notation:
 namespace QuantumMechanics
 
 open Filter
-open MeasureTheory
+open MeasureTheory InnerProductSpace
 open SchwartzMap
 open SpaceDHilbertSpace
 open SchwartzSubmodule PolyBddSchwartzSubmodule
@@ -93,6 +93,14 @@ lemma positionCLM_apply_fun (ψ : 𝓢(Space d, ℂ)) : 𝐱 i ψ = (fun x : Spa
 lemma positionCLM_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) : 𝐱 i ψ x = x i * ψ x := by
   simp [positionCLM_apply_fun]
 
+/-- Position is symmetric for the Hilbert-space inner product of Schwartz maps. -/
+lemma positionCLM_inner [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure]
+    (f g : 𝓢(Space d, ℂ)) :
+    ⟪schwartzEquiv μ (𝐱 i f), schwartzEquiv μ g⟫_ℂ =
+      ⟪schwartzEquiv μ f, schwartzEquiv μ (𝐱 i g)⟫_ℂ := by
+  simp only [schwartzEquiv_inner, positionCLM_apply, map_mul, Complex.conj_ofReal,
+    mul_left_comm, mul_assoc]
+
 /-!
 ### A.2. Radius powers (regularized)
 -/

From 1d12dc2ecf8b1b38d7e48df21c0e755149937f7d Mon Sep 17 00:00:00 2001
From: Zhuoran Li <lizr.phys@gmail.com>
Date: Tue, 22 Sep 2026 19:57:03 +0800
Subject: [PATCH 2/2] refactor: consolidate angular momentum operators and
 lemmas

Use angularMomentumCLM for Schwartz components and angularMomentumOperator
for the Hilbert-space operator, following the position and momentum APIs.
Move angular momentum symmetry and commutation results into AngularMomentum,
leaving shared commutation infrastructure in Commutation. Update the direct
downstream references and API map without changing mathematical statements
or proofs beyond the renamed identifiers.

AI assistance: Codex (GPT-6 Astra).

Co-authored-by: GPT-6 Astra <noreply@openai.com>
---
 .../Hydrogen/LaplaceRungeLenzVector.lean      |  40 ++--
 .../QuantumMechanics/Operators/API-map.yaml   |   8 +-
 .../Operators/AngularMomentum.lean            | 186 +++++++++++++++---
 .../Operators/Commutation.lean                | 139 +------------
 4 files changed, 186 insertions(+), 187 deletions(-)

diff --git a/Physlib/QuantumMechanics/Hydrogen/LaplaceRungeLenzVector.lean b/Physlib/QuantumMechanics/Hydrogen/LaplaceRungeLenzVector.lean
index 8475ecc761..1bf8b93711 100644
--- a/Physlib/QuantumMechanics/Hydrogen/LaplaceRungeLenzVector.lean
+++ b/Physlib/QuantumMechanics/Hydrogen/LaplaceRungeLenzVector.lean
@@ -6,7 +6,7 @@ Authors: Gregory J. Loges
 module
 
 public import Physlib.QuantumMechanics.Hydrogen.Basic
-public import Physlib.QuantumMechanics.Operators.Commutation
+public import Physlib.QuantumMechanics.Operators.AngularMomentum
 /-!
 
 # Laplace-Runge-Lenz vector
@@ -48,7 +48,7 @@ lemma lrlOperator_eq (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i = 𝐱 i 
   calc
     _ = (2 : ℝ)⁻¹ • ∑ j, ((𝐩 j ∘L 𝐱 i) ∘L 𝐩 j + 𝐱 i ∘L 𝐩 j ∘L 𝐩 j
         - ((𝐩 j ∘L 𝐱 j) ∘L 𝐩 i + 𝐱 j ∘L 𝐩 j ∘L 𝐩 i)) := by
-      simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumOperator, comp_sub,
+      simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumCLM, comp_sub,
         sub_comp, comp_assoc, momentum_comp_commute, ← sub_sub, add_sub, sub_add_eq_add_sub]
     _ = (2 : ℂ)⁻¹ • ∑ j, ((2 : ℂ) • 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - (I * ℏ) • δ[i,j] • 𝐩 j
         - ((2 : ℂ) • (𝐱 j ∘L 𝐩 j) ∘L 𝐩 i - (I * ℏ) • 𝐩 i)) := by
@@ -72,7 +72,7 @@ lemma lrlOperator_eq' (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i =
   rw [lrlOperator_eq, sub_left_inj, add_left_inj]
   symm
   trans ∑ j, 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - ∑ j, (𝐱 j ∘L 𝐩 j) ∘L 𝐩 i
-  · simp [dotProduct, mul_def, angularMomentumOperator, comp_assoc, momentum_comp_commute]
+  · simp [dotProduct, mul_def, angularMomentumCLM, comp_assoc, momentum_comp_commute]
   simp [← comp_finsetSum, ← finsetSum_comp, dotProduct, mul_def]
 
 /-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/
@@ -103,7 +103,7 @@ lemma angularMomentum_commutation_Ldot_p (i j k : Fin H.d) :
     comp_smul, smul_comp, comp_sub, sub_comp, add_comp]
   simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.smul_sum,
     KroneckerDelta.sum_smul]
-  rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j]
+  rw [angularMomentumCLM_antisymm k i, angularMomentumCLM_antisymm k j]
   simp only [neg_comp]
   module
 
@@ -182,9 +182,9 @@ private lemma positionCompMomentumSqr_comm {d : ℕ} (i j : Fin d) :
       simp [lie_leibniz, leibniz_lie, comp_assoc]
     _ = (2 * I * ℏ) • 𝐋 j i ∘L (𝐩 ⬝ᵥ 𝐩) := by
       simp_rw [← lie_skew (𝐩 ⬝ᵥ 𝐩) _, position_commutation_momentumSqr, comp_neg, comp_smul,
-        ← sub_eq_add_neg, ← smul_sub, smul_comp, angularMomentumOperator]
+        ← sub_eq_add_neg, ← smul_sub, smul_comp, angularMomentumCLM]
     _ = (-2 * I * ℏ) • (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j := by
-      rw [angularMomentumOperator_antisymm j i, neg_comp, smul_neg, ← neg_smul, ← neg_mul,
+      rw [angularMomentumCLM_antisymm j i, neg_comp, smul_neg, ← neg_smul, ← neg_mul,
         ← neg_mul, momentumSqr_comp_angularMomentum_commute]
 
 private lemma positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add
@@ -194,7 +194,7 @@ private lemma positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add
       = (-I * ℏ) • (𝐱 k ∘L 𝐩 l - δ[k,l] • (𝐱 ⬝ᵥ 𝐩)) ∘L (𝐩 ⬝ᵥ 𝐩) by
     nth_rw 2 [← lie_skew]
     simp_rw [this, ← sub_eq_add_neg, ← smul_sub, ← sub_comp, symm j i, sub_sub_sub_cancel_right,
-      momentumSqr_comp_angularMomentum_commute, angularMomentumOperator]
+      momentumSqr_comp_angularMomentum_commute, angularMomentumCLM]
   intro k l
   calc
     _ = (𝐱 ⬝ᵥ 𝐩) ∘L ⁅𝐱 k, 𝐩 l⁆ ∘L (𝐩 ⬝ᵥ 𝐩) + 𝐱 k ∘L ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐱[d] ⬝ᵥ 𝐩⁆ ∘L 𝐩 l
@@ -248,7 +248,7 @@ private lemma positionCompMomentumSqr_comm_radiusRegInvCompPosition_add
     _ = 𝐫₀ ε (-1) ∘L (𝐱 i ∘L ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐱 j⁆ - 𝐱 j ∘L ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐱 i⁆) := by simp [hA]
     _ = (-2 * I * ℏ) • 𝐫₀ ε (-1) ∘L 𝐋 i j := by
       simp_rw [← lie_skew _ (𝐱 _), position_commutation_momentumSqr, comp_neg, comp_smul,
-        ← neg_smul, ← neg_mul, ← smul_sub, comp_smul, angularMomentumOperator]
+        ← neg_smul, ← neg_mul, ← smul_sub, comp_smul, angularMomentumCLM]
 
 private lemma momentum_comm_radiusRegPow_position_symm {d : ℕ} (ε : ℝˣ) (s : ℝ) (i j : Fin d) :
     ⁅𝐩 i, 𝐫₀ ε s ∘L 𝐱 j⁆ = ⁅𝐩 j, 𝐫₀ ε s ∘L 𝐱 i⁆ := by
@@ -262,8 +262,8 @@ private lemma positionDotMomentumCompMomentum_comm_radiusRegInvCompPosition_add
     nth_rw 2 [← lie_skew]
     simp_rw [leibniz_lie, this,
       momentum_comm_radiusRegPow_position_symm, ← sub_eq_add_neg, add_sub_add_left_eq_sub,
-      smul_comp, ← smul_sub, comp_assoc, ← comp_sub, angularMomentumOperator_antisymm i j, comp_neg,
-      smul_neg, neg_mul, neg_smul, angularMomentumOperator]
+      smul_comp, ← smul_sub, comp_assoc, ← comp_sub, angularMomentumCLM_antisymm i j, comp_neg,
+      smul_neg, neg_mul, neg_smul, angularMomentumCLM]
   intro k
   calc
     _ = -(I * ℏ) • (ε.1 ^ 2) • 𝐫₀ ε (-1-2) ∘L 𝐱 k := by
@@ -330,7 +330,7 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) :
     𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱 = (2 : ℝ) • (𝐱 ⬝ᵥ 𝐩) ∘L 𝐱 i + (-I * ℏ * (d - 3)) • 𝐱 i
     + ((-2 : ℝ) • 𝐫₀ ε 2 ∘L 𝐩 i + (2 * ε.1 ^ 2 : ℝ) • 𝐩 i) := by
   -- Change summand
-  simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumOperator, comp_sub,
+  simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumCLM, comp_sub,
     sub_comp, comp_assoc, sub_add_sub_comm, momentum_comp_position_eq, comp_sub, comp_smul,
     comp_id, ← comp_assoc, position_comp_commute i _, ← add_sub_assoc, ← two_smul ℝ,
     sub_sub_eq_add_sub, sub_add_eq_add_sub, comp_assoc, comp_eq_comp_add_commute (𝐱 i) (𝐩 _),
@@ -425,14 +425,14 @@ private lemma sum_Lpp (d : ℕ) : ∑ i : Fin d, ∑ j, 𝐋 i j ∘L 𝐩 j ∘
   rw [sum_symmetrize]
   conv_lhs =>
     enter [2, 2, i, 2, j]
-    rw [angularMomentumOperator_antisymm j i, momentum_comp_commute j i]
+    rw [angularMomentumCLM_antisymm j i, momentum_comp_commute j i]
   simp
 
 private lemma sum_ppL (d : ℕ) : ∑ i : Fin d, ∑ j, 𝐩 i ∘L 𝐩 j ∘L 𝐋 i j = 0 := by
   rw [sum_symmetrize]
   conv_lhs =>
     enter [2, 2, i, 2, j]
-    rw [← comp_assoc, ← comp_assoc, angularMomentumOperator_antisymm j i, momentum_comp_commute j i]
+    rw [← comp_assoc, ← comp_assoc, angularMomentumCLM_antisymm j i, momentum_comp_commute j i]
   simp
 
 private lemma sum_LppL (d : ℕ) :
@@ -442,15 +442,15 @@ private lemma sum_LppL (d : ℕ) :
     enter [2, 2, i, 2, j, 2, k]
     calc
       _ = (𝐋 i k ∘L 𝐩 k ∘L 𝐩 j - 𝐋 j k ∘L 𝐩 k ∘L 𝐩 i) ∘L 𝐋 i j := by
-        simp [angularMomentumOperator_antisymm j i, comp_neg, ← comp_assoc, sub_eq_add_neg]
+        simp [angularMomentumCLM_antisymm j i, comp_neg, ← comp_assoc, sub_eq_add_neg]
       _ = (𝐱 i ∘L 𝐩 k ∘L 𝐩 k ∘L 𝐩 j - 𝐱 k ∘L 𝐩 i ∘L 𝐩 k ∘L 𝐩 j
           - (𝐱 j ∘L 𝐩 k ∘L 𝐩 k ∘L 𝐩 i - 𝐱 k ∘L 𝐩 j ∘L 𝐩 k ∘L 𝐩 i)) ∘L 𝐋 i j := by
-        simp_rw [angularMomentumOperator, sub_comp, comp_assoc]
+        simp_rw [angularMomentumCLM, sub_comp, comp_assoc]
       _ = (𝐱 i ∘L 𝐩 j ∘L 𝐩 k ∘L 𝐩 k - 𝐱 j ∘L 𝐩 i ∘L 𝐩 k ∘L 𝐩 k) ∘L 𝐋 i j := by
         simp_rw [momentum_comp_commute k, ← comp_assoc (𝐩 _), momentum_comp_commute k,
           momentum_comp_commute i j, sub_sub_sub_cancel_right]
       _ = 𝐋 i j ∘L (𝐩 k ∘L 𝐩 k) ∘L 𝐋 i j := by
-        simp_rw [← comp_assoc, ← sub_comp, angularMomentumOperator]
+        simp_rw [← comp_assoc, ← sub_comp, angularMomentumCLM]
   trans (2 : ℂ)⁻¹ • ∑ i, ∑ j, 𝐋 i j ∘L (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j
   · simp_rw [← comp_finsetSum, ← finsetSum_comp, ← comp_assoc, dotProduct, mul_def]
   simp_rw [← comp_assoc, ← momentumSqr_comp_angularMomentum_commute, comp_assoc, ← comp_finsetSum,
@@ -464,9 +464,9 @@ private lemma sum_Lprx (d : ℕ) (ε : ℝˣ) :
     enter [1, 2, 2, i, 2, j]
     calc
       _ = 𝐋 i j ∘L (𝐩 j ∘L 𝐱 i - 𝐩 i ∘L 𝐱 j) := by
-        simp [angularMomentumOperator_antisymm j i, comp_assoc, sub_eq_add_neg]
+        simp [angularMomentumCLM_antisymm j i, comp_assoc, sub_eq_add_neg]
       _ = 𝐋 i j ∘L 𝐋 i j := by
-        simp [momentum_comp_position_eq, symm j i, angularMomentumOperator]
+        simp [momentum_comp_position_eq, symm j i, angularMomentumCLM]
   rw [← angularMomentumSqr_comp_radiusRegPow_commute, angularMomentumOperatorSqr]
 
 private lemma sum_rxpL (d : ℕ) (ε : ℝˣ) :
@@ -475,8 +475,8 @@ private lemma sum_rxpL (d : ℕ) (ε : ℝˣ) :
   rw [sum_symmetrize]
   conv_lhs =>
     enter [2, 2, 2, i, 2, j]
-    rw [angularMomentumOperator_antisymm j i, comp_neg, comp_neg, ← sub_eq_add_neg, ← comp_assoc,
-      ← comp_assoc, ← sub_comp, ← angularMomentumOperator]
+    rw [angularMomentumCLM_antisymm j i, comp_neg, comp_neg, ← sub_eq_add_neg, ← comp_assoc,
+      ← comp_assoc, ← sub_comp, ← angularMomentumCLM]
   rw [angularMomentumOperatorSqr]
 
 private lemma sum_prx (d : ℕ) (ε : ℝˣ) :
diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml
index d449ec3787..0704f8563c 100644
--- a/Physlib/QuantumMechanics/Operators/API-map.yaml
+++ b/Physlib/QuantumMechanics/Operators/API-map.yaml
@@ -127,19 +127,19 @@ Requirements:
 
   - description: "The components 𝐋ᵢⱼ = xᵢpⱼ - xⱼpᵢ of the angular momentum operator and the scalar 𝐋² are defined on Schwartz maps, with antisymmetry in the two indices and the vanishing of a repeated index, and the one-, two- and three-dimensional cases are treated separately."
     done: true
-    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumOperator, notation 𝐋, angularMomentumOperator_apply, angularMomentumOperator_antisymm, angularMomentumOperator_eq_zero, angularMomentumOperatorSqr, notation 𝐋², angularMomentumOperatorSqr_apply, angularMomentumOperator1D_trivial, angularMomentumOperator2D, angularMomentumOperator3D)"
+    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumCLM, notation 𝐋, angularMomentumCLM_apply, angularMomentumCLM_antisymm, angularMomentumCLM_eq_zero, angularMomentumOperatorSqr, notation 𝐋², angularMomentumOperatorSqr_apply, angularMomentumOperator1D_trivial, angularMomentumOperator2D, angularMomentumOperator3D)"
 
   - description: "Position and momentum transform as vectors under the angular momenta, which close into the Lie algebra of rotations."
     done: true
-    location: "Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentum_commutation_position, angularMomentum_commutation_momentum, angularMomentum_commutation_angularMomentum)"
+    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentum_commutation_position, angularMomentum_commutation_momentum, angularMomentum_commutation_angularMomentum)"
 
   - description: "The scalar 𝐋² commutes with every angular momentum component, with the momentum squared and with any regularized power of the radius."
     done: true
-    location: "Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_momentumSqr, angularMomentumSqr_commutation_radiusRegPow, angularMomentum_commutation_momentumSqr, angularMomentum_commutation_radiusRegPow)"
+    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_momentumSqr, angularMomentumSqr_commutation_radiusRegPow, angularMomentum_commutation_momentumSqr, angularMomentum_commutation_radiusRegPow)"
 
   - description: "Each angular momentum component acts on the Hilbert space with dense Schwartz domain, agrees almost everywhere with its Schwartz-space action, preserves the Schwartz submodule, and is symmetric and closable."
     done: true
-    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumHilbertOperator, angularMomentumHilbertOperator_domain_eq, angularMomentumHilbertOperator_apply, angularMomentumHilbertOperator_apply_ae, angularMomentumHilbertOperator_range, angularMomentumHilbertOperator_hasDenseDomain); Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentumOperator_eq_momentum_position, angularMomentumHilbertOperator_isSymmetric, angularMomentumHilbertOperator_isUnbounded)"
+    location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumOperator, angularMomentumOperator_domain_eq, angularMomentumOperator_apply, angularMomentumOperator_apply_ae, angularMomentumOperator_range, angularMomentumOperator_hasDenseDomain, angularMomentumCLM_eq_momentum_position, angularMomentumOperator_isSymmetric, angularMomentumOperator_isUnbounded)"
 
   - description: "The API shall extend angular momentum from its Schwartz domain to self-adjoint operators on the Hilbert space, with their spectra, the raising and lowering operators, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions."
     done: false
diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
index 4b99786326..24b6d5c127 100644
--- a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
+++ b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
@@ -5,8 +5,7 @@ Authors: Gregory J. Loges
 -/
 module
 
-public import Physlib.QuantumMechanics.Operators.Position
-public import Physlib.QuantumMechanics.Operators.Momentum
+public import Physlib.QuantumMechanics.Operators.Commutation
 /-!
 
 # Angular momentum operator
@@ -14,23 +13,27 @@ public import Physlib.QuantumMechanics.Operators.Momentum
 ## i. Overview
 
 In this module we introduce several angular momentum operators for quantum mechanics on `Space d`.
-Each component also acts on `SpaceDHilbertSpace d` with domain `SchwartzSubmodule d`.
-Symmetry on this domain is proved in `QuantumMechanics.Operators.Commutation`.
+Each component also acts symmetrically on `SpaceDHilbertSpace d` with domain `SchwartzSubmodule d`.
+We prove its symmetry and commutation relations.
 
 ## ii. Key results
 
 Definitions:
-- `angularMomentumOperator` : (components of) the angular momentum operator acting on Schwartz maps
+- `angularMomentumCLM` : (components of) the angular momentum operator acting on Schwartz maps
     `𝓢(Space d, ℂ)` as `𝐱ᵢ∘𝐩ⱼ - 𝐱ⱼ∘𝐩ᵢ`.
 - `angularMomentumOperatorSqr` : the operator acting on Schwartz maps `𝓢(Space d, ℂ)`
     as `½ ∑ᵢⱼ 𝐋ᵢⱼ∘𝐋ᵢⱼ`.
 - `angularMomentumOperator2D` : the (pseudo)scalar angular momentum operator for `d = 2`.
 - `angularMomentumOperator3D` : the (pseudo)vector angular momentum operator for `d = 3`.
-- `angularMomentumHilbertOperator` : each component as a partially defined operator on
+- `angularMomentumOperator` : each component as a partially defined operator on
     `SpaceDHilbertSpace d`, preserving the dense Schwartz submodule.
 
+Lemmas:
+- `angularMomentumOperator_isSymmetric` : angular momentum is symmetric on the Schwartz domain.
+- `angularMomentum_commutation_angularMomentum` : angular momenta generate an `𝔰𝔬(d)` algebra.
+
 Notation:
-- `𝐋` for `angularMomentumOperator`
+- `𝐋` for `angularMomentumCLM`
 - `𝐋²` for `angularMomentumOperatorSqr`
 
 ## iii. Table of contents
@@ -40,6 +43,10 @@ Notation:
 - B. Angular momentum squared operator
 - C. Special cases in low dimensions
 - D. Hilbert-space angular momentum operator
+- E. Commutation relations
+  - E.1. Angular momentum / position
+  - E.2. Angular momentum / momentum
+  - E.3. Angular momentum / angular momentum
 
 ## iv. References
 
@@ -61,19 +68,19 @@ open ContDiff SchwartzMap
 
 /-- Component `i j` of the angular momentum operator is the continuous linear map
 from `𝓢(Space d, ℂ)` to itself defined by `𝐋ᵢⱼ ≔ 𝐱ᵢ∘𝐩ⱼ - 𝐱ⱼ∘𝐩ᵢ`. -/
-def angularMomentumOperator {d : ℕ} (i j : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+def angularMomentumCLM {d : ℕ} (i j : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
   𝐱 i ∘L 𝐩 j - 𝐱 j ∘L 𝐩 i
 
-@[inherit_doc angularMomentumOperator]
-notation "𝐋" => angularMomentumOperator
+@[inherit_doc angularMomentumCLM]
+notation "𝐋" => angularMomentumCLM
 
-@[inherit_doc angularMomentumOperator]
-notation "𝐋[" d' "]" => angularMomentumOperator (d := d')
+@[inherit_doc angularMomentumCLM]
+notation "𝐋[" d' "]" => angularMomentumCLM (d := d')
 
-lemma angularMomentumOperator_apply_fun {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+lemma angularMomentumCLM_apply_fun {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) :
     𝐋 i j ψ = 𝐱 i (𝐩 j ψ) - 𝐱 j (𝐩 i ψ) := rfl
 
-lemma angularMomentumOperator_apply {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+lemma angularMomentumCLM_apply {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
     𝐋 i j ψ x = 𝐱 i (𝐩 j ψ) x - 𝐱 j (𝐩 i ψ) x := rfl
 
 /-!
@@ -83,11 +90,11 @@ lemma angularMomentumOperator_apply {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d,
 -/
 
 /-- The angular momentum operator is antisymmetric, `𝐋ᵢⱼ = -𝐋ⱼᵢ` -/
-lemma angularMomentumOperator_antisymm {d : ℕ} (i j : Fin d) : 𝐋 i j = -𝐋 j i :=
+lemma angularMomentumCLM_antisymm {d : ℕ} (i j : Fin d) : 𝐋 i j = -𝐋 j i :=
   Eq.symm (neg_sub _ _)
 
 /-- Angular momentum operator components with repeated index vanish, `𝐋ᵢᵢ = 0`. -/
-lemma angularMomentumOperator_eq_zero {d : ℕ} (i : Fin d) : 𝐋 i i = 0 := sub_self _
+lemma angularMomentumCLM_eq_zero {d : ℕ} (i : Fin d) : 𝐋 i i = 0 := sub_self _
 
 /-!
 
@@ -132,7 +139,7 @@ lemma angularMomentumOperatorSqr_apply {d : ℕ} (ψ : 𝓢(Space d, ℂ)) (x :
 /-- In one dimension the angular momentum operator is trivial. -/
 lemma angularMomentumOperator1D_trivial : 𝐋[1] = 0 := by
   ext i j
-  simp [Subsingleton.elim i j, angularMomentumOperator_eq_zero]
+  simp [Subsingleton.elim i j, angularMomentumCLM_eq_zero]
 
 /-- The angular momentum (pseudo)scalar operator in two dimensions, `𝐋 ≔ 𝐋₀₁`. -/
 def angularMomentumOperator2D : 𝓢(Space 2, ℂ) →L[ℂ] 𝓢(Space 2, ℂ) := 𝐋 0 1
@@ -154,27 +161,148 @@ variable {d : ℕ} (i j : Fin d)
 
 /-- Component `i j` of angular momentum on the Hilbert space, with Schwartz domain.
 This transports the existing Schwartz-space operator `𝐋 i j`. -/
-def angularMomentumHilbertOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d where
+def angularMomentumOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d where
   domain := SchwartzSubmodule d
   toFun := (schwartzIncl volume).1 ∘ₗ (𝐋 i j).1 ∘ₗ (schwartzEquiv volume).symm.1
 
-lemma angularMomentumHilbertOperator_domain_eq :
-    (angularMomentumHilbertOperator i j).domain = SchwartzSubmodule d := rfl
+lemma angularMomentumOperator_domain_eq :
+    (angularMomentumOperator i j).domain = SchwartzSubmodule d := rfl
 
-lemma angularMomentumHilbertOperator_apply (ψ : SchwartzSubmodule d) :
-    angularMomentumHilbertOperator i j ψ =
+lemma angularMomentumOperator_apply (ψ : SchwartzSubmodule d) :
+    angularMomentumOperator i j ψ =
       schwartzEquiv volume (𝐋 i j ((schwartzEquiv volume).symm ψ)) := rfl
 
-lemma angularMomentumHilbertOperator_apply_ae (ψ : SchwartzSubmodule d) :
-    angularMomentumHilbertOperator i j ψ =ᵐ[volume] 𝐋 i j ((schwartzEquiv volume).symm ψ) :=
+lemma angularMomentumOperator_apply_ae (ψ : SchwartzSubmodule d) :
+    angularMomentumOperator i j ψ =ᵐ[volume] 𝐋 i j ((schwartzEquiv volume).symm ψ) :=
   schwartzEquiv_coe_ae _
 
-lemma angularMomentumHilbertOperator_range (ψ : SchwartzSubmodule d) :
-    angularMomentumHilbertOperator i j ψ ∈ SchwartzSubmodule d := by
-  simp [angularMomentumHilbertOperator_apply]
+lemma angularMomentumOperator_range (ψ : SchwartzSubmodule d) :
+    angularMomentumOperator i j ψ ∈ SchwartzSubmodule d := by
+  simp [angularMomentumOperator_apply]
+
+lemma angularMomentumOperator_hasDenseDomain :
+    (angularMomentumOperator i j).HasDenseDomain := SchwartzSubmodule.dense d _
+
+/-- Reversing the order of position and momentum leaves angular momentum unchanged. -/
+lemma angularMomentumCLM_eq_momentum_position :
+    𝐋 i j = 𝐩 j ∘L 𝐱 i - 𝐩 i ∘L 𝐱 j := by
+  rw [momentum_comp_position_eq, momentum_comp_position_eq, KroneckerDelta.symm j i]
+  simp [angularMomentumCLM]
+
+/-- Each angular momentum component is symmetric on the Schwartz domain. -/
+lemma angularMomentumOperator_isSymmetric :
+    (angularMomentumOperator i j).IsSymmetric := by
+  intro ψ φ
+  obtain ⟨f, rfl⟩ := (schwartzEquiv volume).surjective ψ
+  obtain ⟨g, rfl⟩ := (schwartzEquiv volume).surjective φ
+  simp only [angularMomentumOperator_apply, LinearEquiv.symm_apply_apply,
+    ← Submodule.coe_inner]
+  rw [angularMomentumCLM_apply_fun, map_sub, inner_sub_left,
+    positionCLM_inner, positionCLM_inner, momentumCLM_inner, momentumCLM_inner,
+    ← inner_sub_right, ← map_sub, angularMomentumCLM_eq_momentum_position]
+  rfl
+
+/-- Angular momentum on the Schwartz domain is densely defined and closable. -/
+lemma angularMomentumOperator_isUnbounded :
+    (angularMomentumOperator i j).IsUnbounded :=
+  (angularMomentumOperator_isSymmetric i j).isUnbounded_iff_hasDenseDomain.mpr
+    (angularMomentumOperator_hasDenseDomain i j)
+
+/-!
+## E. Commutation relations
+-/
+
+open Complex KroneckerDelta Bracket ContinuousLinearMap
+
+variable (k l : Fin d) (ε : ℝˣ) (s : ℝ)
+
+attribute [local instance 100] LieRing.ofAssociativeRing
+
+/-!
+
+### E.1. Angular momentum / position
+
+-/
+
+lemma angularMomentum_commutation_position :
+    ⁅𝐋 i j, 𝐱 k⁆ = (I * ℏ) • (δ[i,k] • 𝐱 j - δ[j,k] • 𝐱 i) := by
+  trans 𝐱 i ∘L ⁅𝐩 j, 𝐱 k⁆ - 𝐱 j ∘L ⁅𝐩 i, 𝐱 k⁆
+  · simp [angularMomentumCLM, leibniz_lie]
+  simp only [← lie_skew (𝐩 _), comp_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg,
+    position_commutation_momentum, comp_smul, comp_id, smul_sub, symm k _]
+
+@[simp]
+lemma angularMomentum_commutation_radiusRegPow : ⁅𝐋 i j, 𝐫₀[d] ε s⁆ = 0 := by
+  trans 𝐱 i ∘L ⁅𝐩 j, 𝐫₀ ε s⁆ - 𝐱 j ∘L ⁅𝐩 i, 𝐫₀ ε s⁆
+  · simp [angularMomentumCLM, leibniz_lie]
+  simp [← lie_skew (𝐩 _), radiusRegPow_commutation_momentum, comp_neg,
+    ← position_comp_radiusRegPow_commute, ← comp_assoc, position_comp_commute]
+
+lemma angularMomentum_comp_radiusRegPow_commute : 𝐋 i j ∘L 𝐫₀ ε s = 𝐫₀ ε s ∘L 𝐋 i j := by
+  rw [comp_eq_comp_add_commute, angularMomentum_commutation_radiusRegPow, add_zero]
+
+@[simp]
+lemma angularMomentumSqr_commutation_radiusRegPow : ⁅𝐋²[d], 𝐫₀[d] ε s⁆ = 0 := by
+  simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie]
+
+lemma angularMomentumSqr_comp_radiusRegPow_commute : 𝐋² ∘L 𝐫₀[d] ε s = 𝐫₀ ε s ∘L 𝐋² := by
+  rw [comp_eq_comp_add_commute, angularMomentumSqr_commutation_radiusRegPow, add_zero]
+
+/-!
+
+### E.2. Angular momentum / momentum
+
+-/
+
+lemma angularMomentum_commutation_momentum :
+    ⁅𝐋 i j, 𝐩 k⁆ = (I * ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) := by
+  trans ⁅𝐱 i, 𝐩 k⁆ ∘L 𝐩 j - ⁅𝐱 j, 𝐩 k⁆ ∘L 𝐩 i
+  · simp [angularMomentumCLM, leibniz_lie]
+  simp only [position_commutation_momentum, smul_comp, id_comp, smul_sub]
+
+lemma momentum_comp_angularMomentum_eq :
+    𝐩 k ∘L 𝐋 i j = 𝐋 i j ∘L 𝐩 k - (I * ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) := by
+  rw [comp_eq_comp_sub_commute, angularMomentum_commutation_momentum]
+
+@[simp]
+lemma angularMomentum_commutation_momentumSqr : ⁅𝐋 i j, 𝐩[d] ⬝ᵥ 𝐩⁆ = 0 := by
+  simp only [dotProduct, mul_def, lie_sum, lie_leibniz, angularMomentum_commutation_momentum,
+    comp_smul, comp_sub, smul_comp, sub_comp, ← smul_add, ← Finset.smul_sum, Finset.sum_add_distrib,
+    Finset.sum_sub_distrib, sum_smul, sub_add_sub_cancel, sub_self, smul_zero]
+
+lemma momentumSqr_comp_angularMomentum_commute : (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j = 𝐋 i j ∘L (𝐩 ⬝ᵥ 𝐩) := by
+  rw [comp_eq_comp_sub_commute, angularMomentum_commutation_momentumSqr, sub_zero]
+
+@[simp]
+lemma angularMomentumSqr_commutation_momentumSqr : ⁅𝐋²[d], 𝐩[d] ⬝ᵥ 𝐩⁆ = 0 := by
+  simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie]
+
+/-!
+
+### E.3. Angular momentum / angular momentum
+
+-/
 
-lemma angularMomentumHilbertOperator_hasDenseDomain :
-    (angularMomentumHilbertOperator i j).HasDenseDomain := SchwartzSubmodule.dense d _
+lemma angularMomentum_commutation_angularMomentum : ⁅𝐋 i j, 𝐋 k l⁆ =
+    (I * ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k) := by
+  nth_rw 2 [angularMomentumCLM]
+  simp only [angularMomentum_commutation_position, angularMomentum_commutation_momentum,
+    lie_sub, lie_leibniz, comp_smul, smul_comp, comp_sub, sub_comp, ← smul_add, ← smul_sub]
+  dsimp [angularMomentumCLM]
+  ext
+  simp only [nsmul_eq_mul, smul_apply, sub_apply, add_apply, mul_apply_eq_comp, comp_apply,
+    _root_.natCast_apply, positionCLM_apply, momentumCLM_apply, neg_mul, mul_neg, smul_neg,
+    sub_neg_eq_add, smul_eq_mul, smul_add]
+  ring
+
+@[simp]
+lemma angularMomentumSqr_commutation_angularMomentum : ⁅𝐋²[d], 𝐋 i j⁆ = 0 := by
+  simp only [angularMomentumOperatorSqr, smul_lie, sum_lie, leibniz_lie, ← smul_add, comp_smul,
+    comp_add, comp_sub, smul_comp, add_comp, sub_comp, angularMomentum_commutation_angularMomentum,
+    angularMomentumCLM_antisymm _ i, angularMomentumCLM_antisymm j _, symm _ i, symm _ j,
+    sum_smul, ← Finset.smul_sum, Finset.sum_add_distrib, Finset.sum_sub_distrib]
+  abel_nf
+  simp [smul_zero]
 
 end
 end QuantumMechanics
diff --git a/Physlib/QuantumMechanics/Operators/Commutation.lean b/Physlib/QuantumMechanics/Operators/Commutation.lean
index b205399fd4..b9f97910ed 100644
--- a/Physlib/QuantumMechanics/Operators/Commutation.lean
+++ b/Physlib/QuantumMechanics/Operators/Commutation.lean
@@ -7,15 +7,16 @@ module
 
 public import Physlib.Mathematics.KroneckerDelta.Basic
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial
-public import Physlib.QuantumMechanics.Operators.AngularMomentum
+public import Physlib.QuantumMechanics.Operators.Position
+public import Physlib.QuantumMechanics.Operators.Momentum
 /-!
 
 # Commutation relations
 
 ## i. Overview
 
-In this module we compute the commutators for common operators acting on Schwartz maps on `Space d`.
-We also use these relations to prove symmetry of angular momentum on the Schwartz submodule.
+In this module we compute the commutators of position and momentum operators on Schwartz maps
+on `Space d`, including regularized powers of the radius.
 
 Commutator lemmas come in three flavors:
   - 1. `a_commutation_b` lemmas are of the form `⁅a, b⁆ = (⋯)`.
@@ -25,15 +26,6 @@ Commutator lemmas come in three flavors:
 ## 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)`.
-- `angularMomentumHilbertOperator_isSymmetric` : angular momentum is symmetric on the
-    Schwartz submodule of `SpaceDHilbertSpace d`.
 
 ## iii. Table of contents
 
@@ -42,10 +34,6 @@ Commutator lemmas come in three flavors:
   - 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
-- C. Symmetry of Hilbert-space angular momentum
 
 ## iv. References
 
@@ -61,7 +49,7 @@ open KroneckerDelta
 open Bracket
 open SchwartzMap ContinuousLinearMap
 
-variable {d : ℕ} (i j k l : Fin d) (ε : ℝˣ) (s t : ℝ)
+variable {d : ℕ} (i j k : Fin d) (ε : ℝˣ) (s t : ℝ)
 
 /-!
 
@@ -239,122 +227,5 @@ lemma radiusRegPow_commutation_momentumSqr :
       simp_rw [← sub_add, sub_sub, ← add_smul, I_sq, sub_eq_add_neg, ← neg_smul]
       ring_nf
 
-/-!
-
-### B.4. Angular momentum / position
-
--/
-
-lemma angularMomentum_commutation_position :
-    ⁅𝐋 i j, 𝐱 k⁆ = (I * ℏ) • (δ[i,k] • 𝐱 j - δ[j,k] • 𝐱 i) := by
-  trans 𝐱 i ∘L ⁅𝐩 j, 𝐱 k⁆ - 𝐱 j ∘L ⁅𝐩 i, 𝐱 k⁆
-  · simp [angularMomentumOperator, leibniz_lie]
-  simp only [← lie_skew (𝐩 _), comp_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg,
-    position_commutation_momentum, comp_smul, comp_id, smul_sub, symm k _]
-
-@[simp]
-lemma angularMomentum_commutation_radiusRegPow : ⁅𝐋 i j, 𝐫₀[d] ε s⁆ = 0 := by
-  trans 𝐱 i ∘L ⁅𝐩 j, 𝐫₀ ε s⁆ - 𝐱 j ∘L ⁅𝐩 i, 𝐫₀ ε s⁆
-  · simp [angularMomentumOperator, leibniz_lie]
-  simp [← lie_skew (𝐩 _), radiusRegPow_commutation_momentum, comp_neg,
-    ← position_comp_radiusRegPow_commute, ← comp_assoc, position_comp_commute]
-
-lemma angularMomentum_comp_radiusRegPow_commute : 𝐋 i j ∘L 𝐫₀ ε s = 𝐫₀ ε s ∘L 𝐋 i j := by
-  rw [comp_eq_comp_add_commute, angularMomentum_commutation_radiusRegPow, add_zero]
-
-@[simp]
-lemma angularMomentumSqr_commutation_radiusRegPow : ⁅𝐋²[d], 𝐫₀[d] ε s⁆ = 0 := by
-  simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie]
-
-lemma angularMomentumSqr_comp_radiusRegPow_commute : 𝐋² ∘L 𝐫₀[d] ε s = 𝐫₀ ε s ∘L 𝐋² := by
-  rw [comp_eq_comp_add_commute, angularMomentumSqr_commutation_radiusRegPow, add_zero]
-
-/-!
-
-### B.5. Angular momentum / momentum
-
--/
-
-lemma angularMomentum_commutation_momentum :
-    ⁅𝐋 i j, 𝐩 k⁆ = (I * ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) := by
-  trans ⁅𝐱 i, 𝐩 k⁆ ∘L 𝐩 j - ⁅𝐱 j, 𝐩 k⁆ ∘L 𝐩 i
-  · simp [angularMomentumOperator, leibniz_lie]
-  simp only [position_commutation_momentum, smul_comp, id_comp, smul_sub]
-
-lemma momentum_comp_angularMomentum_eq :
-    𝐩 k ∘L 𝐋 i j = 𝐋 i j ∘L 𝐩 k - (I * ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) := by
-  rw [comp_eq_comp_sub_commute, angularMomentum_commutation_momentum]
-
-@[simp]
-lemma angularMomentum_commutation_momentumSqr : ⁅𝐋 i j, 𝐩[d] ⬝ᵥ 𝐩⁆ = 0 := by
-  simp only [dotProduct, mul_def, lie_sum, lie_leibniz, angularMomentum_commutation_momentum,
-    comp_smul, comp_sub, smul_comp, sub_comp, ← smul_add, ← Finset.smul_sum, Finset.sum_add_distrib,
-    Finset.sum_sub_distrib, sum_smul, sub_add_sub_cancel, sub_self, smul_zero]
-
-lemma momentumSqr_comp_angularMomentum_commute : (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j = 𝐋 i j ∘L (𝐩 ⬝ᵥ 𝐩) := by
-  rw [comp_eq_comp_sub_commute, angularMomentum_commutation_momentumSqr, sub_zero]
-
-@[simp]
-lemma angularMomentumSqr_commutation_momentumSqr : ⁅𝐋²[d], 𝐩[d] ⬝ᵥ 𝐩⁆ = 0 := by
-  simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie]
-
-/-!
-
-### B.6. Angular momentum / angular momentum
-
--/
-
-lemma angularMomentum_commutation_angularMomentum : ⁅𝐋 i j, 𝐋 k l⁆ =
-    (I * ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k) := by
-  nth_rw 2 [angularMomentumOperator]
-  simp only [angularMomentum_commutation_position, angularMomentum_commutation_momentum,
-    lie_sub, lie_leibniz, comp_smul, smul_comp, comp_sub, sub_comp, ← smul_add, ← smul_sub]
-  dsimp [angularMomentumOperator]
-  ext
-  simp only [nsmul_eq_mul, smul_apply, sub_apply, add_apply, mul_apply_eq_comp, comp_apply,
-    _root_.natCast_apply, positionCLM_apply, momentumCLM_apply, neg_mul, mul_neg, smul_neg,
-    sub_neg_eq_add, smul_eq_mul, smul_add]
-  ring
-
-@[simp]
-lemma angularMomentumSqr_commutation_angularMomentum : ⁅𝐋²[d], 𝐋 i j⁆ = 0 := by
-  simp only [angularMomentumOperatorSqr, smul_lie, sum_lie, leibniz_lie, ← smul_add, comp_smul,
-    comp_add, comp_sub, smul_comp, add_comp, sub_comp, angularMomentum_commutation_angularMomentum,
-    angularMomentumOperator_antisymm _ i, angularMomentumOperator_antisymm j _, symm _ i, symm _ j,
-    sum_smul, ← Finset.smul_sum, Finset.sum_add_distrib, Finset.sum_sub_distrib]
-  abel_nf
-  simp [smul_zero]
-
-/-!
-## C. Symmetry of Hilbert-space angular momentum
--/
-
-open MeasureTheory SpaceDHilbertSpace SchwartzSubmodule
-
-/-- Reversing the order of position and momentum leaves angular momentum unchanged. -/
-lemma angularMomentumOperator_eq_momentum_position :
-    𝐋 i j = 𝐩 j ∘L 𝐱 i - 𝐩 i ∘L 𝐱 j := by
-  rw [momentum_comp_position_eq, momentum_comp_position_eq, KroneckerDelta.symm j i]
-  simp [angularMomentumOperator]
-
-/-- Each angular momentum component is symmetric on the Schwartz domain. -/
-lemma angularMomentumHilbertOperator_isSymmetric :
-    (angularMomentumHilbertOperator i j).IsSymmetric := by
-  intro ψ φ
-  obtain ⟨f, rfl⟩ := (schwartzEquiv volume).surjective ψ
-  obtain ⟨g, rfl⟩ := (schwartzEquiv volume).surjective φ
-  simp only [angularMomentumHilbertOperator_apply, LinearEquiv.symm_apply_apply,
-    ← Submodule.coe_inner]
-  rw [angularMomentumOperator_apply_fun, map_sub, inner_sub_left,
-    positionCLM_inner, positionCLM_inner, momentumCLM_inner, momentumCLM_inner,
-    ← inner_sub_right, ← map_sub, angularMomentumOperator_eq_momentum_position]
-  rfl
-
-/-- Angular momentum on the Schwartz domain is densely defined and closable. -/
-lemma angularMomentumHilbertOperator_isUnbounded :
-    (angularMomentumHilbertOperator i j).IsUnbounded :=
-  (angularMomentumHilbertOperator_isSymmetric i j).isUnbounded_iff_hasDenseDomain.mpr
-    (angularMomentumHilbertOperator_hasDenseDomain i j)
-
 end
 end QuantumMechanics