Standard subspaces of a Hilbert space

This files defines standard subspaces of a complex Hilbert space: a standard subspace S of H is a closed real subspace S such that S ⊓ i S = ⊥ and S ⊔ i S = ⊤. For a standard subspace, one can define a closable operator x + i y ↦ x - i y and develop an analogue of the Tomita-Takesaki modular theory for von Neumann algebras. By considering inclusions of standard subspaces, one can obtain unitary representations of various Lie groups.

Main definitions and results

• instance : InnerProductSpace ℝ H for InnerProductSpace ℂ H, by restricting the scalar product to its real part

• StandardSubspace as a structure with a ClosedSubmodule for InnerProductSpace ℝ H satisfying IsCyclic and IsSeparating. Actually the interesting cases need CompleteSpace H, but the definition is given for a general case.

• symplComp as a StandardSubspace of the symplectic complement of a standard subspace with respect to ⟪⬝, ⬝⟫.im

• symplComp_symplComp_eq the double symplectic complement is equal to itself

References

• Chap. 2 of Lecture notes by R. Longo

• Oberwolfach report

TODO

Define the Tomita conjugation, prove Tomita's theorem, prove the KMS condition.

noncomputable def scalarSMulCLE (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] (c : ℂˣ) : H ≃L[ℝ] H

the scalar product by a non-zero complex number as a continuous real-linear equivalence.

Equations

• scalarSMulCLE H c = ContinuousLinearEquiv.smulLeft c

@[simp]

theorem scalarSMulCLE_apply (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] (c : ℂˣ) (x : H) : (scalarSMulCLE H c) x = c • x

@[simp]

theorem scalarSMulCLE_symm_apply (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] (c : ℂˣ) (x : H) : (scalarSMulCLE H c).symm x = c⁻¹ • x

@[implicit_reducible]

noncomputable def ClosedSubmodule.instInnerProductSpaceReal {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] : InnerProductSpace ℝ H

H as a real Hilbert space. This instance is declared inside ClosedSubmodule namespace. If one needs this structure (for example when considering standard subspaces), one should just open ClosedSubmodule and not declare another instance.

Equations

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

theorem ClosedSubmodule.inner_real_eq_re_inner {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (x y : H) : inner ℝ x y = (inner ℂ x y).re

def Complex.UnitI : ℂˣ

The imaginary unit as an invertible element.

Equations

• Complex.UnitI = { val := Complex.I, inv := -Complex.I, val_inv := Complex.UnitI._proof_1, inv_val := Complex.UnitI._proof_2 }

@[simp]

theorem Complex.val_inv_UnitI : ↑UnitI⁻¹ = -I

@[simp]

theorem Complex.val_UnitI : ↑UnitI = I

@[reducible, inline]

noncomputable abbrev ClosedSubmodule.mulI {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) : ClosedSubmodule ℝ H

The image of a closed submodule by the multiplication by Complex.I.

Equations

• S.mulI = (ClosedSubmodule.mapEquiv (scalarSMulCLE H Complex.UnitI)) S

@[reducible, inline]

noncomputable abbrev ClosedSubmodule.symplComp {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) : ClosedSubmodule ℝ H

The symplectic complement of a closed submodule with respect to ⟪⬝, ⬝⟫.im, defined as the image of mulI and orthogonal. The proof that this is the symplectic complement is given by mem_symplComp_iff.

Equations

• S.symplComp = S.mulIᗮ

theorem ClosedSubmodule.mem_iff {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) {x : H} : x ∈ S ↔ x ∈ (↑S).carrier

theorem ClosedSubmodule.mem_symplComp_iff {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] {x : H} {S : ClosedSubmodule ℝ H} : x ∈ S.symplComp ↔ ∀ y ∈ S, (inner ℂ y x).im = 0

theorem ClosedSubmodule.mulI_orthogonal_eq_symplComp {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) : Sᗮ.mulI = S.symplComp

theorem ClosedSubmodule.mulI_orthogonal {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) : Sᗮ.mulI = S.mulIᗮ

@[simp]

theorem ClosedSubmodule.mulI_symplComp {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] {S : ClosedSubmodule ℝ H} : S.symplComp.mulI = S.mulI.symplComp

@[simp]

theorem ClosedSubmodule.mulI_mulI_eq {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) : S.mulI.mulI = S

theorem ClosedSubmodule.involutive_mulI {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] : Function.Involutive mulI

@[simp]

theorem ClosedSubmodule.symplComp_symplComp_eq {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] [CompleteSpace H] {S : ClosedSubmodule ℝ H} : S.symplComp.symplComp = S

theorem ClosedSubmodule.mulI_sup {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S T : ClosedSubmodule ℝ H) : (S ⊔ T).mulI = S.mulI ⊔ T.mulI

theorem ClosedSubmodule.mulI_inf {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S T : ClosedSubmodule ℝ H) : (S ⊓ T).mulI = S.mulI ⊓ T.mulI

@[simp]

theorem ClosedSubmodule.symplComp_sup {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S T : ClosedSubmodule ℝ H) : (S ⊔ T).symplComp = S.symplComp ⊓ T.symplComp

@[simp]

theorem ClosedSubmodule.symplComp_inf {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] [CompleteSpace H] (S T : ClosedSubmodule ℝ H) : (S ⊓ T).symplComp = S.symplComp ⊔ T.symplComp

structure StandardSubspace (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type u_1

A standard subspace S of a complex Hilbert space (or just an inner product space) H is a closed real subspace S such that S ⊓ i S = ⊥ and S ⊔ i S = ⊤.

• toClosedSubmodule : ClosedSubmodule ℝ H

  A real closed subspace S.

• IsSeparating : self.toClosedSubmodule ⊓ self.toClosedSubmodule.mulI = ⊥

  S is separating, that is, S ⊓ i S is the trivial subspace.

• IsCyclic : self.toClosedSubmodule ⊔ self.toClosedSubmodule.mulI = ⊤

  S is cyclic, that is, S ⊔ i S is the whole space.

theorem StandardSubspace.ext {H : Type u_1} {inst✝ : NormedAddCommGroup H} {inst✝¹ : InnerProductSpace ℂ H} {x y : StandardSubspace H} (toClosedSubmodule : x.toClosedSubmodule = y.toClosedSubmodule) : x = y

theorem StandardSubspace.ext_iff {H : Type u_1} {inst✝ : NormedAddCommGroup H} {inst✝¹ : InnerProductSpace ℂ H} {x y : StandardSubspace H} : x = y ↔ x.toClosedSubmodule = y.toClosedSubmodule

@[simp]

theorem StandardSubspace.toClosedSubmodule_inj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {S T : StandardSubspace H} : S.toClosedSubmodule = T.toClosedSubmodule ↔ S = T

theorem StandardSubspace.toClosedSubmodule_injective {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Function.Injective toClosedSubmodule

noncomputable def StandardSubspace.mulI {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S : StandardSubspace H) : StandardSubspace H

The image of a standard subspace by the multiplication by Complex.I, bundled as a StandardSubspace.

Equations

• S.mulI = { toClosedSubmodule := S.toClosedSubmodule.mulI, IsSeparating := ⋯, IsCyclic := ⋯ }

noncomputable def StandardSubspace.symplComp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : StandardSubspace H) : StandardSubspace H

The symplectic complement of a standard subspace, bundled as a StandardSubspace.

Equations

• S.symplComp = { toClosedSubmodule := S.toClosedSubmodule.symplComp, IsSeparating := ⋯, IsCyclic := ⋯ }

@[simp]

theorem StandardSubspace.symplComp_symplComp_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : StandardSubspace H) : S.symplComp.symplComp = S

theorem StandardSubspace.involutive_symplComp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Function.Involutive symplComp