Derivations.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The triangular representation of a bounded derivation

Similarity of the upper triangular representation gives an inner implementer for a bounded derivation.

theorem OAI.KadisonSimilarity.orthogonal_projection_commutes line 22

Source documentation

The orthogonal projection onto a closed subspace invariant under a family and its adjoints commutes with that family.

theorem orthogonal_projection_commutes (U : A → (H →L[ℂ] H))
    (hstar : ∀ a, U (star a) = star (U a)) (M : ClosedSubmodule ℂ H)
    (hM : ∀ a x, x ∈ M → U a x ∈ M) (a : A) :
    Commute M.toSubmodule.starProjection (U a) := by
…

theorem OAI.KadisonSimilarity.exists_commuting_projection line 40

Source documentation

Similarity to a star representation supplies a bounded commuting projection onto every closed invariant subspace.

theorem exists_commuting_projection (π : BoundedUnitalHom A H)
    (hπ : SimilarToStar A H π) (M : ClosedSubmodule ℂ H)
    (hM : ∀ a x, x ∈ M → π.1 a x ∈ M) :
    ∃ P : H →L[ℂ] H, (∀ x, P x ∈ M) ∧
      (∀ x, x ∈ M → P x = x) ∧ ∀ a, Commute P (π.1 a) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.SimilarToStar

def OAI.KadisonSimilarity.Derivation.triangularOperator line 81
Source documentation
The bounded upper triangular operator with equal diagonal blocks.
```
def triangularOperator (σ d : H →L[ℂ] H) : Double H →L[ℂ] Double H :=
…
```
theorem OAI.KadisonSimilarity.Derivation.triangularOperator_fst line 85
theorem OAI.KadisonSimilarity.Derivation.triangularOperator_snd line 90
theorem OAI.KadisonSimilarity.Derivation.map_one_eq_zero line 96
Source documentation
A bounded derivation vanishes at the identity.
```
theorem map_one_eq_zero (σ : BoundedUnitalHom A H) (δ : A →L[ℂ] (H →L[ℂ] H))
    (hδ : ∀ a b, δ (a * b) = σ.1 a * δ b + δ a * σ.1 b) : δ 1 = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom
def OAI.KadisonSimilarity.Derivation.representation line 104
Source documentation
The triangular algebra representation associated to a bounded derivation.
```
def representation (σ : BoundedUnitalHom A H) (δ : A →L[ℂ] (H →L[ℂ] H))
    (hδ : ∀ a b, δ (a * b) = σ.1 a * δ b + δ a * σ.1 b) :
    BoundedUnitalHom A (Double H) := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom
theorem OAI.KadisonSimilarity.Derivation.inner_of_similar line 141
Source documentation
A similarity of the triangular representation provides an inner implementer for the derivation.
```
theorem inner_of_similar (σ : BoundedUnitalHom A H) (δ : A →L[ℂ] (H →L[ℂ] H))
    (hδ : ∀ a b, δ (a * b) = σ.1 a * δ b + δ a * σ.1 b)
    (hsim : SimilarToStar A (Double H) (representation σ δ hδ)) :
    ∃ V : H →L[ℂ] H, ∀ a, δ a = V * σ.1 a - σ.1 a * V := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.SimilarToStar, OAI.KadisonSimilarity.Derivation.representation
def OAI.KadisonSimilarity.AlgebraSimilarityProperty line 186
Source documentation
The similarity property of one algebra, with an independent universe for Hilbert spaces. This is property (SP) in Ozawa's formulation.
```
def AlgebraSimilarityProperty (A : Type u) [CStarAlgebra A] : Prop :=
…
```
def OAI.KadisonSimilarity.FaithfulStarDerivationsInner line 192
Source documentation
The bounded form of property (DP): innerness is tested in every faithful unital star representation, independently of a bounded homomorphism under test.
```
def FaithfulStarDerivationsInner (A : Type u) [CStarAlgebra A] : Prop :=
…
```
def OAI.KadisonSimilarity.KirchbergDerivationCriterion line 203
Source documentation
Kirchberg's derivation criterion (1996), as stated in Ozawa, An invitation to the similarity problems, Theorem 1.1, with boundedness supplied by Ringrose (1972), Theorem 2, p. 434.
```
def KirchbergDerivationCriterion (A : Type u) [CStarAlgebra A] : Prop :=
…
```
theorem OAI.KadisonSimilarity.faithfulStarDerivationsInner_of_similarity line 208
Source documentation
The elementary converse to the published Kirchberg implication, proved by the triangular representation and its invariant first summand.
```
theorem faithfulStarDerivationsInner_of_similarity {A : Type u} [CStarAlgebra A]
    (similarity : AlgebraSimilarityProperty.{u,v} A) : FaithfulStarDerivationsInner.{u,v} A := by
…
```