OAI/Analysis/KadisonKastler/MeasurableFiberRepresentations.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed-coordinate representations on measurable rank strata

  1. abbrev OAI.KadisonKastler.representationUnitProjection line 20
  2. theorem OAI.KadisonKastler.representationUnitProjection_idempotent line 22
  3. def OAI.KadisonKastler.fixedFiberRepresentation line 27

    Source documentation

    A nonunital ambient field acts unitally on each fixed-coordinate range.

    def fixedFiberRepresentation (n : ℕ)
    (x : projectionRankStratum (representationUnitProjection ρ) b n) :
    A →⋆ₐ[ℂ] (ℓ²(projectionDimensionIndex n, ℂ) →L[ℂ] ℓ²(projectionDimensionIndex n, ℂ)) := by
…

    Mentions: OAI.KadisonKastler.projectionRankStratum, OAI.KadisonKastler.representationUnitProjection, OAI.KadisonKastler.projectionDimensionIndex

  4. theorem OAI.KadisonKastler.representationUnitProjection_invariant line 37
  5. theorem OAI.KadisonKastler.fixedFiberRepresentation_eq line 43
  6. theorem OAI.KadisonKastler.fixedFiberRepresentation_measurable line 55