ConjugateRightAlgebra.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual conjugate right algebra

An involutive conjugate-linear Hilbert isometry transports a concrete von Neumann algebra to its exact operator image. Conjugating an ambient contractive projection twice transports injectivity as well. These constructions preserve the represented algebraic operations.

theorem OAI.KadisonKastler.conjugationOperator_add line 20
theorem OAI.KadisonKastler.conjugationOperator_smul line 26
theorem OAI.KadisonKastler.conjugateIsometry_inner line 32
theorem OAI.KadisonKastler.conjugationOperator_star line 57
Source documentation
Conjugation by an involutive anti-isometry preserves operator adjoints.
```
theorem conjugationOperator_star (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (a : H →L[ℂ] H) :
    conjugationOperator J (star a) = star (conjugationOperator J a) := by
…
```
Mentions: OAI.KadisonKastler.conjugationOperator
theorem OAI.KadisonKastler.centralizer_image_conjugationOperator line 76
def OAI.KadisonKastler.conjugateRightStarAlgebra line 92

def OAI.KadisonKastler.conjugateRightAlgebra line 112

Source documentation

The actual image J R J, as a concrete von Neumann algebra.

def conjugateRightAlgebra (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R : VonNeumannAlgebra H) : VonNeumannAlgebra H where
…

theorem OAI.KadisonKastler.conjugateRightAlgebra_coe line 121

def OAI.KadisonKastler.conjugateOperatorMap line 127

Source documentation

Conjugating a complex-linear map twice restores complex linearity.

def conjugateOperatorMap (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H)) :
    (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H) :=
…

theorem OAI.KadisonKastler.conjugateOperatorMap_apply line 146
theorem OAI.KadisonKastler.norm_conjugateOperatorMap_le line 150
theorem OAI.KadisonKastler.isInjective_conjugateRightAlgebra line 159
Source documentation
An actual ambient contractive projection onto R gives one onto J R J.
```
theorem isInjective_conjugateRightAlgebra
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (R : VonNeumannAlgebra H) (hR : IsInjective R) :
    IsInjective (conjugateRightAlgebra J hJ R) := by
…
```
Mentions: OAI.KadisonKastler.IsInjective, OAI.KadisonKastler.conjugateRightAlgebra
theorem OAI.KadisonKastler.exists_preparedRight_graph_comparison_of_injective line 181
Source documentation
The generic preparation theorem needs only injectivity of the common left algebra; the right algebra and its injectivity are constructed.
```
theorem exists_preparedRight_graph_comparison_of_injective
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding