BaseCommutatorCompression.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Compression of commutators with base-algebra elements needs no invariance hypothesis on the other operator. This also restores the original operator after the free-product symmetrization.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.left_injective line 22
Source documentation
Faithfulness of the tracial algebra vectors makes left multiplication faithful as an algebra representation.
```
theorem left_injective (hfaithful : Function.Injective G.vector) :
    Function.Injective G.left := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_left line 30
Source documentation
The faithful tracial representation preserves the C-star norm.
```
theorem norm_left (hfaithful : Function.Injective G.vector) (a : P) :
    ‖G.left a‖ = ‖a‖ :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseInclusion_adjoint_intertwines line 35

Source documentation

The adjoint base inclusion intertwines every base-algebra element.

theorem baseInclusion_adjoint_intertwines (a : A) :
    (G.baseInclusion A).toContinuousLinearMap.adjoint.comp (G.left (a : P)) =
      (G.baseRepresentation A a).comp (G.baseInclusion A).toContinuousLinearMap.adjoint := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator_commutator_subalgebra line 50
Source documentation
Compression commutes with the commutator against a base element.
```
theorem baseOperator_commutator_subalgebra (Y : H →L[ℂ] H) (a : A) :
    G.baseOperator A (commutator Y (G.left (a : P))) =
      commutator (G.baseOperator A Y) (G.baseRepresentation A a) := by
…
```
Mentions: OAI.KadisonSimilarity.commutator
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator_commutator_eq_of_compression_eq line 62
Source documentation
Equal base compressions preserve exactly the compressed commutator used by the free-product corner theorem, even before invariance is established.
```
theorem baseOperator_commutator_eq_of_compression_eq (Y Z : H →L[ℂ] H)
    (h : G.baseOperator A Y = G.baseOperator A Z) (a : A) :
    G.baseOperator A (commutator Y (G.left (a : P))) =
      G.baseOperator A (commutator Z (G.left (a : P))) := by
…
```
Mentions: OAI.KadisonSimilarity.commutator