OAI/Analysis/Nuclearity/PureStateQuotient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive decompositions of a pulled-back pure state are trivial. This supplies the face argument for pure states on represented quotients.

  1. theorem OAI.WeakPureInfiniteness.pure_pullback_positive_summand line 17
  2. theorem OAI.WeakPureInfiniteness.exists_pure_state_pullback line 39

    Source documentation

    Pullback through a quotient preserves purity.

    theorem exists_pure_state_pullback (q : A →⋆ₐ[ℂ] B) (hq : Function.Surjective q)
    (f : B →ₚ[ℂ] ℂ) (hf : f 1 = 1)
    (hp : PureStateExcision.ofPositiveState f hf ∈
      (PureStateExcision.realStateCarrier (A := B)).extremePoints ℝ) :
…

    Mentions: OAI.PureStateExcision.ofPositiveState, OAI.PureStateExcision.realStateCarrier