JointFiberRestriction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Restricting a joint unitized representation

A unital inclusion preserves the old-unit projection. Thus restricting a joint unitized representation to one source preserves its actual Hilbert range, and the range representations agree after the canonical identity isometry between the two equal projection ranges.

def OAI.KadisonSimilarity.unitizationRestrict line 21

Source documentation

Restrict through the functorial map between the two unitizations.

def unitizationRestrict (φ : B →⋆ₐ[ℂ] S)
    (ρ : Unitization ℂ S →⋆ₐ[ℂ] (F →L[ℂ] F)) :
    Unitization ℂ B →⋆ₐ[ℂ] (F →L[ℂ] F) :=
…

theorem OAI.KadisonSimilarity.unitizationRestrict_inr line 26
theorem OAI.KadisonSimilarity.unitizationRestrict_projection line 34
Source documentation
Both old units act by exactly the same ambient projection.
```
theorem unitizationRestrict_projection (φ : B →⋆ₐ[ℂ] S)
    (ρ : Unitization ℂ S →⋆ₐ[ℂ] (F →L[ℂ] F)) :
    unitizationProjection (unitizationRestrict φ ρ) = unitizationProjection ρ := by
…
```
Mentions: OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationRestrict

def OAI.KadisonSimilarity.projectionFiberEquivOfEq line 41

Source documentation

Equal projections have the identity isometry between their ranges.

def projectionFiberEquivOfEq (p q : F →L[ℂ] F)
    (hp : IsStarProjection p) (hq : IsStarProjection q) (h : p = q) :
    projectionFiber p hp ≃ₗᵢ[ℂ] projectionFiber q hq :=
…

Mentions: OAI.KadisonSimilarity.projectionFiber

theorem OAI.KadisonSimilarity.projectionFiberEquivOfEq_coe line 47

def OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv line 54

Source documentation

Restriction preserves the range Hilbert space up to its canonical identity-on-vectors isometry.

def unitizationRestrictionFiberEquiv (φ : B →⋆ₐ[ℂ] S)
    (ρ : Unitization ℂ S →⋆ₐ[ℂ] (F →L[ℂ] F)) :
    projectionFiber (unitizationProjection (unitizationRestrict φ ρ))
        (unitizationProjection_isStarProjection (unitizationRestrict φ ρ)) ≃ₗᵢ[ℂ]
      projectionFiber (unitizationProjection ρ) (unitizationProjection_isStarProjection ρ) :=
…

Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationRestrict, OAI.KadisonSimilarity.unitizationProjection_isStarProjection

theorem OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv_coe line 61
theorem OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv_symm_coe line 67

theorem OAI.KadisonSimilarity.unitizationRestriction_compression_conjugacy line 74

Source documentation

Compression of every ambient operator respects this identification, not only operators from the represented source.

theorem unitizationRestriction_compression_conjugacy (φ : B →⋆ₐ[ℂ] S)
    (ρ : Unitization ℂ S →⋆ₐ[ℂ] (F →L[ℂ] F)) (T : F →L[ℂ] F) :
    (unitizationRestrictionFiberEquiv φ ρ).conjStarAlgEquiv
        (projectionFiberCompression (unitizationProjection (unitizationRestrict φ ρ))
          (unitizationProjection_isStarProjection (unitizationRestrict φ ρ)) T) =
      projectionFiberCompression (unitizationProjection ρ)
        (unitizationProjection_isStarProjection ρ) T := by
…

Mentions: OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv, OAI.KadisonSimilarity.projectionFiberCompression, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationRestrict, OAI.KadisonSimilarity.unitizationProjection_isStarProjection

theorem OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv_intertwines line 93

Source documentation

The restricted range action is the joint action of the included source element on the very same ambient vector.

theorem unitizationRestrictionFiberEquiv_intertwines (φ : B →⋆ₐ[ℂ] S)
    (ρ : Unitization ℂ S →⋆ₐ[ℂ] (F →L[ℂ] F)) (b : B)
    (v : projectionFiber (unitizationProjection (unitizationRestrict φ ρ))
      (unitizationProjection_isStarProjection (unitizationRestrict φ ρ))) :
    unitizationRestrictionFiberEquiv φ ρ
        (unitizationRangeRepresentation (unitizationRestrict φ ρ) b v) =
      unitizationRangeRepresentation ρ (φ b) (unitizationRestrictionFiberEquiv φ ρ v) := by
…

Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationRestrict, OAI.KadisonSimilarity.unitizationProjection_isStarProjection, OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv, OAI.KadisonSimilarity.unitizationRangeRepresentation

theorem OAI.KadisonSimilarity.unitizationRestriction_range_conjugacy line 106
Source documentation
Exact equality of the genuine representations after identifying the two equal projection ranges.
```
theorem unitizationRestriction_range_conjugacy (φ : B →⋆ₐ[ℂ] S)
    (ρ : Unitization ℂ S →⋆ₐ[ℂ] (F →L[ℂ] F)) :
    (unitizationRestrictionFiberEquiv φ ρ).conjStarAlgEquiv.toStarAlgHom.comp
        (unitizationRangeRepresentation (unitizationRestrict φ ρ)) =
      (unitizationRangeRepresentation ρ).comp φ := by
…
```
Mentions: OAI.KadisonSimilarity.unitizationRestrictionFiberEquiv, OAI.KadisonSimilarity.unitizationRangeRepresentation, OAI.KadisonSimilarity.unitizationRestrict