Physicslib4.Operators.Conjugation

Conjugation by a unit and by a unitary

Spacetime-agnostic operator-algebra machinery used by the geometric-covariance results of algebraic QFT (both the Minkowski and curved Haag-Kastler nets), kept here so neither net depends on the other.

• Units.conjMulEquiv u — conjugation by a monoid unit, x ↦ u x u⁻¹, as a multiplicative automorphism.
• MulEquiv.image_centralizer / image_centralizer_centralizer — a multiplicative automorphism maps centralizers (hence bicommutants) to those of the image.
• Physicslib4.lieConj U — conjugation by a unitary U : H ≃ₗᵢ[ℂ] H on B(H), with lieConj_apply and the bridge lieConj_apply_eq_conjStarAlgEquiv to Mathlib's LinearIsometryEquiv.conjStarAlgEquiv. Its algebra/metric structure is recorded by lieConj_one, lieConj_add, lieConj_smul, lieConj_star, exp_lieConj, and the norm preservation norm_lieConj.
• Physicslib4.scalarOperators / IsFactor and IsFactor.conj — the factor (trivial-center) property and its preservation under conjugation.
• Physicslib4.restrictStarAlgEquiv — a *-automorphism carrying one star-subalgebra's set onto another's restricts to a *-algebra equivalence.

def Units.conjMulEquiv {M : Type u_1} [Monoid M] (u : Mˣ) : M ≃* M

Conjugation x ↦ u x u⁻¹ by an invertible element u of a monoid, as a multiplicative automorphism.

It preserves products, (u x u⁻¹)(u y u⁻¹) = u (xy) u⁻¹, and its inverse is conjugation by u⁻¹. In operator algebra u is an invertible operator, typically a unitary implementing a symmetry, and the automorphism is the induced change of frame on observables, A ↦ u A u⁻¹.

Implementation note: u is a Units element, so u⁻¹ is a genuine two-sided inverse. Only the multiplicative structure is recorded; lieConj specialises this to unitaries on a Hilbert space.

Blueprint: def:unitary-conjugation

Equations

• u.conjMulEquiv = { toFun := fun (x : M) => ↑u * x * ↑u⁻¹, invFun := fun (x : M) => ↑u⁻¹ * x * ↑u, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem Units.conjMulEquiv_apply {M : Type u_1} [Monoid M] (u : Mˣ) (x : M) : u.conjMulEquiv x = ↑u * x * ↑u⁻¹

theorem MulEquiv.image_centralizer {M : Type u_1} [Mul M] (φ : M ≃* M) (S : Set M) : ⇑φ '' S.centralizer = (⇑φ '' S).centralizer

A multiplicative automorphism φ maps the centralizer of a set S onto the centralizer of φ(S).

The centralizer, or commutant, S' is the set of elements commuting with every element of S. An element commutes with every s ∈ S exactly when its image commutes with every φ(s), so φ(S') = φ(S)'. This is the algebraic fact behind geometric covariance of the local von Neumann algebras: conjugation by a unitary commutes with taking commutants.

Implementation note: the centralizer is Mathlib's Set.centralizer, and only multiplication is used, so the statement holds in any Mul structure.

Blueprint: lmm:automorphism-commutant

theorem MulEquiv.image_centralizer_centralizer {M : Type u_1} [Mul M] (φ : M ≃* M) (S : Set M) : ⇑φ '' S.centralizer.centralizer = (⇑φ '' S).centralizer.centralizer

A multiplicative automorphism φ maps the bicommutant S'' of a set onto the bicommutant of φ(S).

This is image_centralizer applied twice. For a set S of bounded operators closed under adjoints, S'' is the von Neumann algebra generated by S and 𝟙 (by von Neumann's bicommutant theorem), so conjugation by a unitary U carries the von Neumann algebra generated by S onto the one generated by U S U⁻¹. Through this lemma the local von Neumann algebras R(B) inherit geometric covariance from the net.

Implementation note: the bicommutant is Set.centralizer (Set.centralizer S); the lemma does not use the bicommutant theorem.

Blueprint: lmm:automorphism-commutant

noncomputable def Physicslib4.lieConj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Uop : H ≃ₗᵢ[ℂ] H) : (H →L[ℂ] H) ≃* (H →L[ℂ] H)

Conjugation T ↦ U T U⁻¹ by a unitary U, as a multiplicative automorphism of the bounded operators on H.

If a symmetry acts on state vectors by U, it acts on observables by T ↦ U T U⁻¹; this is how a unitary representation of the Poincaré group, or of a group of isometries, moves the local algebras of a net. The map preserves products, sums, scalar multiples, adjoints and the operator norm (lieConj_add, lieConj_smul, lieConj_star, norm_lieConj), and commutes with the exponential (exp_lieConj).

Implementation note: the unitary is H ≃ₗᵢ[ℂ] H and the map is Units.conjMulEquiv of the corresponding unit of H →L[ℂ] H, so only the multiplicative structure is in the type. The pointwise formula is lieConj_apply, and lieConj_apply_eq_conjStarAlgEquiv identifies it with Mathlib's *-algebra automorphism LinearIsometryEquiv.conjStarAlgEquiv.

Blueprint: def:unitary-conjugation

Equations

• Physicslib4.lieConj Uop = (↑Uop).toUnit.conjMulEquiv

@[simp]

theorem Physicslib4.lieConj_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Uop : H ≃ₗᵢ[ℂ] H) (T : H →L[ℂ] H) (x : H) : ((lieConj Uop) T) x = Uop (T (Uop.symm x))

theorem Physicslib4.exp_lieConj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (W : H ≃ₗᵢ[ℂ] H) (A : H →L[ℂ] H) : NormedSpace.exp ((lieConj W) A) = (lieConj W) (NormedSpace.exp A)

Conjugation by a unitary commutes with the exponential: exp(W A W⁻¹) = W exp(A) W⁻¹ for every bounded operator A.

Each term of the exponential series satisfies (W A W⁻¹)ⁿ = W Aⁿ W⁻¹, and conjugation is continuous. With A = itP and lieConj_smul it gives exp(it W P W⁻¹) = W exp(itP) W⁻¹: the conjugate of the unitary group generated by a bounded P is the group generated by W P W⁻¹.

Implementation note: the exponential is Mathlib's NormedSpace.exp, and the proof is NormedSpace.exp_units_conj, since lieConj W is conjugation by the unit W. The series converges because H is complete.

Blueprint: def:unitary-conjugation

theorem Physicslib4.lieConj_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H ≃ₗᵢ[ℂ] H) (c : ℂ) (A : H →L[ℂ] H) : (lieConj W) (c • A) = c • (lieConj W) A

Conjugation by a unitary is ℂ-linear: lieConj W (c • A) = c • lieConj W A.

@[simp]

theorem Physicslib4.lieConj_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H ≃ₗᵢ[ℂ] H) : (lieConj W) 1 = 1

Conjugation by a unitary fixes the identity: lieConj W 1 = 1.

theorem Physicslib4.lieConj_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H ≃ₗᵢ[ℂ] H) (A B : H →L[ℂ] H) : (lieConj W) (A + B) = (lieConj W) A + (lieConj W) B

Conjugation by a unitary is additive: lieConj W (A + B) = lieConj W A + lieConj W B.

def Physicslib4.scalarOperators (H : Type u_2) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Set (H →L[ℂ] H)

The scalar operators on H: the multiples c𝟙 of the identity, c ∈ ℂ.

They commute with every operator, so they lie in the center of every algebra that contains them. An algebra whose center is exactly the scalars is a factor (IsFactor). For an irreducible representation the commutant of its image is ℂ𝟙 itself (Schur's lemma).

Implementation note: the set is {T | ∃ c : ℂ, T = c • 1} in H →L[ℂ] H, and needs no completeness of H.

Blueprint: def:factor

Equations

• Physicslib4.scalarOperators H = {T : H →L[ℂ] H | ∃ (c : ℂ), T = c • 1}

def Physicslib4.IsFactor {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (R : Set (H →L[ℂ] H)) : Prop

A set R of bounded operators is a factor when its center R ∩ R' is exactly the scalar operators.

Here R' is the commutant, the operators commuting with every element of R. For a von Neumann algebra this is the usual notion of a factor: it cannot be split as a direct sum of two smaller von Neumann algebras by a central projection. In algebraic quantum field theory the local algebras R(B) of many models are factors. The library proves that this property is preserved by unitary conjugation (IsFactor.conj), hence constant along the orbit of a region under the symmetry group (HaagKastlerNet.localVonNeumann_isFactor_smul), and relates it to irreducible inclusions (HaagKastlerNet.isFactor_of_isIrreducibleInclusion).

Implementation note: the definition applies to any set of operators, not only to von Neumann algebras, with the commutant given by Set.centralizer; since the center must equal the scalars, a factor contains 𝟙.

Blueprint: def:factor

Equations

• Physicslib4.IsFactor R = (R ∩ R.centralizer = Physicslib4.scalarOperators H)

theorem Physicslib4.lieConj_image_scalarOperators {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Uop : H ≃ₗᵢ[ℂ] H) : ⇑(lieConj Uop) '' scalarOperators H = scalarOperators H

Conjugation by a unitary fixes the scalar operators setwise: U (c · 1) U⁻¹ = c · 1.

theorem Physicslib4.IsFactor.conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Uop : H ≃ₗᵢ[ℂ] H) {R : Set (H →L[ℂ] H)} (h : IsFactor R) : IsFactor (⇑(lieConj Uop) '' R)

If R is a factor and U is unitary, then U R U⁻¹ is a factor.

Conjugation by U is a multiplicative bijection, so it carries the center R ∩ R' onto the center of U R U⁻¹ (MulEquiv.image_centralizer), and it fixes every scalar operator, U (c𝟙) U⁻¹ = c𝟙. Combined with geometric covariance, R(L·B) = U(L) R(B) U(L)⁻¹, this shows that being a factor is constant along the orbit of a region under the symmetry group.

Implementation note: U R U⁻¹ is the image lieConj Uop '' R, and H need not be complete.

Blueprint: lmm:factor-conj

theorem Physicslib4.lieConj_apply_eq_conjStarAlgEquiv {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (Uop : H ≃ₗᵢ[ℂ] H) (T : H →L[ℂ] H) : (lieConj Uop) T = Uop.conjStarAlgEquiv T

Conjugation by a unitary U, lieConj U, agrees on every operator with Mathlib's conjugation *-algebra automorphism LinearIsometryEquiv.conjStarAlgEquiv U.

Both send T to U T U⁻¹. The point is that the second is a *-algebra automorphism, so the equation transfers preservation of adjoints to lieConj U (lieConj_star), and lets the local algebras of a net be moved by a *-algebra equivalence (restrictStarAlgEquiv).

Implementation note: lieConj U is only a MulEquiv; this lemma is the bridge to the StarAlgEquiv, used, for example, in lieConj_star.

Blueprint: def:unitary-conjugation

theorem Physicslib4.lieConj_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (W : H ≃ₗᵢ[ℂ] H) (A : H →L[ℂ] H) : (lieConj W) (star A) = star ((lieConj W) A)

Conjugation by a unitary is star-preserving: lieConj W (star A) = star (lieConj W A). It agrees with Mathlib's conjugation *-automorphism, which preserves the adjoint.

theorem Physicslib4.norm_lieConj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H ≃ₗᵢ[ℂ] H) (A : H →L[ℂ] H) : ‖(lieConj W) A‖ = ‖A‖

Conjugation by a unitary preserves the operator norm: ‖W A W⁻¹‖ = ‖A‖.

Since W and W⁻¹ are isometries, ‖W A W⁻¹ ψ‖ = ‖A W⁻¹ψ‖ ≤ ‖A‖ ‖ψ‖, and the reverse inequality follows in the same way from A = W⁻¹ (W A W⁻¹) W. So conjugation is an isometric automorphism of the C*-algebra of bounded operators.

Implementation note: both inequalities are proved by ContinuousLinearMap.opNorm_le_bound, and H need not be complete.

Blueprint: def:unitary-conjugation

def Physicslib4.restrictStarAlgEquiv {A : Type u_2} [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] (e : A ≃⋆ₐ[ℂ] A) {S T : StarSubalgebra ℂ A} (hfwd : ∀ x ∈ S, e x ∈ T) (hbwd : ∀ y ∈ T, e.symm y ∈ S) : ↥S ≃⋆ₐ[ℂ] ↥T

A *-algebra automorphism e that maps a *-subalgebra S into T, and whose inverse maps T into S, restricts to a *-algebra isomorphism from S onto T.

This is how a symmetry acts between local algebras: conjugation by the unitary U(L) is a *-automorphism of the bounded operators that carries the local von Neumann algebra R(B) onto R(L·B), and so gives a *-isomorphism between the two (HaagKastlerNet.localVonNeumannEquiv).

Implementation note: the two inclusion hypotheses hfwd and hbwd make the restriction and its inverse well defined; @[simps! apply] generates the lemma that the restriction acts as e.

Blueprint: lmm:restrict-star-alg-equiv

Equations

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

@[simp]

theorem Physicslib4.restrictStarAlgEquiv_apply {A : Type u_2} [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] (e : A ≃⋆ₐ[ℂ] A) {S T : StarSubalgebra ℂ A} (hfwd : ∀ x ∈ S, e x ∈ T) (hbwd : ∀ y ∈ T, e.symm y ∈ S) (x : ↥S) : (restrictStarAlgEquiv e hfwd hbwd) x = ⟨e ↑x, ⋯⟩