NormalTraceFaithfulness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A normal trace faithful on the center is faithful on the whole algebra.

lemma OAI.BoundedHochschild.KadisonRingrose.normal_tracial_null_projection_join line 21

theorem OAI.BoundedHochschild.KadisonRingrose.normal_trace_largest_null_projection line 33

Source documentation

The largest projection annihilated by a normal trace is central.

theorem normal_trace_largest_null_projection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (τ : M →ₚ[ℂ] ℂ) (hτ : TraceInPredual e τ)
    (htr : ∀ a b : M, τ (a * b) = τ (b * a)) :
    ∃ p : M, IsStarProjection p ∧ (∀ a : M, p * a = a * p) ∧ τ p = 0 ∧
      ∀ q : M, IsStarProjection q → τ q = 0 → q ≤ p := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual

theorem OAI.BoundedHochschild.KadisonRingrose.normal_trace_faithful_of_center line 89

Source documentation

Faithfulness on central projections suffices for a normal trace.

theorem normal_trace_faithful_of_center (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (τ : M →ₚ[ℂ] ℂ) (hτ : TraceInPredual e τ)
    (htr : ∀ a b : M, τ (a * b) = τ (b * a))
    (hcenter : ∀ p : M, IsStarProjection p → (∀ a : M, p * a = a * p) →
      τ p = 0 → p = 0) : ∀ a : M, τ (star a * a) = 0 → a = 0 := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual