RegularCoreCommutant.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The regular crossed-product commutant and fixed algebra

The sole input is the commutant-generator theorem for a covariant representation of a von Neumann algebra. See Takesaki, Theory of Operator Algebras II (2003), Theorem X.1.21, and Van Daele, Continuous Crossed Products and Type III von Neumann Algebras (1978), Part I, Theorem 3.11. The exact covariant-implementation formula is also stated in Takesaki's author notes Structure of von Neumann Algebras of Type III, Lecture 1, Theorem 1.3(ii), pp. 10--11: https://www.imsc.res.in/~sunder/mtnotes.pdf

Its generators here are constant operators from P' and the actual operators f(t) ↦ U(s) f(t+s). The fixed-algebra equality is proved below from this input and double commutants; it is not an input.

def OAI.KadisonKastler.regularCommutantGenerators line 35
Source documentation
The concrete generators on the commutant side of the regular crossed-product commutation theorem.
```
def regularCommutantGenerators
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) (P : VonNeumannAlgebra H) :
    Set (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
def OAI.KadisonKastler.regularCommutantAlgebra line 43
Source documentation
The actual von Neumann algebra generated by the commutant generators.
```
def regularCommutantAlgebra
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) (P : VonNeumannAlgebra H) :
    VonNeumannAlgebra (RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
def OAI.KadisonKastler.PublishedRegularCommutant line 51
Source documentation
The real-group specialization of the published commutant-generator theorem. Strong continuity refers to the ordinary topology on ℝ. No fixed-point equality or perturbation assertion is assumed.
```
def PublishedRegularCommutant : Prop :=
…
```
theorem OAI.KadisonKastler.generated_le_vonNeumann line 60
theorem OAI.KadisonKastler.regularCommutantAlgebra_le_fixed_commutant line 78
Source documentation
Each explicit commutant generator commutes with the fixed algebra; the same therefore holds for the generated von Neumann algebra.
```
theorem regularCommutantAlgebra_le_fixed_commutant
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) (P : VonNeumannAlgebra H) :
    regularCommutantAlgebra U P ≤
      (fixedPointAlgebra (regularCoreAction U) (regularTensorAlgebra P)).commutant := by
…
```
Mentions: OAI.KadisonKastler.regularCommutantAlgebra, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularTensorAlgebra

theorem OAI.KadisonKastler.regularCoreAlgebra_eq_fixed_of_published line 96

Source documentation

The reverse core inclusion follows by applying the published commutant formula and then taking one more commutant.

theorem regularCoreAlgebra_eq_fixed_of_published
    [TopologicalSpace.SeparableSpace H]
    (hComm : PublishedRegularCommutant.{u})
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ => (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (P : VonNeumannAlgebra H)
    (hP : ∀ s T, T ∈ P → unitaryConj (U s) T ∈ P) :
    regularCoreAlgebra U hU P =
      fixedPointAlgebra (regularCoreAction U) (regularTensorAlgebra P) := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularTensorAlgebra

theorem OAI.KadisonKastler.regularCore_characterFixed_coe_of_published line 120

Source documentation

Character fixed points of the actual generated core recover the original algebra's regular image.

theorem regularCore_characterFixed_coe_of_published
    [TopologicalSpace.SeparableSpace H]
    (hComm : PublishedRegularCommutant.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ => (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (P : VonNeumannAlgebra H)
    (hP : ∀ s T, T ∈ P → unitaryConj (U s) T ∈ P) :
    (fixedPointAlgebra (regularCharacterRepresentation (H := H))
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.regularCharacterRepresentation