RegularCoreFiniteProjection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Regular-core stability from one finite full projection

The published countable-copy theorem supplies the matrix geometry. The represented corner's factor, finite and diffuse properties are proved by compression, and the periodic matrix stages supply the injective subalgebra. No corner type or stability conclusion is included in the projection input.

theorem OAI.KadisonKastler.regularCore_spatial_of_finite_full_projection line 33

Source documentation

Only one nonzero finite projection in the properly infinite source core is needed; the remaining matrix and II₁ corner data are constructed.

theorem regularCore_spatial_of_finite_full_projection
    (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