FactorAnticommuting.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Anticommuting unitaries in finite factors

The two Pauli matrices in a unital system of two-by-two matrix units give selfadjoint anticommuting unitaries. Every II₁ factor contains such a system, so the quantitative Jordan orientation test applies without an additional assumption on the source factor.

def OAI.KadisonKastler.matrixUnitsPauliZ line 24
Source documentation
The diagonal Pauli matrix in the given matrix units.
```
def matrixUnitsPauliZ : A := E.entry 0 0 - E.entry 1 1
```
def OAI.KadisonKastler.matrixUnitsPauliX line 27
Source documentation
The off-diagonal Pauli matrix in the given matrix units.
```
def matrixUnitsPauliX : A := E.entry 0 1 + E.entry 1 0
```
theorem OAI.KadisonKastler.matrixUnitsPauliZ_star line 29
theorem OAI.KadisonKastler.matrixUnitsPauliX_star line 32
theorem OAI.KadisonKastler.matrixUnitsPauliZ_sq line 35
theorem OAI.KadisonKastler.matrixUnitsPauliX_sq line 40
def OAI.KadisonKastler.matrixUnitsPauliZUnitary line 46
Source documentation
The diagonal Pauli unitary.
```
def matrixUnitsPauliZUnitary : unitary A :=
…
```
def OAI.KadisonKastler.matrixUnitsPauliXUnitary line 51
Source documentation
The off-diagonal Pauli unitary.
```
def matrixUnitsPauliXUnitary : unitary A :=
…
```
theorem OAI.KadisonKastler.matrixUnitsPauli_anticommute line 55
theorem OAI.KadisonKastler.exists_anticommuting_unitaries_of_matrixUnits line 65
Source documentation
A unital two-by-two matrix algebra supplies the exact pair used in the Jordan orientation argument.
```
theorem exists_anticommuting_unitaries_of_matrixUnits
    (E : Generator.MatrixUnitSystem (Fin 2) A) :
    ∃ a b : unitary A, star (a : A) = (a : A) ∧ star (b : A) = (b : A) ∧
      (a : A) * (b : A) = -((b : A) * (a : A)) :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem

theorem OAI.KadisonKastler.exists_anticommuting_unitaries_of_II1 line 80

Source documentation

Every concrete II₁ factor contains selfadjoint anticommuting unitaries.

theorem exists_anticommuting_unitaries_of_II1
    (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    ∃ a b : unitary (Algebra M),
      star (a : Algebra M) = (a : Algebra M) ∧
      star (b : Algebra M) = (b : Algebra M) ∧
      (a : Algebra M) * (b : Algebra M) = -((b : Algebra M) * (a : Algebra M)) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.PreservesJordan.multiplicative_of_close_of_II1 line 91

Source documentation

A sufficiently close surjective Jordan map out of a II₁ factor has the multiplicative orientation; no contractivity hypothesis is needed.

theorem PreservesJordan.multiplicative_of_close_of_II1
    {B D : Type*} [NormedRing B] [NormedAlgebra ℂ B]
    [NormedRing D] [NormedAlgebra ℂ D]
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (θ : Algebra M →ₗ[ℂ] B) (ι : Algebra M →ₐ[ℂ] D) (κ : B →ₐ[ℂ] D) {e : ℝ}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖)
    (hclose : ∀ x, ‖κ (θ x) - ι x‖ ≤ e * ‖x‖)
    (hsmall : 3 * e + e ^ 2 < 2) :
    ∀ x y, θ (x * y) = θ x * θ y := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra