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 by a unit u, as a multiplicative automorphism of the monoid: x ↦ u * x * u⁻¹.

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 onto the centralizer of its image.

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 bicommutants to bicommutants.

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

Conjugation by a unitary U : H ≃ₗᵢ[ℂ] H as a multiplicative automorphism of the algebra H →L[ℂ] H of bounded operators: T ↦ U T U⁻¹.

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 operator exponential: exp (W A W⁻¹) = W (exp A) W⁻¹. Immediate from NormedSpace.exp_units_conj, since lieConj W is conjugation by the unit W.

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 {c · 1 : c ∈ ℂ} of a Hilbert space, the (would-be) center of any von Neumann algebra acting irreducibly.

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 von Neumann algebra (a set of operators) is a factor when its center R ∩ R' is exactly the scalars.

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)

Conjugation preserves factoriality. If a von Neumann algebra R is a factor, so is its conjugate U R U⁻¹. Conjugation is a multiplicative automorphism, so it carries the center R ∩ R' onto the center of U R U⁻¹ and fixes the scalars.

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

The conjugation MulEquiv lieConj U agrees, as a map of operators, with Mathlib's conjugation *-algebra automorphism LinearIsometryEquiv.conjStarAlgEquiv U. This bridges our bare-monoid conjugation to the full StarAlgEquiv.

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 is norm-preserving: ‖lieConj W A‖ = ‖A‖. Since W and W⁻¹ are isometries, conjugation is a similarity that preserves the operator norm; proved directly by bounding both directions.

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 star-algebra automorphism e of A whose underlying map carries the set of a star-subalgebra S onto that of T restricts to a star-algebra equivalence S ≃⋆ₐ[ℂ] T.

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, ⋯⟩