OAI/Topology/CoarseAssembly/ClopenRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restricting analytic K-homology to a compact open component

Extension by zero is constructed on the actual continuous-function algebras. Its contravariant action on Fredholm modules is a left inverse to pushforward of the component inclusion. No additivity theorem is needed for this restriction calculation.

  1. theorem OAI.CoarseAssembly.Analytic.continuous_zeroExtension line 26
  2. theorem OAI.CoarseAssembly.Analytic.zeroExtension_apply line 35
  3. theorem OAI.CoarseAssembly.Analytic.zeroExtension_apply_outside line 39
  4. def OAI.CoarseAssembly.Analytic.compactOpenInclusion line 43
  5. def OAI.CoarseAssembly.Analytic.restrictComponent line 46
  6. theorem OAI.CoarseAssembly.Analytic.restrictComponent_pushforward line 49