OAI/Topology/CoarseAssembly/PointCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The odd analytic coefficient group of a point

All scalar Fredholm cycles vanish by explicit operator normalization. The constant-function and evaluation maps identify the point coefficient algebra with the scalars, so its odd group vanishes as well.

  1. def OAI.CoarseAssembly.Analytic.pointConstants line 19
  2. def OAI.CoarseAssembly.Analytic.pointEvaluation line 27
  3. theorem OAI.CoarseAssembly.Analytic.pointConstants_evaluation line 35
  4. theorem OAI.CoarseAssembly.Analytic.point_cycleClass_zero line 41
  5. theorem OAI.CoarseAssembly.Analytic.subsingleton_of_cycleClass_zero line 47
  6. theorem OAI.CoarseAssembly.Analytic.point_odd_zero line 58