OAI/Analysis/RelativeGeneration/InclusionTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Generator.Tracial.traceFreeRelativeImage line 25

    Source documentation

    The actual WOT-closed image of the original given subalgebra.

    def traceFreeRelativeImage (P : StarSubalgebra ℂ (H →L[ℂ] H)) (hP : WOTClosed P) :
    VonNeumannAlgebra K :=
…

    Mentions: OAI.Generator.WOTClosed

  2. theorem OAI.Generator.Tracial.traceFreeRelativeImage_le line 33
  3. def OAI.Generator.Tracial.traceFreeRelativeImageHom line 39
  4. theorem OAI.Generator.Tracial.traceFreeRelativeImageHom_bijective line 43
  5. def OAI.Generator.Tracial.traceFreeRelativeImageEquiv line 54
  6. theorem OAI.Generator.Tracial.traceFreeRelativeImage_isII1Factor line 59
  7. theorem OAI.Generator.Tracial.traceFreeRelativeImage_irreducible line 65
  8. theorem OAI.Generator.Tracial.traceFreeRelativeGeneration_iff line 88

    Source documentation

    Generation is transported both ways, using closed preimages and closed images.

    theorem traceFreeRelativeGeneration_iff (u : M.toStarSubalgebra) :
    wstar ((P : Set (H →L[ℂ] H)) ∪ {u.val}) = M.toStarSubalgebra ↔
      wstar ((N : Set (K →L[ℂ] K)) ∪ {π u}) = (R).toStarSubalgebra := by
…

    Mentions: OAI.Generator.wstar