MATHLIBANNEX / CANONICAL DECLARATION CARD

Approximately inner homogeneity of pure CAR states

MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity

def

The homogeneity property asks for exact state transport by an automorphism that is locally approximable by inner automorphisms.

Statement

Let be the completed CAR algebra, the norm completion of the matrix stages under , with the fixed coordinate reindexing. A state means a positive continuous complex-linear functional taking value at the identity; a pure state is an extreme point of this convex state space. The property of pure-state homogeneity says that, for every pair of pure states on , there is a complex star automorphism such that for every . In addition, for every finite and every , there is with for all .

Definition

The first requirement transports the state exactly, with the stated composition direction. The second is point-norm approximate innerness: a finite amount of algebra data can be moved almost as moves it. Both requirements concern the same . No continuous path of unitaries is part of this definition.

Assumptions

The algebra is the fixed completed CAR algebra. The two functionals are pure states in the sense specified above. The automorphism is chosen for the state pair before the finite set and the error tolerance are given.

Conclusion

The equality is . One unitary approximates on the entire chosen finite set; that unitary may change with the finite set and tolerance.

This declaration defines a property; the separate CAR homogeneity theorem proves it. It does not assert that itself is inner or that implementing unitaries converge. The proposition about all simple separable unital C*-algebras named Kishimoto–Ozawa–Sakai is a different, more broadly quantified source definition.

Main citations

Supporting route explanation

Lean source signature (exact)

def PureStateHomogeneity : Prop :=
  ∀ (phi psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit phi →
    MathlibAnnex.CStarAlgebra.IsPureState Limit psi →
      ∃ alpha : Limit ≃⋆ₐ[ℂ] Limit,
        (∀ a : Limit, phi (alpha a) = psi a) ∧
        ∀ (F : Finset Limit) (epsilon : ℝ), 0 < epsilon →
          ∃ v : unitary Limit, ∀ a ∈ F,
            ‖alpha a - (v : Limit) * a * star (v : Limit)‖ < epsilon
In the source Mathematical meaning
PureStateHomogeneity : Prop A property of the fixed CAR algebra , rather than an automorphism or a proof that the property holds.
∀ (phi psi : Limit →L[ℂ] ℂ) For every pair of continuous complex-linear functionals .
IsPureState Limit phi → IsPureState Limit psi → Restrict to states that are positive, normalized and extreme in the real convex state space.
∃ alpha : Limit ≃⋆ₐ[ℂ] Limit One bijective complex-linear star algebra map is chosen for the pair of pure states.
∀ a : Limit, phi (alpha a) = psi a For every , , that is in this direction.
∀ (F : Finset Limit) (epsilon : ℝ), 0 < epsilon → For every finite and every , after has already been chosen.
∃ v : unitary Limit, ∀ a ∈ F, ‖alpha a - (v : Limit) * a * star (v : Limit)‖ < epsilon There is one unitary (named v) with for every . The unitary may depend on ; is common to all tests. This is point-norm approximate innerness.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity

Accepted content SHA-256: a54ff0f62bf2e543c952a693b85f5dd4c792d9d2f45fa97c294b41d0a5462b8e

Accepted source guide SHA-256: 6aad4a9c09c84eae33964227ced7034af6d725e23c16a2ac2a8b75f032457f21

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑