TraceInvariantVectors.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar invariant vectors in the trace completion

Relative convex averaging identifies invariant vectors without assuming that a Hilbert-space vector is represented by a bounded algebra element.

theorem OAI.KadisonKastler.inner_trace_scalar_of_relative_invariant line 21

Source documentation

An invariant coefficient has the same value at an element and its scalar trace, by continuity on the actual relative orbit hull.

theorem inner_trace_scalar_of_relative_invariant
    (τ : FaithfulTracialState (Algebra M)) (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (hτ : FiniteVectorTrace τ)
    (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (v : E) (hinv : ∀ (u : unitary R) x,
      inner ℂ v (J (φ u * x * star (φ u))) = inner ℂ v (J x))
    (x : Algebra M) :
    inner ℂ v (J (τ.toLinearMap x • (1 : Algebra M))) = inner ℂ v (J x) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.scalar_of_relative_invariant_coefficients line 44

Source documentation

In a dense tracial realization, invariant coefficients force the vector to be a scalar multiple of the trace vector.

theorem scalar_of_relative_invariant_coefficients
    (τ : FaithfulTracialState (Algebra M)) (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (hτ : FiniteVectorTrace τ)
    (hdense : DenseRange J)
    (htrace : ∀ x, inner ℂ (J 1) (J x) = τ.toLinearMap x)
    (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (v : E) (hinv : ∀ (u : unitary R) x,
      inner ℂ v (J (φ u * x * star (φ u))) = inner ℂ v (J x)) :
    ∃ z : ℂ, v = z • J 1 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.concreteTraceEmbedding_inner line 65

theorem OAI.KadisonKastler.concreteTrace_inner_conjugation_of_fixed line 73

Source documentation

A vector fixed by one unitary conjugation has an invariant coefficient.

theorem concreteTrace_inner_conjugation_of_fixed
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (u : unitary (Algebra M)) (v : ConcreteTraceHilbert hM)
    (hfixed : concreteTraceLeftAction hM u
      (concreteTraceRightAction hM (star (u : Algebra M)) v) = v)
    (x : Algebra M) :
    inner ℂ v (concreteTraceEmbedding hM
      ((u : Algebra M) * x * star (u : Algebra M))) =
        inner ℂ v (concreteTraceEmbedding hM x) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert, OAI.KadisonKastler.concreteTraceLeftAction, OAI.KadisonKastler.concreteTraceRightAction, OAI.KadisonKastler.concreteTraceEmbedding

theorem OAI.KadisonKastler.concreteTrace_scalar_of_conjugation_invariant line 100

Source documentation

The actual two-sided unitary action of an irreducible subalgebra has only scalar trace vectors as invariant vectors.

theorem concreteTrace_scalar_of_conjugation_invariant
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (v : ConcreteTraceHilbert hM)
    (hinv : ∀ u : unitary R,
      concreteTraceLeftAction hM (φ u)
        (concreteTraceRightAction hM (star (φ u)) v) = v) :
    ∃ z : ℂ, v = z • concreteTraceEmbedding hM 1 := by
…