OAI/Topology/CoarseAssembly/NonUnitalK1.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

K₁ of nonunital C*-algebras

The group is the kernel of the scalar projection from the unitization. Nonunital star homomorphisms induce actual maps of these kernels, preserving composition. This is the target functor for the reduced Roe assembly map.

  1. theorem OAI.CoarseAssembly.OperatorKTheory.scalarMap_matrixClass line 28
  2. theorem OAI.CoarseAssembly.OperatorKTheory.unitizationMap_matrixClass line 35
  3. theorem OAI.CoarseAssembly.OperatorKTheory.scalarMap_natural line 42
  4. theorem OAI.CoarseAssembly.OperatorKTheory.map_coe line 55
  5. theorem OAI.CoarseAssembly.OperatorKTheory.unitizationMap_comp line 58
  6. theorem OAI.CoarseAssembly.OperatorKTheory.map_comp line 71
  7. theorem OAI.CoarseAssembly.OperatorKTheory.unitizationMap_id line 78
  8. theorem OAI.CoarseAssembly.OperatorKTheory.map_id line 91