UnitizationFiberClosure.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Bicommutant closure on the old-unit fibers

Restriction to the range of the old unit sends the represented unitization bicommutant into the bicommutant of the genuine original-algebra representation. This uses commutants and actual compression, including when the range is the zero Hilbert space.

theorem OAI.KadisonSimilarity.projectionFiberRetraction_eq_adjoint line 21
Source documentation
Retraction onto the closed range of an orthogonal projection is the Hilbert adjoint of its inclusion.
```
theorem projectionFiberRetraction_eq_adjoint (p : K →L[ℂ] K) (hp : IsStarProjection p) :
    projectionFiberRetraction p hp =
      (projectionFiberInclusion p hp).toContinuousLinearMap.adjoint := by
…
```
Mentions: OAI.KadisonSimilarity.projectionFiberRetraction, OAI.KadisonSimilarity.projectionFiberInclusion
theorem OAI.KadisonSimilarity.isometricExtension_projectionFiberCompression line 32
Source documentation
A supported operator is the zero extension of its actual compression.
```
theorem isometricExtension_projectionFiberCompression
    (p : K →L[ℂ] K) (hp : IsStarProjection p) (T : K →L[ℂ] K)
    (hleft : p * T = T) (hright : T * p = T) :
    isometricExtension (projectionFiberInclusion p hp)
      (projectionFiberCompression p hp T) = T := by
…
```
Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.projectionFiberInclusion, OAI.KadisonSimilarity.projectionFiberCompression
theorem OAI.KadisonSimilarity.unitization_inr_left_support line 43
theorem OAI.KadisonSimilarity.unitization_inr_right_support line 49
theorem OAI.KadisonSimilarity.unitizationRangeRepresentation_eq_compression line 55
theorem OAI.KadisonSimilarity.isometricExtension_unitizationRangeRepresentation line 64
Source documentation
The zero extension of the original algebra's range representation is the given represented inr element, not a new abstract representation.
```
theorem isometricExtension_unitizationRangeRepresentation
    (ρ : Unitization ℂ B →⋆ₐ[ℂ] (K →L[ℂ] K)) (b : B) :
    isometricExtension (projectionFiberInclusion (unitizationProjection ρ)
      (unitizationProjection_isStarProjection ρ)) (unitizationRangeRepresentation ρ b) =
      ρ (Unitization.inr b) := by
…
```
Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.projectionFiberInclusion, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationProjection_isStarProjection, OAI.KadisonSimilarity.unitizationRangeRepresentation

theorem OAI.KadisonSimilarity.unitization_representation_decomposition line 74

Source documentation

Every unitization element is its scalar part plus its inr part.

theorem unitization_representation_decomposition
    (ρ : Unitization ℂ B →⋆ₐ[ℂ] (K →L[ℂ] K)) (a : Unitization ℂ B) :
    ρ a = a.fst • (1 : K →L[ℂ] K) + ρ (Unitization.inr a.snd) := by
…

theorem OAI.KadisonSimilarity.unitizationRange_commutant_extension_commutes line 87

Source documentation

Operators in the commutant of the genuine old-unit range representation extend to operators commuting with the full unitization.

theorem unitizationRange_commutant_extension_commutes
    (ρ : Unitization ℂ B →⋆ₐ[ℂ] (K →L[ℂ] K))
    (T : projectionFiber (unitizationProjection ρ) (unitizationProjection_isStarProjection ρ)
      →L[ℂ] projectionFiber (unitizationProjection ρ) (unitizationProjection_isStarProjection ρ))
    (hT : T ∈ (representationVonNeumannAlgebra (unitizationRangeRepresentation ρ)).commutant)
    (a : Unitization ℂ B) :
    isometricExtension (projectionFiberInclusion (unitizationProjection ρ)
      (unitizationProjection_isStarProjection ρ)) T * ρ a =
      ρ a * isometricExtension (projectionFiberInclusion (unitizationProjection ρ)
        (unitizationProjection_isStarProjection ρ)) T := by
…

Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationProjection_isStarProjection, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.unitizationRangeRepresentation, OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.projectionFiberInclusion

theorem OAI.KadisonSimilarity.unitizationFiberCompression_mem line 115
Source documentation
Compression to the old-unit fiber preserves represented bicommutant membership. No support condition on the original operator is required.
```
theorem unitizationFiberCompression_mem
    (ρ : Unitization ℂ B →⋆ₐ[ℂ] (K →L[ℂ] K))
    (Q : K →L[ℂ] K) (hQ : Q ∈ representationVonNeumannAlgebra ρ) :
    projectionFiberCompression (unitizationProjection ρ)
      (unitizationProjection_isStarProjection ρ) Q ∈
        representationVonNeumannAlgebra (unitizationRangeRepresentation ρ) := by
…
```
Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.projectionFiberCompression, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationProjection_isStarProjection, OAI.KadisonSimilarity.unitizationRangeRepresentation