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.

Main citations

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

Here Limit is , IsPureState Limit phi and ... psi specify the pure states, and alpha : Limit ≃⋆ₐ[ℂ] Limit is . The source unitary v is in the finite-set condition. The full right-hand side below the declaration name includes both the state equation and this approximation condition.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:395ec0494a4bb733050d7af49df8a7f8f5401408da63357e77d640e03a14a1fb

Card revision: 1 · SHA-256: 094d318ed67743b2eb9ece586df619117001cc2f39a6893f0651e14cf6567c52

Exposition revision: 1 · SHA-256: b52e1fdd8374862f7d1cec368978c2039bd508f13aeed66f82b0b4ede2cc742f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 4dbef65c00476bf6c6fac11ae2c9fd2806a3213f9335e9243c7bb962a321d950