RegularCoreStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-corner argument for the actual regular cores

This specializes the proved injective-matrix argument and character descent to the concrete regular representation. The semifinite matrix subalgebra and its finite initial corner are explicit data. In particular, none of the action, fixed-point, or range-identification conclusions is assumed.

theorem OAI.KadisonKastler.regularCore_spatial_of_injective_matrix_subalgebra line 35

Source documentation

A tensor gap, an injective matrix subalgebra in the source regular core, and an II₁ initial corner give the original-space conjugacy.

theorem regularCore_spatial_of_injective_matrix_subalgebra
    (h : FiniteFactorPublishedInputs.{u})
    (hComm : PublishedRegularCommutant.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ =>
      (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (hM : ∀ s T, T ∈ M → unitaryConj (U s) T ∈ M)
…

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

theorem OAI.KadisonKastler.regularCore_spatial_of_matrix_corner line 80

Source documentation

The injective matrix subalgebra is constructed from the actual full matrix corner by increasing factorial-period stages. Thus the only semifinite data left here are the full corner and its II₁ initial corner.

theorem regularCore_spatial_of_matrix_corner
    (h : FiniteFactorPublishedInputs.{u})
    (hComm : PublishedRegularCommutant.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ =>
      (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (hM : ∀ s T, T ∈ M → unitaryConj (U s) T ∈ M)
…

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

theorem OAI.KadisonKastler.regularCore_spatial_of_finite_projection_matrix_corner line 118

Source documentation

A finite nonzero first projection in the diffuse source factor suffices: its actual II₁ corner is proved by compression, rather than assumed. The countable matrix units and finite projection remain explicit geometric data.

theorem regularCore_spatial_of_finite_projection_matrix_corner
    (h : FiniteFactorPublishedInputs.{u})
    (hComm : PublishedRegularCommutant.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ =>
      (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (hM : ∀ s T, T ∈ M → unitaryConj (U s) T ∈ M)
…

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