TracialBaseGeometry.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The closed base algebra has its actual tracial Hilbert representation inside the ambient one. Its left, right, and conjugation actions are compatible with the canonical base inclusion.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseAlgebra_isClosed_of_complete line 21
Source documentation
Completeness in the inherited subtype norm supplies the closedness needed for Mathlib's subtype C-star algebra instance.
```
theorem baseAlgebra_isClosed_of_complete [CompleteSpace A] : IsClosed (A : Set P) :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry line 28
Source documentation
Restrict the trace and left action to the closed base algebra; the Hilbert space is the closure of its actual ambient algebra vectors.
```
def baseGeometry : TracialCornerGeometry A (G.baseSpace A) where
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_trace line 40
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_vector_coe line 43
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_left_coe line 46
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_trace_one line 50
Source documentation
The actual base trace is normalized whenever the ambient trace is.
```
theorem baseGeometry_trace_one (htrace : G.trace 1 = 1) :
    (G.baseGeometry A).trace 1 = 1 := htrace
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_vector_injective line 54
Source documentation
Faithfulness of the represented algebra vectors passes to the base.
```
theorem baseGeometry_vector_injective (hfaithful : Function.Injective G.vector) :
    Function.Injective (G.baseGeometry A).vector := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_conjugation_coe line 63
Source documentation
The tracial conjugation of the base is exactly the restriction of ambient tracial conjugation, proved on the dense algebra vectors.
```
theorem baseGeometry_conjugation_coe (x : G.baseSpace A) :
    ((G.baseGeometry A).conjugation x : H) = G.conjugation (x : H) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.conjugation
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_right_coe line 75
Source documentation
Base right multiplication is the restriction of actual ambient right multiplication. No independent commutation representation is assumed.
```
theorem baseGeometry_right_coe (a : A) (x : G.baseSpace A) :
    ((G.baseGeometry A).right a x : H) = G.right (a : P) (x : H) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.right
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_right_invariant line 87
Source documentation
The completed base subspace is invariant under right multiplication by its algebra, with membership derived from the constructed base geometry.
```
theorem baseSpace_right_invariant (a : A) (x : H) (hx : x ∈ G.baseSpace A) :
    G.right (a : P) x ∈ G.baseSpace A := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_right_intertwines line 93
Source documentation
Operator form of the exact right-action inclusion.
```
theorem baseGeometry_right_intertwines (a : A) :
    (G.baseInclusion A).toContinuousLinearMap.comp ((G.baseGeometry A).right a) =
      (G.right (a : P)).comp (G.baseInclusion A).toContinuousLinearMap := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.right
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_right_compression line 101
Source documentation
Compression of an ambient base-algebra right multiplier is its actual right action in the completed base representation.
```
theorem baseGeometry_right_compression (a : A) :
    G.baseOperator A (G.right (a : P)) = (G.baseGeometry A).right a := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.right