OperatorTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The classical input for algebras represented as full operator algebras

Kadison--Ringrose, Cohomology of operator algebras I (1971), Theorem 4.4, includes the type I vanishing result. Here its full-operator-algebra case is proved using the explicit rank-one homotopy in OperatorPrimitives, and is transported across an actual star algebra equivalence. No cohomological vanishing hypothesis is assumed.

def OAI.BoundedHochschild.expectedEmbeddingOfStarAlgEquiv line 24
Source documentation
An algebra equivalence gives mutually inverse contractive expectation maps.
```
def expectedEmbeddingOfStarAlgEquiv (φ : N ≃⋆ₐ[ℂ] M) : ExpectedEmbedding N M where
…
```
Mentions: OAI.BoundedHochschild.ExpectedEmbedding
lemma OAI.BoundedHochschild.expectedEmbeddingOfStarAlgEquiv_surjective line 44
lemma OAI.BoundedHochschild.ExpectedEmbedding.extend_primitive_of_surjective line 51
Source documentation
For a surjective inclusion the finite exactness identity holds at every tuple.
```
lemma extend_primitive_of_surjective (E : ExpectedEmbedding N M)
    (hE : Function.Surjective E.includeMap) {n : ℕ}
    (f : Cochain M (n + 1)) (g : Cochain N n)
    (hg : ∀ x, differentialValue g x = E.restrict f x) :
    ∀ x, differentialValue (E.extend g) x = f x := by
…
```
Mentions: OAI.BoundedHochschild.ExpectedEmbedding, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue

theorem OAI.BoundedHochschild.primitive_of_starAlgEquiv line 63

Source documentation

A norm-controlled primitive is preserved by a star algebra equivalence.

theorem primitive_of_starAlgEquiv (φ : N ≃⋆ₐ[ℂ] M) {n : ℕ}
    (f : Cochain M (n + 1))
    (hN : ∀ F : Cochain N (n + 1), (∀ x, differentialValue F x = 0) →
      ∃ g : Cochain N n, ‖g‖ ≤ ‖F‖ ∧ ∀ x, differentialValue g x = F x)
    (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M n, ‖g‖ ≤ ‖f‖ ∧ ∀ x, differentialValue g x = f x := by
…

Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue

theorem OAI.BoundedHochschild.primitive_of_full_operator_equiv line 78

Source documentation

The non-II₁ classical input is discharged for any actual presentation as B(H). The rank-one homotopy also provides the norm-one primitive bound.

theorem primitive_of_full_operator_equiv
    {M H : Type*} [CStarAlgebra M]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (φ : (H →L[ℂ] H) ≃⋆ₐ[ℂ] M) {n : ℕ}
    (f : Cochain M (n + 1)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M n, ‖g‖ ≤ ‖f‖ ∧ ∀ x, differentialValue g x = f x :=
…

Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue