Cocycle.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Cocycle algebra in an arbitrary ring, specializing to bounded complex Hilbert-space operators.

def OAI.Dixmier.conjugate line 12
theorem OAI.Dixmier.conjugate_one line 14
theorem OAI.Dixmier.conjugate_mul line 17
theorem OAI.Dixmier.conjugate_sub line 21
def OAI.Dixmier.coboundary line 25
theorem OAI.Dixmier.coboundary_one line 27
theorem OAI.Dixmier.coboundary_cocycle line 31
Source documentation
The coboundary cocycle identity, before taking direct sums.
```
theorem coboundary_cocycle (U : G →* R) (T : R) (g h : G) :
    coboundary U T (g * h) = coboundary U T g + conjugate U g (coboundary U T h) := by
…
```
Mentions: OAI.Dixmier.coboundary, OAI.Dixmier.conjugate
theorem OAI.Dixmier.conjugate_eq_self_iff_commute line 36
theorem OAI.Dixmier.equal_coboundaries_iff_commute_sub line 50
Source documentation
Comparing the two implementers gives the commutant element T - B.
```
theorem equal_coboundaries_iff_commute_sub (U : G →* R) (T B : R) (g : G) :
    coboundary U T g = coboundary U B g ↔ Commute (U g) (T - B) := by
…
```
Mentions: OAI.Dixmier.coboundary
def OAI.Dixmier.triangular line 67
Source documentation
Algebraic upper triangular operator product, without any norm assertion.
```
def triangular (a b : R) : R × R → R × R :=
…
```
theorem OAI.Dixmier.triangular_cocycle_mul line 70