UnitalRepresentative.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Unital representatives for compact-source analytic classes

Adjoin a degenerate character cycle and exchange the complementary subspaces by the explicit projection-swap unitary. This proves that completion of a representation by a character preserves its class.

theorem OAI.CoarseAssembly.Analytic.projectionSwap_representation line 21
theorem OAI.CoarseAssembly.Analytic.projectionSwap_operator line 51
theorem OAI.CoarseAssembly.Analytic.characterExtension_class line 82
theorem OAI.CoarseAssembly.Analytic.exists_unital_representative line 109
Source documentation
Every analytic cycle over an algebra with a character has a unital representative. The assertion includes equality in the actual cycle quotient.
```
theorem exists_unital_representative (c : OddCycle A) (χ : A →⋆ₐ[ℂ] ℂ) :
    ∃ d : OddCycle A, cycleClass A d = cycleClass A c ∧ d.representation 1 = 1 := by
…
```
Mentions: OAI.CoarseAssembly.Analytic.OddCycle, OAI.CoarseAssembly.Analytic.cycleClass
theorem OAI.CoarseAssembly.Analytic.exists_unital_involutive_representative line 119
Source documentation
The representatives needed by whole-family Rips localization can be chosen unital, self-adjoint, involutive, and uniformly bounded by one.
```
theorem exists_unital_involutive_representative (c : OddCycle A) (χ : A →⋆ₐ[ℂ] ℂ) :
    ∃ d : OddCycle A, cycleClass A d = cycleClass A c ∧ d.representation 1 = 1 ∧
      IsSelfAdjoint d.operator ∧ d.operator * d.operator = 1 ∧ ‖d.operator‖ ≤ 1 := by
…
```
Mentions: OAI.CoarseAssembly.Analytic.OddCycle, OAI.CoarseAssembly.Analytic.cycleClass