FiberCommutant.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Commutants of genuine fiber representations

A global commutation relation passes to the operator fields by their action on all L² vectors. Norm separability then gives one conull set on which the field commutes with the entire represented algebra, and hence its bicommutant.

theorem OAI.KadisonSimilarity.pointwise_field_commute line 25

Source documentation

Commuting L² operators have commuting fields almost everywhere.

theorem pointwise_field_commute
    (T S : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R Q : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hQ : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, S f a = Q a (f a))
    (hcomm : T * S = S * T) :
    ∀ᵐ a ∂μ, R a * Q a = Q a * R a := by
…

theorem OAI.KadisonSimilarity.ae_commutes_fiber_representation line 45

Source documentation

A countable dense family of algebra elements makes the exceptional set independent of the element of the algebra.

theorem ae_commutes_fiber_representation
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : Ω, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R : Ω → H →L[ℂ] H)
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a ∂μ, σ b f a = ρ a b (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hcomm : ∀ b : A, T * σ b = σ b * T) :
    ∀ᵐ a ∂μ, ∀ b : A, R a * ρ a b = ρ a b * R a := by
…

theorem OAI.KadisonSimilarity.ae_mem_fiber_representation_commutant line 69

Source documentation

The same field belongs almost everywhere to the commutant of the von Neumann algebra generated by the genuine fiber representation.

theorem ae_mem_fiber_representation_commutant
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : Ω, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R : Ω → H →L[ℂ] H)
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a ∂μ, σ b f a = ρ a b (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hcomm : ∀ b : A, T * σ b = σ b * T) :
    ∀ᵐ a ∂μ, R a ∈ (representationVonNeumannAlgebra (ρ a)).commutant := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.pointwise_field_commute_on line 86

Source documentation

The field commutation argument also works on a measurable restricted base, while the original operators still act on L² of the full base.

theorem pointwise_field_commute_on
    (s : Set Ω) (hs : MeasurableSet s)
    (T S : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R Q : s → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ,
      ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, T f a = R a (f a))
    (hQ : ∀ f : Lp H 2 μ,
      ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, S f a = Q a (f a))
    (hcomm : T * S = S * T) :
    ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, R a * Q a = Q a * R a := by
…

theorem OAI.KadisonSimilarity.ae_commutes_restricted_fiber_representation line 107

Source documentation

Genuine fiber representations need only exist on their measurable conull base. No representation on the exceptional complement is used. The conclusion remains valid for any measurable restricted base.

theorem ae_commutes_restricted_fiber_representation
    (s : Set Ω) (hs : MeasurableSet s)
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : s, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R : Ω → H →L[ℂ] H)
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, σ b f a = ρ a b (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hcomm : ∀ b : A, T * σ b = σ b * T) :
    ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ,
      ∀ b : A, R a * ρ a b = ρ a b * R a := by
…

theorem OAI.KadisonSimilarity.ae_mem_restricted_fiber_representation_commutant line 135

Source documentation

Restricted-base form of the fiber bicommutant-commutant conclusion.

theorem ae_mem_restricted_fiber_representation_commutant
    (s : Set Ω) (hs : MeasurableSet s)
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : s, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R : Ω → H →L[ℂ] H)
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, σ b f a = ρ a b (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hcomm : ∀ b : A, T * σ b = σ b * T) :
    ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ,
      R a ∈ (representationVonNeumannAlgebra (ρ a)).commutant := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra