OAI/Analysis/Nuclearity/PositiveStateQuotient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive functionals descend through surjective star homomorphisms when they vanish on the kernel. Positivity is proved by lifting a square root.

  1. theorem OAI.WeakPureInfiniteness.positiveFunctional_descends line 16
  2. theorem OAI.WeakPureInfiniteness.state_descends line 44
  3. theorem OAI.WeakPureInfiniteness.positive_summands_descend line 52

    Source documentation

    Each positive summand of a functional pulled back from a quotient also passes through that quotient.

    theorem positive_summands_descend (q : A →⋆ₐ[ℂ] B) (hq : Function.Surjective q)
    (f : B →ₚ[ℂ] ℂ) (g h : A →ₚ[ℂ] ℂ)
    (hsum : ∀ a, g a + h a = f (q a)) :
    ∃ (g' h' : B →ₚ[ℂ] ℂ),
      (∀ a, g' (q a) = g a) ∧ (∀ a, h' (q a) = h a) ∧
      ∀ b, g' b + h' b = f b := by
…