CommonRightAction.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Common right actions in a cyclic representation

Two operators in the same commutant are equal if they agree on the cyclic vector. Equality of the right actions obtained this way makes the product of the two tracial conjugations commute with both module actions.

def OAI.KadisonKastler.conjugationOperator line 20
Source documentation
Conjugating a linear operator by a conjugate-linear isometry gives a complex-linear operator.
```
def conjugationOperator (J : H ≃ₗᵢ⋆[ℂ] H) (a : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.conjugationOperator_apply line 24
theorem OAI.KadisonKastler.conjugationOperator_twice line 27

theorem OAI.KadisonKastler.conjugations_comp_apply_commute line 36

Source documentation

Equality of the right conjugates intertwines the product of the two conjugations with the original operator.

theorem conjugations_comp_apply_commute
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (hJ₁ : Function.Involutive J₁) (hJ₂ : Function.Involutive J₂)
    (a : H →L[ℂ] H)
    (ha : conjugationOperator J₁ a = conjugationOperator J₂ a) (ξ : H) :
    J₂ (J₁ (a ξ)) = a (J₂ (J₁ ξ)) := by
…

Mentions: OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.tracialConjugationDefect_commute_of_common_right line 48

Source documentation

Subtracting the identity retains this commutation relation.

theorem tracialConjugationDefect_commute_of_common_right
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (hJ₁ : Function.Involutive J₁) (hJ₂ : Function.Involutive J₂)
    (a : H →L[ℂ] H)
    (ha : conjugationOperator J₁ a = conjugationOperator J₂ a) :
    Commute (tracialConjugationDefect J₁ J₂) a := by
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.tracialConjugationDefect

theorem OAI.KadisonKastler.tracialConjugationDefect_commute_both line 60

Source documentation

The same comparison commutes with the common right operator too.

theorem tracialConjugationDefect_commute_both
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (hJ₁ : Function.Involutive J₁) (hJ₂ : Function.Involutive J₂)
    (a : H →L[ℂ] H)
    (ha : conjugationOperator J₁ a = conjugationOperator J₂ a) :
    Commute (tracialConjugationDefect J₁ J₂) a ∧
      Commute (tracialConjugationDefect J₁ J₂) (conjugationOperator J₁ a) := by
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.tracialConjugationDefect

theorem OAI.KadisonKastler.operator_eq_of_commute_of_eq_on_cyclicVector line 77

Source documentation

A cyclic vector separates the commutant, expressed without introducing any representation or standard-form hypothesis.

theorem operator_eq_of_commute_of_eq_on_cyclicVector
    {I : Type*} (A : I → H →L[ℂ] H) (Ω : H)
    (hcyclic : DenseRange (fun i => A i Ω)) (q r : H →L[ℂ] H)
    (hq : ∀ i, Commute q (A i)) (hr : ∀ i, Commute r (A i))
    (hΩ : q Ω = r Ω) : q = r := by
…

theorem OAI.KadisonKastler.conjugationOperator_algebraVector line 97
Source documentation
The standard tracial conjugation turns a left multiplier into the right multiplier by its adjoint, first on the dense algebra vectors.
```
theorem conjugationOperator_algebraVector
    (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (hJ : ∀ x : Algebra M, J (x.val Ω) = (star x).val Ω)
    (a x : Algebra M) :
    conjugationOperator J a.val (x.val Ω) = (x * star a).val Ω := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.conjugationOperator_mem_commutant line 108

Source documentation

In a cyclic standard tracial representation the conjugated left multiplier lies in the commutant of the whole algebra.

theorem conjugationOperator_mem_commutant
    (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (hJ : ∀ x : Algebra M, J (x.val Ω) = (star x).val Ω)
    (hcyclic : DenseRange (fun x : Algebra M => x.val Ω)) (a : Algebra M) :
    conjugationOperator J a.val ∈ M.commutant := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.conjugationOperator_common_vector line 132

Source documentation

A common left multiplier has the same right-action value on the common standard vector, before equality of the right operators is known.

theorem conjugationOperator_common_vector
    (M N : VonNeumannAlgebra H) (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (hM : ∀ x : Algebra M, J₁ (x.val Ω) = (star x).val Ω)
    (hN : ∀ x : Algebra N, J₂ (x.val Ω) = (star x).val Ω)
    (a : H →L[ℂ] H) (haM : a ∈ M) (haN : a ∈ N) :
    conjugationOperator J₁ a Ω = conjugationOperator J₂ a Ω := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.operator_eq_of_mem_commutant_of_eq_on_cyclicVector line 147

Source documentation

Concrete commutant members agreeing on a cyclic vector are equal.

theorem operator_eq_of_mem_commutant_of_eq_on_cyclicVector
    (M : VonNeumannAlgebra H) (Ω : H)
    (hcyclic : DenseRange (fun x : Algebra M => x.val Ω))
    (q r : H →L[ℂ] H) (hq : q ∈ M.commutant) (hr : r ∈ M.commutant)
    (hΩ : q Ω = r Ω) : q = r := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.tracialConjugationDefect_commute_both_of_cyclic line 162

Source documentation

Common commutant membership and the common cyclic-vector value supply the two commutation premises in the tracial-conjugation bound.

theorem tracialConjugationDefect_commute_both_of_cyclic
    (M : VonNeumannAlgebra H) (Ω : H)
    (hcyclic : DenseRange (fun x : Algebra M => x.val Ω))
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (hJ₁ : Function.Involutive J₁) (hJ₂ : Function.Involutive J₂)
    (a : H →L[ℂ] H)
    (h₁ : conjugationOperator J₁ a ∈ M.commutant)
    (h₂ : conjugationOperator J₂ a ∈ M.commutant)
    (hΩ : conjugationOperator J₁ a Ω = conjugationOperator J₂ a Ω) :
    Commute (tracialConjugationDefect J₁ J₂) a ∧
      Commute (tracialConjugationDefect J₁ J₂) (conjugationOperator J₁ a) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.tracialConjugationDefect