The geometric structure of a representation image as a component closure

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.imageGeometricStructureHomeomorph

def

Identifies the geometric structure of a representation image with a component closure.

Statement

Let be a complex C*-algebra, possibly without an identity, and let be a nonzero -representation on a complete complex Hilbert space. Let be a geometric-structure point whose component satisfies

\bigcap_{I\in C(I_0)}I=\ker\pi. \tag{1}

With the inherited C*-algebra structure on , there is a specified closure-space homeomorphism

E_{\pi,I_0}:S(\pi(A))\longrightarrow c_A(C(I_0)). \tag{2}

The target carries the subspace closure from . The exact declaration requires nonzero action and the explicit equality (1); it does not require irreducibility of in addition to them.

Definition

For any algebra here, denotes kernels of extreme points of the closed unit ball in the Banach dual , using real convexity. The geometric identification is supplied by the extreme-functional kernel characterization. Its closure is , including the empty family.

Regard as a map from onto its image . The defining map and its inverse are

E_{\pi,I_0}(J)=\pi^{-1}(J),\qquad E_{\pi,I_0}^{-1}(I)=\pi(I).

Here and . The target is the ambient closure of the whole specified component, equipped with subspace closure. It is not the component alone.

The surjective preimage construction supplies the homeomorphism onto the geometric points containing . The component-closure identification uses (1) to identify that target with , without changing the point map. The image's nontriviality and compatible order are supplied by the image construction, not additional hypotheses.

Assumptions

The displayed scope requires a nonzero complex C*-algebra with its compatible order and a complete complex Hilbert space . The representation is nonzero, and the component of the specified point satisfies (1). Neither faithfulness nor irreducibility is an additional hypothesis. The cited image construction equips with its C*-algebra structure and compatible order.

Conclusion

The output bundles the displayed preimage map and its image-map inverse, with full closure continuity in both directions. The target is exactly with the inherited closure; it is not a claim that is closed.

Main citations

Exact full definition: NonUnitalCStarRepresentation.imageGeometricStructureHomeomorph.
SurjectivePreimage.lean, geometricStructurePreimageHomeomorph: the first stage of the construction.
ImageSubspace.lean, closure_component_eq_hull_ker and the value and closure lemmas following the definition: the target identification and the concrete action.
Ryotaro Tanaka, arXiv:2504.05551v1, Theorem 5.17. This card uses the quotient of the original algebra and its representation image.
Surjective preimage construction: the exact map and inverse.
Actual C*-image structure.

Lean source signature (exact)

The full definition below is copied from the pinned source.

def imageGeometricStructureHomeomorph (hpi : pi.IsNonzero)
    (I : NormedSpace.GeometricStructureSpace ℂ A)
    (hI : NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A I) =
      ((imageSubspaceContinuousMap pi).ker : Set A)) :
    ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range pi))
      ((NormedSpace.geometricStructureClosure ℂ A).subspace
        ((NormedSpace.geometricStructureClosure ℂ A).closure
          ((NormedSpace.geometricStructureClosure ℂ A).component I))) := by
  letI : Nontrivial (NonUnitalStarAlgHom.range pi) := nontrivial_image_of_isNonzero pi hpi
  letI : PartialOrder (NonUnitalStarAlgHom.range pi) := _root_.CStarAlgebra.spectralOrder (NonUnitalStarAlgHom.range pi)
  letI : StarOrderedRing (NonUnitalStarAlgHom.range pi) := _root_.CStarAlgebra.spectralOrderedRing (NonUnitalStarAlgHom.range pi)
  let q := (NonUnitalStarAlgHom.rangeRestrict pi)
  have hq : Function.Surjective q := rangeRestrict_surjective pi
  have hker : ((imageSubspaceContinuousMap q).ker : Set A) =
      ((imageSubspaceContinuousMap pi).ker : Set A) := by
    ext a
    change q a = 0 ↔ pi a = 0
    constructor
    · intro h
      exact congrArg Subtype.val h
    · intro h
      apply Subtype.ext
      change pi a = 0
      exact h
  have htarget : ClosureSpace.HullKernel.hull (NormedSpace.geometricStructureFamily ℂ A)
      ((imageSubspaceContinuousMap q).ker : Set A) =
        (NormedSpace.geometricStructureClosure ℂ A).closure
          ((NormedSpace.geometricStructureClosure ℂ A).component I) := by
    rw [hker, closure_component_eq_hull_ker pi I hI]
  exact (geometricStructurePreimageHomeomorph q hq).trans
    ((ClosureSpace.Homeomorph.refl (NormedSpace.geometricStructureClosure ℂ A)).subspace
      _ _ (fun J => Set.ext_iff.mp htarget J))

In the source	Mathematical meaning
Surrounding Exact declaration`A`, `H` and their instances	The nonzero complex C*-algebra with compatible order, and the complete complex Hilbert space . A unit is not required.
Exact declaration`pi`, `hpi`, `I`, `hI`	The nonzero representation , the point , and the equality . The representation need not be faithful or irreducible.
Exact declaration`NonUnitalStarAlgHom.range pi` and the local instances	The image , with its inherited C*-algebra structure, nontriviality, and compatible spectral order.
Exact declaration`q := NonUnitalStarAlgHom.rangeRestrict pi`	The same action , now with codomain .
Exact declaration`hq : Function.Surjective q`	Every element of equals for some .
Exact declaration`hker`	The equality as subsets of . Restricting the codomain does not change this kernel.
Exact declaration`geometricStructurePreimageHomeomorph q hq`	The homeomorphism from onto , with inverse .
Exact declaration`htarget`	The set equals , by the component-intersection hypothesis.
Exact declaration`Homeomorph.refl ... .subspace`	The identity on these geometric points, regarded in the target with its inherited closure.
Final Exact declaration`.trans`	First take , then identify its codomain with . The point map and its inverse remain those displayed above.

Exact surrounding source context (separate excerpts)

Source lines 32–32:

variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]

Source lines 33–33:

variable [PartialOrder A] [StarOrderedRing A]

Source lines 34–34:

variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

Source lines 35–35:

variable (pi : NonUnitalCStarRepresentation A H)

Source line 45 supplies the image C*-algebra instance used by the declaration; it is not an additional hypothesis:

attribute [local instance] HomKernelQuotient.imageCStarAlgebra

The continuous-map wrapper in the same source, lines 37–43, is copied separately; it retains the given action with the norm bound supplied by NonUnitalStarAlgHom.norm_apply_le:

private def imageSubspaceContinuousMap {B : Type*} [NonUnitalCStarAlgebra B]
    (q : A →⋆ₙₐ[ℂ] B) : A →L[ℂ] B :=
  LinearMap.mkContinuous
    { toFun := q, map_add' := map_add q, map_smul' := map_smul q }
    1 (fun a => by
      change ‖q a‖ ≤ 1 * ‖a‖
      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le q a)

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

Technical documentation