OAI/Topology/CoarseAssembly/AnalyticKHomology.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The odd Fredholm-module group

The group is formed from actual analytic cycles, modulo degeneracy, unitary equivalence, orthogonal direct sum and norm homotopy. Pullback of star representations descends to this quotient. This gives the analytic domain needed for the subsequent geometric construction; no assembly or nonzero class is postulated here.

  1. theorem OAI.CoarseAssembly.Analytic.relation_zero line 26
  2. theorem OAI.CoarseAssembly.Analytic.degenerate_zero line 30
  3. theorem OAI.CoarseAssembly.Analytic.unitary_eq line 33
  4. theorem OAI.CoarseAssembly.Analytic.directSum_eq line 38
  5. theorem OAI.CoarseAssembly.Analytic.homotopy_eq line 43
  6. theorem OAI.CoarseAssembly.Analytic.precompFree_relation line 50
  7. theorem OAI.CoarseAssembly.Analytic.precomp_cycleClass line 65
  8. theorem OAI.CoarseAssembly.Analytic.hom_ext line 69
  9. theorem OAI.CoarseAssembly.Analytic.precomp_id line 74
  10. theorem OAI.CoarseAssembly.Analytic.precomp_comp line 79