FiniteTypeIVanishing.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unconditional bounded Hochschild vanishing on finite type I algebras.

theorem OAI.BoundedHochschild.KadisonRingrose.finite_typeI_central_partition line 19
theorem OAI.BoundedHochschild.KadisonRingrose.finite_typeI_primitive line 31
Source documentation
Finite type I algebras have bounded primitives in every positive degree. The bound is independent of the ranks of their homogeneous central pieces.
```
theorem finite_typeI_primitive (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (hI : TypeICentralSummand (1 : M))
    {n : ℕ} (f : Cochain M (n + 1)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M n, ‖g‖ ≤ ‖f‖ + n * ‖f‖ ∧ ∀ x, differentialValue g x = f x := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue
theorem OAI.BoundedHochschild.KadisonRingrose.finite_typeI_of_noTypeII1 line 58
Source documentation
In a finite algebra the absence of a type II₁ central summand forces type I.
```
theorem finite_typeI_of_noTypeII1 (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (hno : NoTypeII1Summand M) :
    TypeICentralSummand (1 : M) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand
theorem OAI.BoundedHochschild.KadisonRingrose.finite_noTypeII1_primitive line 72
Source documentation
The entire finite case of the classical non-II₁ vanishing input.
```
theorem finite_noTypeII1_primitive (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (hno : NoTypeII1Summand M)
    {n : ℕ} (f : Cochain M (n + 2)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M (n + 1), ‖g‖ ≤ ‖f‖ + (n + 1) * ‖f‖ ∧
      ∀ x, differentialValue g x = f x := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue