TracialFreeCornerModel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The remaining word and reflection data in the free-corner argument are constructed from the local published reduced-product model and ordinary generated-algebra density. In particular neither an invariant word decomposition nor freeness of the compressed factors is an input.

theorem OAI.KadisonSimilarity.symmetryHalfProjectionProof line 20

Source documentation

The canonical half projection of a selfadjoint involution.

theorem symmetryHalfProjectionProof {D : StarSubalgebra ℂ P} (d : D)
    (hdstar : star d = d) (hdsq : d * d = 1) :
    IsStarProjection (dihedralHalfProjection
      (symmetryUnit (d : P) (congrArg (fun x : D => (x : P)) hdsq))) := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.symmetryUnit

theorem OAI.KadisonSimilarity.symmetryHalfProjection_mem line 31

Source documentation

The half projection belongs to every star subalgebra containing its reflection.

theorem symmetryHalfProjection_mem (C : StarSubalgebra ℂ P)
    {D : StarSubalgebra ℂ P} (d : D) (hdsq : d * d = 1) (hdC : (d : P) ∈ C) :
    dihedralHalfProjection
      (symmetryUnit (d : P) (congrArg (fun x : D => (x : P)) hdsq)) ∈ C :=
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.symmetryUnit

theorem OAI.KadisonSimilarity.symmetryRotation_zpow_mem line 39

Source documentation

All integer rotations lie in a star subalgebra containing both involutions. The inverse is the product in reverse order.

theorem symmetryRotation_zpow_mem (C : StarSubalgebra ℂ P)
    {D A : StarSubalgebra ℂ P} (d : D) (s : A)
    (hdsq : d * d = 1) (hssq : s * s = 1)
    (hdC : (d : P) ∈ C) (hsC : (s : P) ∈ C) (j : ℤ) :
    (↑((symmetryUnit (d : P) (congrArg (fun x : D => (x : P)) hdsq) *
      symmetryUnit (s : P) (congrArg (fun x : A => (x : P)) hssq)) ^ j) : P) ∈ C := by
…

Mentions: OAI.KadisonSimilarity.symmetryUnit

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_corner_of_published_local_models line 101

Source documentation

The free-corner estimate from the local reduced-product model. Word coordinates, reduced density, the half projection, rotation membership and compressed freeness are all derived.

theorem free_corner_of_published_local_models
    (hdC : (d : P) ∈ C) (hsC : (s : P) ∈ C)
    (K : StarSubalgebra ℂ (CStarCorner p (symmetryHalfProjectionProof d hdstar hdsq)))
    [IsClosed (K : Set (CStarCorner p (symmetryHalfProjectionProof d hdstar hdsq)))]
    (hK : (factorAlgebra
      (CStarCorner.subalgebra p (symmetryHalfProjectionProof d hdstar hdsq) D
        (symmetryHalfProjection_mem D d hdsq d.property))
      (CStarCorner.subalgebra p (symmetryHalfProjectionProof d hdstar hdsq) C
        (symmetryHalfProjection_mem C d hdsq hdC))).topologicalClosure = K)
    (compression : RicardXuCompressionInput
      ((G.halfCornerGeometry dU (symmetryHalfProjectionProof d hdstar hdsq)
        (trace_dihedralHalfProjection G.trace hτ dU hd0)).baseGeometry K)
…

Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.symmetryHalfProjectionProof, OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra, OAI.KadisonSimilarity.CStarCorner.subalgebra, OAI.KadisonSimilarity.symmetryHalfProjection_mem, OAI.KadisonSimilarity.RicardXuCompressionInput, OAI.KadisonSimilarity.trace_dihedralHalfProjection, OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry