Imports
/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module
public import Physlib.QuantumMechanics.Operators.UnboundedQuantum system
i. Overview
In non-relativistic quantum mechanics a quantum system is characterized by a Hilbert space
(complete inner product space) and self-adjoint Hamiltonian operator; these data are collected in
the QuantumSystem structure.
Two quantum systems are said to be "unitary equivalent" if there is a unitary bijection between their respective Hilbert spaces which sends one Hamiltonian to the other under conjugation. Unitary equivalent quantum systems are physically indestinguishable, as all operators, states, matrix elements, probabilities, eigenvalues, etc. are in 1-1 correspondence.
ii. Key results
Definitions
QuantumSystem : Structure bundling together a choice of Hilbert space
and self-adjoint Hamiltonian operator.
UnitaryRelation : The unitary equivalence relation.
iii. Table of contents
A. Definition
B. Creation from an essentially self-adjoint operator
C. Zero
D. Unitary equivalence
iv. References
@[expose] public sectionA. Definition
A quantum system is identified by its Hilbert space and self-adjoint Hamiltonian operator.
The complex Hilbert space.
The Hilbert space is a normed, commutative group.
The Hilbert space is a complex inner product space.
The Hilbert space is complete.
The self-adjoint Hamiltonian operator.
structure QuantumSystem where HS : Type* [instNormed : NormedAddCommGroup HS] [instInner : InnerProductSpace ℂ HS] [instComplete : CompleteSpace HS] ℋ : HS →ₗ.[ℂ] HS
ℋ_self_adjoint : IsSelfAdjoint ℋinstance (Q : QuantumSystem) : NormedAddCommGroup Q.HS := Q.instNormedinstance (Q : QuantumSystem) : InnerProductSpace ℂ Q.HS := Q.instInnerinstance (Q : QuantumSystem) : CompleteSpace Q.HS := Q.instCompleteB. Creation from an essentially self-adjoint operator
An essentially self-adjoint operator has a unique self-adjoint extension
(c.f. IsEssentiallySelfAdjoint.unique_self_adjoint_extension).
For this reason, a quantum system can be uniquely associated to an e.s.a. Hamiltonian operator.
Create a quantum system from a Hamiltonian operator which is merely essentially self-adjoint by taking its closure.
def mk_esa {HS : Type*} [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS]
{ℋ : HS →ₗ.[ℂ] HS} (hℋ : IsEssentiallySelfAdjoint ℋ) : QuantumSystem := ⟨HS, ℋ.closure, hℋ⟩C. Zero
instance instZero : Zero QuantumSystem := ⟨EuclideanSpace ℂ (Fin 0), 0, adjoint_zero⟩D. Unitary equivalence
The relation on quantum systems where Q₁ is related to Q₂ if there exists a linear isometry
equivalence e : Q₁.HS ≃ₗᵢ[ℂ] Q₂.HS between the respective Hilbert spaces satisfying
e ∘ Q₁.ℋ ∘ e.symm = Q₂.ℋ.
def UnitaryRelation (Q₁ Q₂ : QuantumSystem) : Prop :=
∃ (e : Q₁.HS ≃ₗᵢ[ℂ] Q₂.HS) (h : Q₁.ℋ.domain.map e.toLinearMap = Q₂.ℋ.domain),
∀ ψ : Q₁.ℋ.domain, e (Q₁.ℋ ψ) = Q₂.ℋ ⟨e ψ, Q₁:QuantumSystemQ₂:QuantumSysteme:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh:Submodule.map (↑e.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainψ:↥Q₁.ℋ.domain⊢ e ↑ψ ∈ Q₂.ℋ.domain All goals completed! 🐙⟩
The relation UnitaryRelation is reflexive.
lemma unitaryRelation_refl (Q : QuantumSystem) : UnitaryRelation Q Q :=
⟨LinearIsometryEquiv.refl _ _, Q:QuantumSystem⊢ Submodule.map (↑(LinearIsometryEquiv.refl ℂ Q.HS).toLinearEquiv) Q.ℋ.domain = Q.ℋ.domain Q:QuantumSystemx✝:Q.HS⊢ x✝ ∈ Submodule.map (↑(LinearIsometryEquiv.refl ℂ Q.HS).toLinearEquiv) Q.ℋ.domain ↔ x✝ ∈ Q.ℋ.domain; All goals completed! 🐙, Q:QuantumSystem⊢ ∀ (ψ : ↥Q.ℋ.domain), (LinearIsometryEquiv.refl ℂ Q.HS) (↑Q.ℋ ψ) = ↑Q.ℋ ⟨(LinearIsometryEquiv.refl ℂ Q.HS) ↑ψ, ⋯⟩ All goals completed! 🐙⟩
The relation UnitaryRelation is symmetric.
lemma unitaryRelation_symm {Q₁ Q₂ : QuantumSystem} (h₁₂ : UnitaryRelation Q₁ Q₂) :
UnitaryRelation Q₂ Q₁ := Q₁:QuantumSystemQ₂:QuantumSystemh₁₂:Q₁.UnitaryRelation Q₂⊢ Q₂.UnitaryRelation Q₁
Q₁:QuantumSystemQ₂:QuantumSysteme:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain:Submodule.map (↑e.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh:∀ (ψ : ↥Q₁.ℋ.domain), e (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e ↑ψ, ⋯⟩⊢ Q₂.UnitaryRelation Q₁
refine ⟨e.symm, Q₁:QuantumSystemQ₂:QuantumSysteme:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain:Submodule.map (↑e.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh:∀ (ψ : ↥Q₁.ℋ.domain), e (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e ↑ψ, ⋯⟩⊢ Submodule.map (↑e.symm.toLinearEquiv) Q₂.ℋ.domain = Q₁.ℋ.domain Q₁:QuantumSystemQ₂:QuantumSysteme:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain:Submodule.map (↑e.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh:∀ (ψ : ↥Q₁.ℋ.domain), e (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e ↑ψ, ⋯⟩x✝:Q₁.HS⊢ x✝ ∈ Submodule.map (↑e.symm.toLinearEquiv) Q₂.ℋ.domain ↔ x✝ ∈ Q₁.ℋ.domain; All goals completed! 🐙, fun ψ₂ ↦ ?_⟩
Q₁:QuantumSystemQ₂:QuantumSysteme:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain:Submodule.map (↑e.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh:∀ (ψ : ↥Q₁.ℋ.domain), e (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e ↑ψ, ⋯⟩ψ₂:↥Q₂.ℋ.domain⊢ ↑Q₂.ℋ ψ₂ = e.toLinearEquiv (↑Q₁.ℋ ⟨e.symm ↑ψ₂, ⋯⟩)
All goals completed! 🐙
The relation UnitaryRelation is transitive.
lemma unitaryRelation_trans {Q₁ Q₂ Q₃ : QuantumSystem} (h₁₂ : UnitaryRelation Q₁ Q₂)
(h₂₃ : UnitaryRelation Q₂ Q₃) : UnitaryRelation Q₁ Q₃ := Q₁:QuantumSystemQ₂:QuantumSystemQ₃:QuantumSystemh₁₂:Q₁.UnitaryRelation Q₂h₂₃:Q₂.UnitaryRelation Q₃⊢ Q₁.UnitaryRelation Q₃
Q₁:QuantumSystemQ₂:QuantumSystemQ₃:QuantumSystemh₂₃:Q₂.UnitaryRelation Q₃e₁₂:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain₁₂:Submodule.map (↑e₁₂.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh✝:∀ (ψ : ↥Q₁.ℋ.domain), e₁₂ (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e₁₂ ↑ψ, ⋯⟩⊢ Q₁.UnitaryRelation Q₃
Q₁:QuantumSystemQ₂:QuantumSystemQ₃:QuantumSysteme₁₂:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain₁₂:Submodule.map (↑e₁₂.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh✝¹:∀ (ψ : ↥Q₁.ℋ.domain), e₁₂ (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e₁₂ ↑ψ, ⋯⟩e₂₃:Q₂.HS ≃ₗᵢ[ℂ] Q₃.HSh_domain₂₃:Submodule.map (↑e₂₃.toLinearEquiv) Q₂.ℋ.domain = Q₃.ℋ.domainh✝:∀ (ψ : ↥Q₂.ℋ.domain), e₂₃ (↑Q₂.ℋ ψ) = ↑Q₃.ℋ ⟨e₂₃ ↑ψ, ⋯⟩⊢ Q₁.UnitaryRelation Q₃
exact ⟨e₁₂.trans e₂₃, Q₁:QuantumSystemQ₂:QuantumSystemQ₃:QuantumSysteme₁₂:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain₁₂:Submodule.map (↑e₁₂.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh✝¹:∀ (ψ : ↥Q₁.ℋ.domain), e₁₂ (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e₁₂ ↑ψ, ⋯⟩e₂₃:Q₂.HS ≃ₗᵢ[ℂ] Q₃.HSh_domain₂₃:Submodule.map (↑e₂₃.toLinearEquiv) Q₂.ℋ.domain = Q₃.ℋ.domainh✝:∀ (ψ : ↥Q₂.ℋ.domain), e₂₃ (↑Q₂.ℋ ψ) = ↑Q₃.ℋ ⟨e₂₃ ↑ψ, ⋯⟩⊢ Submodule.map (↑(e₁₂.trans e₂₃).toLinearEquiv) Q₁.ℋ.domain = Q₃.ℋ.domain Q₁:QuantumSystemQ₂:QuantumSystemQ₃:QuantumSysteme₁₂:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain₁₂:Submodule.map (↑e₁₂.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh✝¹:∀ (ψ : ↥Q₁.ℋ.domain), e₁₂ (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e₁₂ ↑ψ, ⋯⟩e₂₃:Q₂.HS ≃ₗᵢ[ℂ] Q₃.HSh_domain₂₃:Submodule.map (↑e₂₃.toLinearEquiv) Q₂.ℋ.domain = Q₃.ℋ.domainh✝:∀ (ψ : ↥Q₂.ℋ.domain), e₂₃ (↑Q₂.ℋ ψ) = ↑Q₃.ℋ ⟨e₂₃ ↑ψ, ⋯⟩x✝:Q₃.HS⊢ x✝ ∈ Submodule.map (↑(e₁₂.trans e₂₃).toLinearEquiv) Q₁.ℋ.domain ↔ x✝ ∈ Q₃.ℋ.domain; All goals completed! 🐙, Q₁:QuantumSystemQ₂:QuantumSystemQ₃:QuantumSysteme₁₂:Q₁.HS ≃ₗᵢ[ℂ] Q₂.HSh_domain₁₂:Submodule.map (↑e₁₂.toLinearEquiv) Q₁.ℋ.domain = Q₂.ℋ.domainh✝¹:∀ (ψ : ↥Q₁.ℋ.domain), e₁₂ (↑Q₁.ℋ ψ) = ↑Q₂.ℋ ⟨e₁₂ ↑ψ, ⋯⟩e₂₃:Q₂.HS ≃ₗᵢ[ℂ] Q₃.HSh_domain₂₃:Submodule.map (↑e₂₃.toLinearEquiv) Q₂.ℋ.domain = Q₃.ℋ.domainh✝:∀ (ψ : ↥Q₂.ℋ.domain), e₂₃ (↑Q₂.ℋ ψ) = ↑Q₃.ℋ ⟨e₂₃ ↑ψ, ⋯⟩⊢ ∀ (ψ : ↥Q₁.ℋ.domain), (e₁₂.trans e₂₃) (↑Q₁.ℋ ψ) = ↑Q₃.ℋ ⟨(e₁₂.trans e₂₃) ↑ψ, ⋯⟩ All goals completed! 🐙⟩
The relation UnitaryRelation is an equivalence relation.
lemma unitaryRelation_equiv : Equivalence UnitaryRelation where
refl := unitaryRelation_refl
symm := unitaryRelation_symm
trans := unitaryRelation_trans
The setoid of quantum systems with UnitaryRelation for equivalence relation.
instance QuantumSystemSetoid : Setoid QuantumSystem := ⟨UnitaryRelation, unitaryRelation_equiv⟩