OAI/Analysis/KadisonKastler/FiniteCochainDifferential.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.finiteBilinearProduct_apply line 13
2. theorem OAI.KadisonKastler.finiteBilinearProduct_mul line 17
3. theorem OAI.KadisonKastler.finiteBilinearProduct_add line 21
4. theorem OAI.KadisonKastler.finiteBilinearProduct_sub line 27
5. theorem OAI.KadisonKastler.finiteBilinearProduct_add_left line 33
6. theorem OAI.KadisonKastler.finiteBilinearProduct_add_right line 39
7. theorem OAI.KadisonKastler.finiteBilinearProduct_smul line 45
8. theorem OAI.KadisonKastler.finiteBilinearProduct_assoc line 53

   Source documentation

   Algebraic associativity survives every rectangular matrix amplification.

   theorem finiteBilinearProduct_assoc (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
       (hm : ∀ x y z, m (m x y) z = m x (m y z)) {p r s q : Type*} [Fintype r] [Fintype s]
       (X : CStarMatrix p r A) (Y : CStarMatrix r s A)
       (Z : CStarMatrix s q A) :
       finiteBilinearProduct m (finiteBilinearProduct m X Y) Z =
         finiteBilinearProduct m X (finiteBilinearProduct m Y Z) := by
   …

   Mentions: OAI.KadisonKastler.finiteBilinearProduct

9. theorem OAI.KadisonKastler.rectangular_mul_assoc_finite line 64
10. def OAI.KadisonKastler.finiteMatrixDifferential line 74

    Source documentation

    The degree-two Hochschild differential, already amplified to matrices.

    def finiteMatrixDifferential (f : A →ₗ[ℂ] A →ₗ[ℂ] A) {p r s q : Type*} [Fintype r] [Fintype s]
        (X : CStarMatrix p r A) (Y : CStarMatrix r s A)
        (Z : CStarMatrix s q A) : CStarMatrix p q A :=
    …

11. theorem OAI.KadisonKastler.finiteMatrixDifferential_defect line 81

    Source documentation

    The Maurer--Cartan identity, with its signs fixed for the correction step.

    theorem finiteMatrixDifferential_defect (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
        (hm : ∀ x y z, m (m x y) z = m x (m y z)) {p r s q : Type*} [Fintype r] [Fintype s]
        (X : CStarMatrix p r A) (Y : CStarMatrix r s A)
        (Z : CStarMatrix s q A) :
        let f := m - LinearMap.mul ℂ A
    …

12. theorem OAI.KadisonKastler.finiteMatrixDifferential_defect_bound line 107