Each selected scalar automorphism is identity or conjugation

MathlibAnnex.Analysis.CStarAlgebra.normalPart_semilinear_factors_scalar_types

theorem

Identifies each scalar automorphism of the fixed semilinear factors as identity or conjugation.

Statement

Let be complex Hilbert spaces, and let and be nonzero norm-closed complex -subalgebras acting irreducibly on and , respectively. Neither algebra is assumed unital. For and , define the bounded complex-linear functionals

\begin{aligned} f^A_{x,y}:A&\to\mathbb C,& f^A_{x,y}(a)&=\langle y,a(x)\rangle,\\ f^B_{z,w}:B&\to\mathbb C,& f^B_{z,w}(b)&=\langle w,b(z)\rangle. \end{aligned}

Their normal parts are

\begin{aligned} N(A)&=\{\ker f^A_{x,y}:x,y\in H\setminus\{0\}\},\\ N(B)&=\{\ker f^B_{z,w}:z,w\in K\setminus\{0\}\}. \end{aligned} \tag{1}

For , the relative geometric closure is

c_A(\mathcal D)=\left\{J\in N(A): \bigcap_{I\in\mathcal D} I\subseteq J\right\}. \tag{2}

Define analogously. Let be a specified finite-homeomorphism: a bijection satisfying for every finite . Assume that is infinite-dimensional and that is also forward continuous for arbitrary families:

e\bigl(c_A(\mathcal D)\bigr)\subseteq c_B\bigl(e(\mathcal D)\bigr) \qquad(\mathcal D\subseteq N(A)). \tag{3}

Keep the two semilinear equivalences and their scalar automorphisms fixed by the algebraic realization of this same . Then

(\sigma_1=\mathrm{id}\ \text{or}\ \sigma_1=\mathrm{conj}) \quad\text{and}\quad (\sigma_2=\mathrm{id}\ \text{or}\ \sigma_2=\mathrm{conj}). \tag{4}

Here . The conclusion concerns the scalar automorphisms of these same two maps.

Assumptions

The two nonzero concrete -algebras are norm closed and act irreducibly on their respective Hilbert spaces. They need not be unital. The inner product is conjugate-linear in its first variable. The closure on each normal part is the intersection closure displayed above.

For their scalar field automorphisms of , the semilinear maps satisfy and . They are the lifts fixed in the algebraic realization of the given , with one global direct or swapped orientation. The rank theorem supplies the bound required for this realization.

Full continuity is required only in the forward direction for . Neither full continuity of nor initial continuity of the two semilinear maps is assumed.

Conclusion

Each of is identity or complex conjugation. The conclusion is a conjunction of two alternatives. It does not assert that the two scalar automorphisms are equal.

Main citations

The scalar-type theorem states the two alternatives. The algebraic realization identifies the factors of the given map; the source fixes their scalar automorphisms in the first and second definitions.

Lean source signature (exact)

The preceding variable declarations introduce the spaces, algebras, irreducibility hypotheses, the finite-homeomorphism e, and hdim. They occur in the conclusion through the selected factors. The earlier include hS hT e remains in scope, and include hH hcont additionally retains infinite-dimensionality and forward full continuity as theorem parameters. Thus the absence of an argument list on the next line does not make this an unconditional theorem. These declarations and commands are quoted separately below.

The following contiguous declaration prefix ends before its proof assignment.

theorem normalPart_semilinear_factors_scalar_types :
    (normalPartFirstScalarEquiv S T hS hT e hdim = RingEquiv.refl ℂ ∨
      normalPartFirstScalarEquiv S T hS hT e hdim = starRingAut (R := ℂ)) ∧
    (normalPartSecondScalarEquiv S T hS hT e hdim = RingEquiv.refl ℂ ∨
      normalPartSecondScalarEquiv S T hS hT e hdim = starRingAut (R := ℂ))

Back to the reading-guide item

In the source, S and T denote the algebras and used here, respectively.

In the source	Mathematical meaning
Hilbert spaces and irreducible algebrasvariable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) variable (T : NonUnitalStarSubalgebra ℂ (K →L[ℂ] K)) variable [IsClosed (S : Set (H →L[ℂ] H))] [IsClosed (T : Set (K →L[ℂ] K))] variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) variable (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T))Fixed source	The complex Hilbert spaces carry the nonzero norm-closed irreducible algebras and , called `S`,`T`. The inclusion representations in the last two lines express these irreducible actions.
Finite closure comparison`variable (e : ClosureSpace.FiniteHomeomorph ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))`Fixed source	The same bijection compares the relative closures. For every finite , $e(c_A(\mathcal D))=c_B(e(\mathcal D)).$ Its underlying equivalence is obtained by `toEquiv`; no new map is selected by that projection.
Included geometric inputs`include hS hT e`Fixed source	The two irreducibility hypotheses and are retained as parameters of the later theorem. They also occur as arguments of the selected scalar maps and semilinear maps.
Dimension and forward continuity`variable (hdim : 3 ≤ Module.rank ℂ H) variable (hH : ¬ FiniteDimensional ℂ H) variable (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv) include hH hcont`Fixed source	The bound specifies the selected lifts. Under the present hypotheses it is guaranteed by the rank theorem cited above. The additional hypotheses are infinite-dimensionality of and, for every , $e(c_A(\mathcal D))\subseteq c_B(e(\mathcal D)).$ The final `include` retains these hypotheses. Full continuity of is not assumed.
Inverse scalar structures`local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.toRingHom σ.symm.toRingHom := RingHomInvPair.of_ringEquiv σ local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.symm.toRingHom σ.toRingHom := RingHomInvPair.of_ringEquiv_symm σ`Fixed source	For a scalar automorphism , these instances pair with its inverse in both orders. They make the inverse of a -semilinear equivalence a -semilinear map; they do not impose .
First selected scalar automorphism`def normalPartFirstScalarEquiv : ℂ ≃+* ℂ := Classical.choose (exists_normalPart_first_semilinearEquiv S T hS hT e hdim)`Fixed source	The source defines the fixed automorphism from the same and dimension bound. For the same selected map it is characterized by . It is not selected separately for each vector.
Second selected scalar automorphism`def normalPartSecondScalarEquiv : ℂ ≃+* ℂ := Classical.choose (exists_normalPart_second_semilinearEquiv S T hS hT e hdim)`Fixed source	This is the fixed scalar automorphism of the same selected map , characterized by , from the same inputs. The first and second scalar automorphisms are not identified with each other.
First scalar alternative`(normalPartFirstScalarEquiv S T hS hT e hdim = RingEquiv.refl ℂ ∨ normalPartFirstScalarEquiv S T hS hT e hdim = starRingAut (R := ℂ)) ∧`Fixed source	The first factor obeys $\sigma_1=\mathrm{id}\quad\text{or}\quad\sigma_1=\mathrm{conj},$ where for every complex scalar. The trailing conjunction joins this whole alternative to the next one.
Second scalar alternative`(normalPartSecondScalarEquiv S T hS hT e hdim = RingEquiv.refl ℂ ∨ normalPartSecondScalarEquiv S T hS hT e hdim = starRingAut (R := ℂ)) :=`Fixed source	The second factor obeys $\sigma_2=\mathrm{id}\quad\text{or}\quad\sigma_2=\mathrm{conj}.$ Both alternatives in (4) hold for the fixed selected maps. This theorem alone does not assert .

Exact surrounding source context (separate excerpts)

These separate excerpts record inverse scalar instances, the ambient spaces and algebras, and the included hypotheses. They are not spliced into the declaration prefix.

NormalPartSemilinearRegularity.lean — separate exact context:

local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.toRingHom σ.symm.toRingHom :=
  RingHomInvPair.of_ringEquiv σ
local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.symm.toRingHom σ.toRingHom :=
  RingHomInvPair.of_ringEquiv_symm σ

Back to the reading-guide item

NormalPartSemilinearRegularity.lean — separate exact context:

universe u v
variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
variable (T : NonUnitalStarSubalgebra ℂ (K →L[ℂ] K))
variable [IsClosed (S : Set (H →L[ℂ] H))] [IsClosed (T : Set (K →L[ℂ] K))]
variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))
variable (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T))
variable (e : ClosureSpace.FiniteHomeomorph
  ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))
  ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))

Back to the reading-guide item

NormalPartSemilinearRegularity.lean — separate exact context:

include hS hT e

Back to the reading-guide item

NormalPartSemilinearRegularity.lean — separate exact context:

variable (hdim : 3 ≤ Module.rank ℂ H)
variable (hH : ¬ FiniteDimensional ℂ H)
variable (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous
  ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv)

include hH hcont

Back to the reading-guide item

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation