OAI/Topology/CoarseAssembly/RepresentedIndex.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The Toeplitz index for nonunital representations

A represented unitary is extended by the identity on the complement of the represented subspace. This supplies a genuine unitary even when the original representation does not preserve the unit.

  1. def OAI.CoarseAssembly.Analytic.unitaryExtension line 19
  2. theorem OAI.CoarseAssembly.Analytic.unitaryExtension_star line 22
  3. theorem OAI.CoarseAssembly.Analytic.unitaryExtension_mul line 27
  4. theorem OAI.CoarseAssembly.Analytic.unitaryExtension_unitary line 33
  5. theorem OAI.CoarseAssembly.Analytic.unitaryExtension_commutator line 40
  6. def OAI.CoarseAssembly.Analytic.representedToeplitz line 48
  7. def OAI.CoarseAssembly.Analytic.representedIndex line 51
  8. theorem OAI.CoarseAssembly.Analytic.representedToeplitz_fredholm line 54
  9. theorem OAI.CoarseAssembly.Analytic.exists_representedToeplitz_fredholm line 65
  10. theorem OAI.CoarseAssembly.Analytic.representedIndex_homotopy line 72
  11. theorem OAI.CoarseAssembly.Analytic.representedIndex_degenerate line 90