AbelianActionStability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Abelian action correction and descent

Finite-Cesaro means give the scalar averaging used in the action and fixed-point arguments. These results apply to the additive real modular group and its character group, viewed as discrete abelian groups.

theorem OAI.KadisonKastler.exists_common_abelian_action_of_near_normalizers line 27
Source documentation
Correct nearby normalizers for an abelian action using an invariant scalar mean and a normalizer factorization.
```
theorem exists_common_abelian_action_of_near_normalizers
    (hpub : PublishedNormalizerFactorization (H := H)) (P : VonNeumannAlgebra H)
…
```
Mentions: OAI.KadisonKastler.PublishedNormalizerFactorization

theorem OAI.KadisonKastler.kkDistance_abelian_fixedPointAlgebra_le line 40

Source documentation

Passage to fixed points of an abelian action decreases the gap.

theorem kkDistance_abelian_fixedPointAlgebra_le
    (U : G →* unitary (H →L[ℂ] H)) (M N : VonNeumannAlgebra H)
    (hM : ∀ g T, T ∈ M → unitaryConj (U g) T ∈ M)
    (hN : ∀ g T, T ∈ N → unitaryConj (U g) T ∈ N) :
    kkDistance (fixedPointAlgebra U M) (fixedPointAlgebra U N) ≤ kkDistance M N :=
…

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

theorem OAI.KadisonKastler.concrete_unitary_of_abelian_character_average line 63

Source documentation

An abelian character action supplies its own averaging map in descent.

theorem concrete_unitary_of_abelian_character_average
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (A B : VonNeumannAlgebra K)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K)) (hj : Function.Injective j)
    (hV : ∀ l T, T ∈ fixedPointAlgebra U B →
      unitaryConj (V l) T ∈ fixedPointAlgebra U B)
    (hjoint : (fixedPointAlgebra V (fixedPointAlgebra U B) : Set (K →L[ℂ] K)) =
      j '' (N : Set (H →L[ℂ] H)))
    (hjM : ∀ x : Algebra M, j x ∈ fixedPointAlgebra U A)
    (hjfix : ∀ l x, unitaryConj (V l) (j x) = j x)
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.spatial_of_abelian_core_matrix_data line 102

Source documentation

The complete finite-corner/character descent for abelian actions, with both averaging means constructed and all core representation data explicit.

theorem spatial_of_abelian_core_matrix_data
    (h : FiniteFactorPublishedInputs.{v}) (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (A B : VonNeumannAlgebra K)
    (hA : ∀ g T, T ∈ A → unitaryConj (U g) T ∈ A)
    (hB : ∀ g T, T ∈ B → unitaryConj (U g) T ∈ B)
    (hV : ∀ l T, T ∈ fixedPointAlgebra U B →
      unitaryConj (V l) T ∈ fixedPointAlgebra U B)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K)) (hj : Function.Injective j)
    (hjoint : (fixedPointAlgebra V (fixedPointAlgebra U B) : Set (K →L[ℂ] K)) =
…