FiniteUnitaryPrimitives.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite unitary averaging for type I pieces

The separability homotopy of a finite group of unitaries has norm at most one. It is exact in the first variable on the linear span of the group. This is the finite-dimensional ingredient of the classical type I vanishing argument.

lemma OAI.BoundedHochschild.KadisonRingrose.differentialValue_leftOutput line 22
lemma OAI.BoundedHochschild.KadisonRingrose.first_separability_identity line 31
lemma OAI.BoundedHochschild.KadisonRingrose.unitary_norm_le line 42
def OAI.BoundedHochschild.KadisonRingrose.finiteUnitaryHomotopy line 47
Source documentation
The finite Haar average of the first-variable contracting homotopies.
```
def finiteUnitaryHomotopy (ρ : G →* unitary M) {n : ℕ}
    (f : Cochain M (n + 1)) : Cochain M n :=
…
```
Mentions: OAI.BoundedHochschild.Cochain
lemma OAI.BoundedHochschild.KadisonRingrose.finiteUnitaryHomotopy_norm line 52
lemma OAI.BoundedHochschild.KadisonRingrose.finiteUnitaryHomotopy_exact_unitary line 77
lemma OAI.BoundedHochschild.KadisonRingrose.finiteUnitaryHomotopy_exact_span line 114

theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_locally_finite_unitaries line 141

Source documentation

Norm-one primitives for the locally finite unitary families used in the finite homogeneous type I argument. The hypotheses are concrete group and norm-density data, independent of cochains.

theorem primitive_of_locally_finite_unitaries (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (S : Set (unitary M))
    (hfinite : ∀ s : Finset S, ∃ H : Subgroup (unitary M),
      Finite H ∧ ∀ u ∈ s, (u : unitary M) ∈ H)
    (hdense : (Submodule.span ℂ (Set.range (fun u : S => ((u : unitary M) : M)))).topologicalClosure = ⊤)
    {n : ℕ} (f : Cochain M (n + 1)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M n, ‖g‖ ≤ ‖f‖ ∧ ∀ x, differentialValue g x = f x := by
…

Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue