OAI/Analysis/Nuclearity/FactorTensorExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The faithful-completion step of Tomiyama's factor-representation argument. Only the represented left algebra is required to be nuclear. In the ideal application it is a quotient image, whose nuclearity still requires proof.

  1. theorem OAI.WeakPureInfiniteness.factor_starTensor_injective line 22
  2. theorem OAI.WeakPureInfiniteness.factor_tensor_norm_eq line 31
  3. theorem OAI.WeakPureInfiniteness.exists_factor_tensor_extension line 44

    Source documentation

    A faithful factor product extends to the given tensor completion. This uses nuclearity of the actual represented algebra, not simplicity.

    theorem exists_factor_tensor_extension (hA : Pureness.IsNuclear.{u,v} A)
    (f : A ⊗[ℂ] B →⋆ₐ[ℂ] E) (hf : Function.Injective f) (hd : DenseRange f)
    (M : VonNeumannAlgebra H) (hM : FactorIndependence.IsFactor M)
    (φ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ψ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hφ : Function.Injective φ) (hψ : Function.Injective ψ)
    (hφM : ∀ a, φ a ∈ M) (hψM : ∀ b, ψ b ∈ M.commutant)
    (hc : ∀ a b, Commute (φ a) (ψ b)) :
    ∃ θ : E →⋆ₐ[ℂ] (H →L[ℂ] H), Isometry θ ∧
      ∀ z, θ (f z) = Pureness.commutingStarTensorHom φ ψ hc z := by
…

    Mentions: OAI.Pureness.commutingStarTensorHom