OAI/Topology/CoarseAssembly/CompactIndex.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact perturbation invariance of the Fredholm index

The compactness of both the perturbation and its adjoint keeps the straight line path unitary modulo compact operators. Local constancy of the Fredholm index then gives invariance, without a spectral choice of normalization.

  1. theorem OAI.CoarseAssembly.Analytic.essentialUnitary_compactPerturb line 18
  2. theorem OAI.CoarseAssembly.Analytic.fredholmIndex_compactPerturb line 40