StarEquivTraceTransport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Tracial and bounded strong transport by a factor isomorphism

Uniqueness of the normalized finite-factor trace makes an algebraic star-isomorphism preserve the tracial two-norm. The concrete finite-vector trace formulas then give strong-operator continuity on every bounded ball, in both directions. No continuity of the isomorphism is assumed.

theorem OAI.KadisonKastler.trace_starAlgEquiv line 30

Source documentation

An algebraic star-isomorphism out of a II₁ factor preserves normalized faithful tracial states.

theorem trace_starAlgEquiv
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (e : Algebra M ≃⋆ₐ[ℂ] Algebra N) (x : Algebra M) :
    τN.toLinearMap (e x) = τM.toLinearMap x := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.traceTwoNorm_starAlgEquiv line 38

Source documentation

Consequently the same isomorphism is an isometry for the two-norm.

theorem traceTwoNorm_starAlgEquiv
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (e : Algebra M ≃⋆ₐ[ℂ] Algebra N) (x : Algebra M) :
    traceTwoNorm τN (e x) = traceTwoNorm τM x := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.starAlgEquiv_tendsto_strong_of_bounded line 49

Source documentation

Strong convergence of any norm-bounded net is preserved.

theorem starAlgEquiv_tendsto_strong_of_bounded
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (hτM : FiniteVectorTrace τM) (hτN : FiniteVectorTrace τN)
    (e : Algebra M ≃⋆ₐ[ℂ] Algebra N)
    {I : Type*} {l : Filter I} (x : I → Algebra M) (a : Algebra M)
    {C : ℝ} (hC : 0 ≤ C) (hx : ∀ i, ‖x i‖ ≤ C)
    (hs : ∀ ξ, Tendsto (fun i => (x i : H →L[ℂ] H) ξ) l
      (𝓝 ((a : H →L[ℂ] H) ξ))) :
    ∀ η, Tendsto (fun i => (e (x i) : K →L[ℂ] K) η) l
      (𝓝 ((e a : K →L[ℂ] K) η)) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.starAlgEquiv_tendsto_strong_iff_of_bounded line 81

Source documentation

The bounded strong-operator topologies agree under a star-isomorphism between two concrete II₁ factors.

theorem starAlgEquiv_tendsto_strong_iff_of_bounded
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (hτM : FiniteVectorTrace τM) (hτN : FiniteVectorTrace τN)
    (e : Algebra M ≃⋆ₐ[ℂ] Algebra N)
    {I : Type*} {l : Filter I} (x : I → Algebra M) (a : Algebra M)
    {C : ℝ} (hC : 0 ≤ C) (hx : ∀ i, ‖x i‖ ≤ C) :
    (∀ ξ, Tendsto (fun i => (x i : H →L[ℂ] H) ξ) l
      (𝓝 ((a : H →L[ℂ] H) ξ))) ↔
    (∀ η, Tendsto (fun i => (e (x i) : K →L[ℂ] K) η) l
      (𝓝 ((e a : K →L[ℂ] K) η))) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace

def OAI.KadisonKastler.starAlgEquivOrderIso line 111
Source documentation
The order isomorphism underlying an algebraic star-isomorphism.
```
def starAlgEquivOrderIso (e : A ≃⋆ₐ[ℂ] B) : A ≃o B where
…
```
theorem OAI.KadisonKastler.starAlgEquiv_isLUB_image line 117
Source documentation
Every existing supremum is preserved. In particular this is the order formulation of normality for bounded increasing operator nets.
```
theorem starAlgEquiv_isLUB_image (e : A ≃⋆ₐ[ℂ] B) {s : Set A} {a : A}
    (ha : IsLUB s a) : IsLUB (e '' s) (e a) :=
…
```

theorem OAI.KadisonKastler.starAlgEquiv_isLUB_range line 122

Source documentation

A convenient net-indexed version of supremum preservation.

theorem starAlgEquiv_isLUB_range (e : A ≃⋆ₐ[ℂ] B) {I : Type*}
    (x : I → A) {a : A} (ha : IsLUB (Set.range x) a) :
    IsLUB (Set.range (fun i => e (x i))) (e a) := by
…