OAI/Topology/CoarseAssembly/TopologicalK1.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Topological K₁ from stable invertible matrices

The unital group is presented by invertible finite matrices, with the actual matrix-product, stabilization and continuous-path relations. The nonunital group will be the kernel of the scalar-quotient map on the unitization. These definitions keep the analytic assembly target tied to its algebra.

  1. theorem OAI.CoarseAssembly.TopologicalK1.relation_zero line 31
  2. theorem OAI.CoarseAssembly.TopologicalK1.matrixClass_mul line 35
  3. theorem OAI.CoarseAssembly.TopologicalK1.matrixClass_stabilize line 41
  4. theorem OAI.CoarseAssembly.TopologicalK1.matrixClass_homotopy line 46
  5. theorem OAI.CoarseAssembly.TopologicalK1.matrixClass_one line 51
  6. theorem OAI.CoarseAssembly.TopologicalK1.continuous_mapGL line 58
  7. theorem OAI.CoarseAssembly.TopologicalK1.mapGL_stabilize line 65
  8. theorem OAI.CoarseAssembly.TopologicalK1.mapFree_relation line 70
  9. theorem OAI.CoarseAssembly.TopologicalK1.map_matrixClass line 82
  10. theorem OAI.CoarseAssembly.TopologicalK1.hom_ext line 86
  11. theorem OAI.CoarseAssembly.TopologicalK1.mapGL_id line 94
  12. theorem OAI.CoarseAssembly.TopologicalK1.map_id line 98
  13. theorem OAI.CoarseAssembly.TopologicalK1.mapGL_comp line 104
  14. theorem OAI.CoarseAssembly.TopologicalK1.map_comp line 109