RegularCoreAlgebra.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The concrete regular core and its first fixed-point inclusion

The tensor algebra is the commutant of the constant copy of P' on L²(ℝ,H). The regular core is the von Neumann algebra generated by the concrete regular embedding and translations. Its generators lie in the tensor algebra and are fixed by the common regular action. This proves the first fixed-point inclusion without a crossed-product assumption.

def OAI.KadisonKastler.regularTensorAlgebra line 26
Source documentation
The concrete tensor algebra, specified by its constant commutant.
```
def regularTensorAlgebra (P : VonNeumannAlgebra H) :
    VonNeumannAlgebra (RegularCoreHilbert H) where
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.mem_regularTensorAlgebra_iff line 37
theorem OAI.KadisonKastler.regularConstant_mem_tensorAlgebra line 55
theorem OAI.KadisonKastler.regularTranslation_mem_tensorAlgebra line 64
theorem OAI.KadisonKastler.regularCoreEmbedding_mem_tensorAlgebra line 76
Source documentation
The field formula for the regular embedding preserves the concrete tensor algebra whenever the original group normalizes P.
```
theorem regularCoreEmbedding_mem_tensorAlgebra (P : VonNeumannAlgebra H)
    (hP : ∀ s T, T ∈ P → unitaryConj (U s) T ∈ P)
    {T : H →L[ℂ] H} (hT : T ∈ P) :
    regularCoreEmbedding U hU T ∈ regularTensorAlgebra P := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularTensorAlgebra
theorem OAI.KadisonKastler.regularTranslation_fixed line 102
Source documentation
Translations are also fixed by the common action: both translation groups are abelian, and constant operators commute with translations.
```
theorem regularTranslation_fixed (s t : Multiplicative ℝ) :
    unitaryConj (regularCoreAction U s)
      (regularRightTranslation (H := H) t :
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularRightTranslation
def OAI.KadisonKastler.regularCoreGenerators line 124
Source documentation
The actual generating set of the regular core.
```
def regularCoreGenerators (P : VonNeumannAlgebra H) :
    Set (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
def OAI.KadisonKastler.regularCoreAlgebra line 131
Source documentation
The von Neumann algebra generated by the regular representation.
```
def regularCoreAlgebra (P : VonNeumannAlgebra H) :
    VonNeumannAlgebra (RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.generatedAlgebra_le_of_le line 135
theorem OAI.KadisonKastler.regularCoreEmbedding_mem_core line 146
theorem OAI.KadisonKastler.regularTranslation_mem_core line 152
theorem OAI.KadisonKastler.regularCoreAlgebra_le_fixed line 160
Source documentation
The generator calculation proves the first core fixed-point inclusion.
```
theorem regularCoreAlgebra_le_fixed (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.regularCoreAlgebra_le_tensor line 173