OAI/Topology/CoarseAssembly/LocallyFinite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Locally finite analytic K-homology and coarsening

The domain is the odd Fredholm-module group of the actual algebra Cā‚€(Y, ā„‚). A proper continuous map acts by pulling back functions and representations. The coarsening limit is an actual algebraic direct limit of those groups.

  1. theorem OAI.CoarseAssembly.Analytic.pullback_apply line 26
  2. theorem OAI.CoarseAssembly.Analytic.pullback_comp line 29
  3. theorem OAI.CoarseAssembly.Analytic.pullback_id line 34
  4. theorem OAI.CoarseAssembly.Analytic.pushforward_comp line 38
  5. theorem OAI.CoarseAssembly.Analytic.pushforward_id line 43
  6. instance OAI.CoarseAssembly.Analytic.Coarsening.(instance at line 50) line 50
  7. def OAI.CoarseAssembly.Analytic.Coarsening.of line 58