IsometricFieldClosure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Membership in the original represented von Neumann algebra passes to the fiber algebra through the actual isometric L² embedding.

theorem OAI.KadisonSimilarity.ae_field_mem_of_isometric_representation_closure line 21

Source documentation

Only the source algebra's actual field action and membership are needed; the fiber fields need not form a simultaneous representation on null sets.

theorem ae_field_mem_of_isometric_representation_closure
    (J : H →ₗᵢ[ℂ] Lp F 2 μ) (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (P : Ω → VonNeumannAlgebra F) (R : A → Ω → F →L[ℂ] F)
    (hR : ∀ b (f : Lp F 2 μ), ∀ᵐ x ∂μ,
      isometricExtension J (σ b) f x = R b x (f x))
    (hmem : ∀ b, ∀ᵐ x ∂μ, R b x ∈ P x)
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ)
    (Q : Ω → F →L[ℂ] F)
    (hQ : ∀ f : Lp F 2 μ, ∀ᵐ x ∂μ, isometricExtension J T f x = Q x (f x)) :
    ∀ᵐ x ∂μ, Q x ∈ P x := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.representationVonNeumannAlgebra