TraceTransport.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Literal weak-operator generation under a concrete star-algebra isomorphism. Continuity is explicitly for the restricted WOT, not the operator norm topology. This transport does not construct a trace representation of a finite factor.

abbrev OAI.Generator.WOTCarrier line 22
Source documentation
The carrier equipped with the subspace topology from ambient WOT.
```
abbrev WOTCarrier (S : StarSubalgebra ℂ (H →L[ℂ] H)) :=
…
```
def OAI.Generator.wotMap line 26
Source documentation
A homomorphism viewed on the WOT carrier, with ambient WOT codomain.
```
def wotMap (φ : S →⋆ₐ[ℂ] T) (a : WOTCarrier S) : K →WOT[ℂ] K :=
…
```
Mentions: OAI.Generator.WOTCarrier

def OAI.Generator.concretePreimage line 30

Source documentation

Ambient concrete inverse image, contained in S.

def concretePreimage (φ : S →⋆ₐ[ℂ] T)
    (Q : StarSubalgebra ℂ (K →L[ℂ] K)) : StarSubalgebra ℂ (H →L[ℂ] H) :=
…

theorem OAI.Generator.concretePreimage_le line 34
theorem OAI.Generator.mem_concretePreimage line 39
theorem OAI.Generator.concretePreimage_wotClosed line 50

theorem OAI.Generator.map_mem_wstar line 67

Source documentation

WOT continuity suffices for the forward inclusion on generated algebras.

theorem map_mem_wstar (φ : S →⋆ₐ[ℂ] T)
    (hS : WOTClosed S) (hφ : Continuous (wotMap φ))
    (s : Set S) (a : S) (ha : a.val ∈ wstar (Subtype.val '' s)) :
    (φ a).val ∈ wstar ((fun b : S => (φ b).val) '' s) := by
…

Mentions: OAI.Generator.WOTClosed, OAI.Generator.wotMap, OAI.Generator.wstar

structure OAI.Generator.WOTStarAlgEquiv line 77
Source documentation
An algebra isomorphism continuous in both directions for the concrete weak operator topologies.
```
structure WOTStarAlgEquiv (S : StarSubalgebra ℂ (H →L[ℂ] H))
    (T : StarSubalgebra ℂ (K →L[ℂ] K)) where
…
```
def OAI.Generator.WOTStarAlgEquiv.symm line 86
theorem OAI.Generator.WOTStarAlgEquiv.mem_wstar_iff line 91
theorem OAI.Generator.WOTStarAlgEquiv.wstar_image_eq line 115
theorem OAI.Generator.WOTStarAlgEquiv.wstar_singleton_eq line 130
theorem OAI.Generator.WOTStarAlgEquiv.singlyGenerated_iff line 142
theorem OAI.Generator.isII1Factor_of_starAlgEquiv line 158
theorem OAI.Generator.WOTStarAlgEquiv.isII1Factor_iff line 206
def OAI.Generator.Tracial.traceFreeHilbertVectorBall line 249
theorem OAI.Generator.Tracial.traceFreeHilbertVectorBall_isClosed line 252
theorem OAI.Generator.Tracial.traceFreeHilbertIntoClosure_symmetrize line 275
theorem OAI.Generator.Tracial.traceFreeHilbertIntoClosure_clip line 279
theorem OAI.Generator.Tracial.traceFreeHilbertClosure_selfAdjoint_approximation line 285
theorem OAI.Generator.Tracial.traceFreeHilbertClosure_selfAdjoint_preimage line 305
theorem OAI.Generator.Tracial.traceFreeHilbertIntoClosure_surjective line 322
theorem OAI.Generator.Tracial.traceFreeHilbertIntoClosure_injective line 330
def OAI.Generator.Tracial.traceFreeHilbertEquiv line 334
theorem OAI.Generator.Tracial.traceFreeHilbertAction_range_eq line 338
theorem OAI.Generator.Tracial.traceHilbertVonNeumann_wotClosed line 347
theorem OAI.Generator.Tracial.traceFreeHilbertAction_range_wotClosed line 367
theorem OAI.Generator.Tracial.traceFreeHilbertEquiv_norm line 405
def OAI.Generator.Tracial.traceFreeHilbertIsometry line 408
theorem OAI.Generator.Tracial.traceFreeHilbertClosure_isII1Factor line 412
theorem OAI.Generator.Tracial.traceFreeHilbertClosure_hasSeparablePredual line 424

theorem OAI.Generator.isII1Factor_cyclic_tracial_representation line 438

Source documentation

The original exact factor and predual predicates produce a concrete cyclic tracial representation and an isometric algebra isomorphism. No WOT continuity of the isomorphism on the whole carrier, or Hilbert separability, is asserted.

theorem isII1Factor_cyclic_tracial_representation
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S) (hsep : HasSeparablePredual S) :
    ∃ (K : Type u) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K) (_ : CompleteSpace K)
      (N : VonNeumannAlgebra K) (e : S ≃⋆ₐ[ℂ] N.toStarSubalgebra)
      (τ : UltrapowerBridge.TracialRepresentation N),
      IsII1Factor N.toStarSubalgebra ∧ HasSeparablePredual N.toStarSubalgebra ∧
      (∀ a, ‖e a‖ = ‖a‖) ∧ DenseRange (fun a : N.toStarSubalgebra => a.val τ.vector) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.Generator.HasSeparablePredual, OAI.UltrapowerBridge.TracialRepresentation

def OAI.Generator.Tracial.traceFreeSubalgebraWeakBall line 510
theorem OAI.Generator.Tracial.traceFreeSubalgebraWeakBall_isCompact line 514
def OAI.Generator.Tracial.traceFreeSubalgebraVectorBall line 532
theorem OAI.Generator.Tracial.traceFreeSubalgebraVectorBall_isClosed line 535
theorem OAI.Generator.Tracial.traceSymmetrize_mem_original line 558
theorem OAI.Generator.Tracial.traceClip_mem_original line 563
def OAI.Generator.Tracial.traceFreeSubalgebraClosure line 615
Source documentation
The double commutant of the represented intersection with Q.
```
def traceFreeSubalgebraClosure : VonNeumannAlgebra K where
…
```
theorem OAI.Generator.Tracial.traceFreeSubalgebraClosure_mem_iff line 629
theorem OAI.Generator.Tracial.traceFreeSubalgebraClosure_le line 636
def OAI.Generator.Tracial.traceFreeSubalgebraInclusion line 645
theorem OAI.Generator.Tracial.traceFreeSubalgebra_selfAdjoint_approximation line 650
theorem OAI.Generator.Tracial.traceFreeSubalgebra_selfAdjoint_preimage line 684
theorem OAI.Generator.Tracial.traceFreeSubalgebraClosure_preimage line 703
theorem OAI.Generator.Tracial.traceFreeSubalgebraImage_eq_closure line 714
theorem OAI.Generator.Tracial.traceFreeSubalgebraImage_wotClosed line 726
Source documentation
Every original WOT-closed subalgebra has WOT-closed represented intersection. No cyclicity of its orbit, factor hypothesis on Q, or full WOT continuity is used.
```
theorem traceFreeSubalgebraImage_wotClosed (hQ : WOTClosed Q) :
    WOTClosed ((Q.comap M.toStarSubalgebra.subtype).map π) := by
…
```
Mentions: OAI.Generator.WOTClosed, OAI.Generator.Tracial.Q
theorem OAI.Generator.Tracial.traceFreeHilbert_singlyGenerated_pullback line 768
Source documentation
Pull a literal W*-generator back through the constructed representation. Closed images of the original generated subalgebra replace any unproved whole-carrier weak-operator continuity assertion.
```
theorem traceFreeHilbert_singlyGenerated_pullback
    (hgen : SinglyGenerated (N).toStarSubalgebra) : SinglyGenerated M.toStarSubalgebra := by
…
```