GlobalFiberRestriction.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Restriction and zero extension of range representations

The old-unit projection is unchanged by restriction along a unital map, even when the represented map is nonunital. Restriction commutes with zero extension from a conull base, so the canonical range identifications are available at every base point, including the zero fibers.

theorem OAI.KadisonSimilarity.nonunitalRestrict_projection line 20
def OAI.KadisonSimilarity.nonunitalRestrictionFiberEquiv line 26
theorem OAI.KadisonSimilarity.nonunitalRestrictionFiberEquiv_coe line 33
theorem OAI.KadisonSimilarity.nonunitalRestrictionFiberEquiv_symm_coe line 39
theorem OAI.KadisonSimilarity.nonunitalRestrictionFiberEquiv_intertwines line 44
theorem OAI.KadisonSimilarity.nonunitalRestriction_range_conjugacy line 55
theorem OAI.KadisonSimilarity.zeroExtend_unitizationRestrict line 74
Source documentation
Zero extension is functorial for restriction of the original algebra.
```
theorem zeroExtend_unitizationRestrict (x : Ω) :
    zeroExtendNonunitalRepresentation s (fun y => unitizationRestrict φ (ρ y)) x =
      (zeroExtendNonunitalRepresentation s ρ x).comp φ.toNonUnitalStarAlgHom := by
…
```
Mentions: OAI.KadisonSimilarity.zeroExtendNonunitalRepresentation, OAI.KadisonSimilarity.unitizationRestrict
theorem OAI.KadisonSimilarity.globalRestriction_projection line 85

def OAI.KadisonSimilarity.globalRestrictionFiberEquiv line 93

Source documentation

The actual zero-extended fibers of the restricted and joint representations are identified by the identity on ambient vectors.

def globalRestrictionFiberEquiv (x : Ω) :
    projectionFiber
        (nonunitalUnitProjection
          (zeroExtendNonunitalRepresentation s (fun y => unitizationRestrict φ (ρ y)) x))
        (nonunitalUnitProjection_isStarProjection
          (zeroExtendNonunitalRepresentation s (fun y => unitizationRestrict φ (ρ y)) x)) ≃ₗᵢ[ℂ]
      projectionFiber (nonunitalUnitProjection (zeroExtendNonunitalRepresentation s ρ x))
        (nonunitalUnitProjection_isStarProjection (zeroExtendNonunitalRepresentation s ρ x)) :=
…

Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.nonunitalUnitProjection, OAI.KadisonSimilarity.zeroExtendNonunitalRepresentation, OAI.KadisonSimilarity.unitizationRestrict, OAI.KadisonSimilarity.nonunitalUnitProjection_isStarProjection

theorem OAI.KadisonSimilarity.globalRestrictionFiberEquiv_coe line 103
theorem OAI.KadisonSimilarity.globalRestrictionFiberEquiv_symm_coe line 111
theorem OAI.KadisonSimilarity.globalRestrictionFiberEquiv_intertwines line 116
theorem OAI.KadisonSimilarity.globalRestriction_range_conjugacy line 133
Source documentation
Exact equality of the global zero-extended range representations.
```
theorem globalRestriction_range_conjugacy (x : Ω) :
    (globalRestrictionFiberEquiv s φ ρ x).conjStarAlgEquiv.toStarAlgHom.comp
        (nonunitalRangeRepresentation
          (zeroExtendNonunitalRepresentation s (fun y => unitizationRestrict φ (ρ y)) x)) =
      (nonunitalRangeRepresentation (zeroExtendNonunitalRepresentation s ρ x)).comp φ := by
…
```
Mentions: OAI.KadisonSimilarity.globalRestrictionFiberEquiv, OAI.KadisonSimilarity.nonunitalRangeRepresentation, OAI.KadisonSimilarity.zeroExtendNonunitalRepresentation, OAI.KadisonSimilarity.unitizationRestrict
theorem OAI.KadisonSimilarity.globalRestriction_compression_conjugacy line 149