OAI/Analysis/BoundedHochschild/HomogeneousTypeIPrimitives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Norm-one primitives on finite homogeneous type I algebras

Finite central partitions and signed permutation groups give exact homotopies on central projection multiples of matrix entries. Their bounded weak-star limit is exact everywhere by the projection-span theorem in the commutant.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.finite_homogeneous_typeI_primitive line 28
  2. theorem OAI.BoundedHochschild.KadisonRingrose.finite_homogeneous_typeI_primitive_of_abelian_diagonal line 89

    Source documentation

    An abelian diagonal corner is the concrete homogeneous type I hypothesis.

    theorem finite_homogeneous_typeI_primitive_of_abelian_diagonal
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) {d : ℕ} (E : MatrixSystem M d) (i : Fin d)
    (hi : FinitePathMain.AbelianProjection (E.entry i i))
    {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.FinitePathMain.AbelianProjection, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue