FiniteTraceCover.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Normal positive functionals for the finite trace cover

Every nonzero projection in an abstract von Neumann algebra is detected by a normal positive state supported on that projection. This constructs the normal positive functionals needed for a later trace cover; it does not assume or assert that finiteness alone supplies a trace.

def OAI.BoundedHochschild.KadisonRingrose.vectorPositiveFunctional line 32
Source documentation
A vector state before normalizing its vector.
```
def vectorPositiveFunctional (π : M →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H) : M →ₚ[ℂ] ℂ where
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.vectorPositiveFunctional_apply line 40
lemma OAI.BoundedHochschild.KadisonRingrose.vectorPositiveFunctional_normal line 44

theorem OAI.BoundedHochschild.KadisonRingrose.exists_normal_state_on_projection line 50

Source documentation

Every nonzero projection supports a normal positive state.

theorem exists_normal_state_on_projection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : IsStarProjection p) (hp0 : p ≠ 0) :
    ∃ ψ : M →ₚ[ℂ] ℂ, TraceInPredual e ψ ∧ ψ 1 = 1 ∧ ψ p = 1 ∧
      ∀ a : M, ψ (p * a * p) = ψ a := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual

lemma OAI.BoundedHochschild.KadisonRingrose.normal_functional_central_null_chain line 105

theorem OAI.BoundedHochschild.KadisonRingrose.exists_normal_positive_central_support line 123

Source documentation

A normal positive functional is faithful on central projections within its central support. This is not a traciality assertion.

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

Mentions: OAI.BoundedHochschild.TraceInPredual

def OAI.BoundedHochschild.KadisonRingrose.HasCentralFaithfulNormalState line 154
Source documentation
A normal state detecting all nonzero central subprojections of p.
```
def HasCentralFaithfulNormalState (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (p : M) : Prop :=
…
```

theorem OAI.BoundedHochschild.KadisonRingrose.exists_central_normal_state_subprojection line 161

Source documentation

Every nonzero central projection contains a nonzero central subprojection on which some normal state is faithful on the center.

theorem exists_central_normal_state_subprojection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {q : M} (hq : IsStarProjection q) (hqc : ∀ a : M, q * a = a * q) (hq0 : q ≠ 0) :
    ∃ p : M, IsStarProjection p ∧ (∀ a : M, p * a = a * p) ∧
      p ≤ q ∧ p ≠ 0 ∧ HasCentralFaithfulNormalState e p := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.HasCentralFaithfulNormalState