FiniteRowAverages.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite row averages, their composition law, and the cochain identity. These are the algebraic operations of Christensen--Sinclair row averaging. No existence of an invariant averaging projection is assumed here.

def OAI.KadisonKastler.finiteRightAverage line 18
Source documentation
Average a linear map by a finite row.
```
def finiteRightAverage (r : ι → A) : (A →ₗ[ℂ] A) →ₗ[ℂ] (A →ₗ[ℂ] A) where
…
```
theorem OAI.KadisonKastler.finiteRightAverage_apply line 26

theorem OAI.KadisonKastler.finiteRightAverage_fixed line 30

Source documentation

A normalized row fixes right module maps.

theorem finiteRightAverage_fixed (r : ι → A) (hr : ∑ i, r i * star (r i) = 1)
    (F : A →ₗ[ℂ] A) (hF : ∀ x y, F (x * y) = F x * y) :
    finiteRightAverage r F = F := by
…

Mentions: OAI.KadisonKastler.finiteRightAverage

theorem OAI.KadisonKastler.finiteRightAverage_comp line 37

Source documentation

Composition corresponds to the product row.

theorem finiteRightAverage_comp (r : ι → A) (s : κ → A) (F : A →ₗ[ℂ] A) :
    finiteRightAverage r (finiteRightAverage s F) =
      finiteRightAverage (fun ij : ι × κ => r ij.1 * s ij.2) F := by
…

Mentions: OAI.KadisonKastler.finiteRightAverage

theorem OAI.KadisonKastler.finiteRow_product_normalized line 45

Source documentation

The product row is normalized whenever its factors are.

theorem finiteRow_product_normalized (r : ι → A) (s : κ → A)
    (hr : ∑ i, r i * star (r i) = 1) (hs : ∑ j, s j * star (s j) = 1) :
    ∑ ij : ι × κ, (r ij.1 * s ij.2) * star (r ij.1 * s ij.2) = 1 := by
…

theorem OAI.KadisonKastler.finiteRightAverage_left_input line 55
Source documentation
Finite averaging commutes with precomposition by left multiplication.
```
theorem finiteRightAverage_left_input (r : ι → A) (F : A →ₗ[ℂ] A) (a x : A) :
    (∑ i, F (a * (x * r i)) * star (r i)) = finiteRightAverage r F (a * x) := by
…
```
Mentions: OAI.KadisonKastler.finiteRightAverage
def OAI.KadisonKastler.finiteCochainAverage line 60
Source documentation
The linear cochain obtained by averaging the last argument.
```
def finiteCochainAverage (r : ι → A) (f : A →ₗ[ℂ] A →ₗ[ℂ] A) : A →ₗ[ℂ] A where
…
```
theorem OAI.KadisonKastler.finiteCochainAverage_apply line 65
def OAI.KadisonKastler.cochainDifferential line 70
Source documentation
The scalar Hochschild differential of a bilinear cochain.
```
def cochainDifferential (f : A →ₗ[ℂ] A →ₗ[ℂ] A) (x y z : A) : A :=
…
```
theorem OAI.KadisonKastler.finiteCochainAverage_residual line 75
Source documentation
The cochain residual is exactly a module defect minus the averaged Hochschild differential. The module defect vanishes at an invariant limit.
```
theorem finiteCochainAverage_residual (r : ι → A)
    (hr : ∑ i, r i * star (r i) = 1) (f : A →ₗ[ℂ] A →ₗ[ℂ] A) (x y : A) :
    f x y - linearCoboundary (finiteCochainAverage r f) x y =
      finiteRightAverage r (f x) y - finiteCochainAverage r f x * y -
        ∑ i, cochainDifferential f x y (r i) * star (r i) := by
…
```
Mentions: OAI.KadisonKastler.linearCoboundary, OAI.KadisonKastler.finiteCochainAverage, OAI.KadisonKastler.finiteRightAverage, OAI.KadisonKastler.cochainDifferential