FullColumnTheorem.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

The full-column implementation argument

The corner commutator is constructed here, corrected by the proved cyclic implementation theorem, and extended through finite matrix coordinates with exactly the same norm. Extension by zero and the tracial commutation theorem then identify the resulting intertwiner as a right multiplier.

The finite-factor realization of the corner and its matrix coordinates remains explicit geometric data; the full-column conclusion is not an input.

def OAI.KadisonSimilarity.cornerCommutator line 30

Source documentation

The actual rectangular commutator of a corner operator.

def cornerCommutator (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F))
    (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) (G : K →L[ℂ] F) : C →L[ℂ] (K →L[ℂ] F) where
…

theorem OAI.KadisonSimilarity.cornerCommutator_apply line 45

theorem OAI.KadisonSimilarity.cornerCommutator_leibniz line 51

Source documentation

The rectangular Leibniz rule follows from composition, with no derivation hypothesis on the corner operator.

theorem cornerCommutator_leibniz (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F))
    (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) (G : K →L[ℂ] F) (a b : C) :
    cornerCommutator ρ σ G (a * b) =
      (ρ a).comp (cornerCommutator ρ σ G b) +
        (cornerCommutator ρ σ G a).comp (σ b) := by
…

Mentions: OAI.KadisonSimilarity.cornerCommutator

theorem OAI.KadisonSimilarity.exists_corner_intertwiner_of_published_inputs line 62

Source documentation

Correct the corner operator to an exact module intertwiner.

theorem exists_corner_intertwiner_of_published_inputs
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K))
    (G : K →L[ℂ] F) {ε : ℝ} (hG : ‖cornerCommutator ρ σ G‖ ≤ ε)
    (dickson : DicksonTwoBound (A := C) (RectangularSum F K))
…

Mentions: OAI.KadisonSimilarity.cornerCommutator, OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum

def OAI.KadisonSimilarity.copyInsert line 98
Source documentation
Insertion into one coordinate of a finite Hilbert sum.
```
def copyInsert {n : ℕ} (i : Fin n) : K →L[ℂ] HilbertCopies K n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.copyInsert_apply line 102
def OAI.KadisonSimilarity.copyMatrixUnit line 106
Source documentation
The scalar matrix unit which sends coordinate j to coordinate i.
```
def copyMatrixUnit {n : ℕ} (i j : Fin n) :
    HilbertCopies K n →L[ℂ] HilbertCopies K n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.copyMatrixUnit_apply line 110
def OAI.KadisonSimilarity.copyCorner line 114
Source documentation
A diagonal corner of a bounded operator on two finite Hilbert sums.
```
def copyCorner {n : ℕ} (i : Fin n) (W : HilbertCopies K n →L[ℂ] HilbertCopies F n) :
    K →L[ℂ] F :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.copyCorner_apply line 118
theorem OAI.KadisonSimilarity.eq_mapCopies_of_matrixUnit_intertwining line 124
Source documentation
Commutation with the scalar matrix units forces one repeated diagonal corner. Only the row of matrix units with target coordinate i is needed.
```
theorem eq_mapCopies_of_matrixUnit_intertwining {n : ℕ} (i : Fin n)
    (W : HilbertCopies K n →L[ℂ] HilbertCopies F n)
    (hW : ∀ j : Fin n, W.comp (copyMatrixUnit i j) = (copyMatrixUnit i j).comp W) :
    W = mapCopies (copyCorner i W) n := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.copyMatrixUnit, OAI.KadisonSimilarity.mapCopies, OAI.KadisonSimilarity.copyCorner
structure OAI.KadisonSimilarity.FullColumnCoordinates line 146
Source documentation
The finite matrix-unit coordinates of a full column and its corner. The two action identities say that full left multiplication has the usual corner matrix entries. They assert no existence of an intertwiner.
```
structure FullColumnCoordinates
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) (n : ℕ) where
…
```
def OAI.KadisonSimilarity.FullColumnCoordinates.extend line 163
Source documentation
Diagonal extension of a corner operator through matrix-unit coordinates.
```
def extend (c : FullColumnCoordinates L Lr ρ σ n) (T : K →L[ℂ] F) : D →L[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates
theorem OAI.KadisonSimilarity.FullColumnCoordinates.extend_apply line 167
theorem OAI.KadisonSimilarity.FullColumnCoordinates.extend_sub line 172
theorem OAI.KadisonSimilarity.FullColumnCoordinates.norm_extend line 179
Source documentation
No factor depending on the number of matrix units enters the norm.
```
theorem norm_extend (c : FullColumnCoordinates L Lr ρ σ n) (hn : 0 < n)
    (T : K →L[ℂ] F) : ‖c.extend T‖ = ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates
theorem OAI.KadisonSimilarity.FullColumnCoordinates.norm_extend_sub line 184
theorem OAI.KadisonSimilarity.FullColumnCoordinates.extend_intertwines line 189
Source documentation
An intertwiner for the corner extends to one for the whole left action.
```
theorem extend_intertwines (c : FullColumnCoordinates L Lr ρ σ n)
    (T : K →L[ℂ] F) (hT : ∀ a, T.comp (σ a) = (ρ a).comp T) (a : P) :
    (c.extend T).comp (Lr a) = (L a).comp (c.extend T) := by
…
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates
def OAI.KadisonSimilarity.FullColumnCoordinates.inCoordinates line 200
Source documentation
Write a full-column operator in the finite matrix-unit coordinates.
```
def inCoordinates (c : FullColumnCoordinates L Lr ρ σ n) (G : D →L[ℂ] H) :
    HilbertCopies K n →L[ℂ] HilbertCopies F n :=
…
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates, OAI.KadisonSimilarity.HilbertCopies
def OAI.KadisonSimilarity.FullColumnCoordinates.corner line 206
Source documentation
The distinguished corner of a full-column operator.
```
def corner (c : FullColumnCoordinates L Lr ρ σ n) (i : Fin n) (G : D →L[ℂ] H) :
    K →L[ℂ] F := copyCorner i (c.inCoordinates G)
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates, OAI.KadisonSimilarity.copyCorner
theorem OAI.KadisonSimilarity.FullColumnCoordinates.eq_extend_of_matrixUnit_intertwining line 212
Source documentation
A full operator commuting with the represented scalar matrix units is exactly the extension of its corner, rather than merely close to a diagonal operator.
```
theorem eq_extend_of_matrixUnit_intertwining
    (c : FullColumnCoordinates L Lr ρ σ n) (i : Fin n) (G : D →L[ℂ] H)
    (hG : ∀ j : Fin n, (c.inCoordinates G).comp (copyMatrixUnit i j) =
      (copyMatrixUnit i j).comp (c.inCoordinates G)) :
    G = c.extend (c.corner i G) := by
…
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates, OAI.KadisonSimilarity.copyMatrixUnit
structure OAI.KadisonSimilarity.TracialRightAction line 237
Source documentation
The right multiplication convention, including faithfulness. Composition has the opposite order: R_b ∘ R_a = R_(a*b).
```
structure TracialRightAction where
…
```
def OAI.KadisonSimilarity.TracialCommutationInput line 246
Source documentation
The finite-trace specialization of the tracial commutation theorem: Hiai, Theorem 2.2 and Example 2.4 (JMJ = M′); equivalently every bounded left-module endomorphism of L²(P,τ) is right multiplication by an element of P. This remains an explicit published input.
```
def TracialCommutationInput (L : P →⋆ₐ[ℂ] (H →L[ℂ] H))
    (R : TracialRightAction (P := P) (H := H)) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.TracialRightAction
theorem OAI.KadisonSimilarity.exists_supported_right_multiplier line 253
Source documentation
A full-column intertwiner extends by zero to a left-module endomorphism; tracial commutation therefore makes it a right multiplier supported on r.
```
theorem exists_supported_right_multiplier
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (R : TracialRightAction (P := P) (H := H)) (r : P)
…
```
Mentions: OAI.KadisonSimilarity.TracialRightAction
def OAI.KadisonSimilarity.CyclicStarRepresentation line 288
Source documentation
A representation has a vector whose algebra orbit is dense. Because the representation is linear in the algebra variable, no additional span is needed.
```
def CyclicStarRepresentation (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```

theorem OAI.KadisonSimilarity.cyclicStarRepresentation_of_module_coordinates line 293

Source documentation

Cyclicity transfers through the unitary module coordinates furnished by right multiplication by a partial isometry in the tracial corner argument.

theorem cyclicStarRepresentation_of_module_coordinates
    (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) (σ' : C →⋆ₐ[ℂ] (Q →L[ℂ] Q))
    (U : K ≃ₗᵢ[ℂ] Q) (ζ : Q) (hζ : DenseRange (fun a : C => σ' a ζ))
    (hU : ∀ a x, U (σ a x) = σ' a (U x)) : CyclicStarRepresentation σ := by
…

Mentions: OAI.KadisonSimilarity.CyclicStarRepresentation

def OAI.KadisonSimilarity.FiniteFactorProjectionComparison line 308
Source documentation
The precise finite-factor comparison consequence needed for the chosen corner. This is the trace form of projection comparison: Blackadar, III.1.1.11, together with the faithful finite trace.
```
def FiniteFactorProjectionComparison (τ : P → ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.TracialCornerCyclicityInput line 317
Source documentation
The local tracial module realization needed after comparison: a partial isometry from r into e realizes the corner representation on eL²(P)r as a cyclic module. In a concrete tracial model this is proved using the unitary ξ ↦ ξ v*, the dense orbit of vv*, and the preceding transfer lemma. It is explicit geometric data, not an invariant or similarity claim.
```
def TracialCornerCyclicityInput (e r : P) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```
def OAI.KadisonSimilarity.HaagerupForCyclicInput line 323
Source documentation
The applicability of the published standard-form theorem to a cyclic representation (Haagerup 1975, Lemma 2.10(1)).
```
def HaagerupForCyclicInput (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```
theorem OAI.KadisonSimilarity.haagerup_of_projection_comparison line 328
Source documentation
Projection comparison and the explicit tracial cyclic realization provide the precise standard-form hypothesis consumed by the analytic argument.
```
theorem haagerup_of_projection_comparison
    (τ : P → ℝ) (comparison : FiniteFactorProjectionComparison τ)
    (e r : P) (he : IsStarProjection e) (hr : IsStarProjection r) (hτ : τ r ≤ τ e)
    (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) (cyclic : TracialCornerCyclicityInput e r σ)
    (haagerup : HaagerupForCyclicInput σ) : HaagerupCyclicVectorRealization σ := by
…
```
Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.TracialCornerCyclicityInput, OAI.KadisonSimilarity.HaagerupForCyclicInput, OAI.KadisonSimilarity.HaagerupCyclicVectorRealization
theorem OAI.KadisonSimilarity.full_column_of_published_inputs line 351
Source documentation
The full-column conclusion from the four specialized published cyclic inputs and tracial commutation. The remaining hypotheses describe the actual corner, its finite matrix coordinates, and its projection into the tracial Hilbert space. In particular, no right-multiplier approximation is assumed.
```
theorem full_column_of_published_inputs
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K))
    {n : ℕ} (hn : 0 < n) (c : FullColumnCoordinates L Lr ρ σ n)
    (R : TracialRightAction (P := P) (H := H)) (r : P)
…
```
Mentions: OAI.KadisonSimilarity.FullColumnCoordinates, OAI.KadisonSimilarity.TracialRightAction

theorem OAI.KadisonSimilarity.full_column_of_matrixUnit_commutation line 380

Source documentation

Version of the full-column theorem in which the actual matrix-unit commutation of the given operator supplies its diagonal form.

theorem full_column_of_matrixUnit_commutation
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K))
    {n : ℕ} (i : Fin n) (c : FullColumnCoordinates L Lr ρ σ n)
    (R : TracialRightAction (P := P) (H := H)) (r : P)
…

Mentions: OAI.KadisonSimilarity.FullColumnCoordinates, OAI.KadisonSimilarity.TracialRightAction