OAI/Topology/CoarseAssembly/CycleIndex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The scalar-unitary index of normalized odd cycles

This constructs the Fredholm operator and its integer index. Descent to the cycle quotient and the explicit circle-generator calculation are separate steps; neither is assumed by these declarations.

  1. def OAI.CoarseAssembly.Analytic.positiveProjection line 19
  2. theorem OAI.CoarseAssembly.Analytic.positiveProjection_selfAdjoint line 21
  3. theorem OAI.CoarseAssembly.Analytic.positiveProjection_sq line 27
  4. theorem OAI.CoarseAssembly.Analytic.positiveProjection_commutator line 36
  5. def OAI.CoarseAssembly.Analytic.cycleToeplitz line 45
  6. def OAI.CoarseAssembly.Analytic.cycleIndex line 48
  7. theorem OAI.CoarseAssembly.Analytic.cycleToeplitz_fredholm line 50
  8. theorem OAI.CoarseAssembly.Analytic.fredholmIndex_homotopy line 61
  9. theorem OAI.CoarseAssembly.Analytic.cycleIndex_homotopy line 71
  10. theorem OAI.CoarseAssembly.Analytic.cycleIndex_degenerate line 86