OAI/Topology/CoarseAssembly/FredholmSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional kernels from the compact square defect

The kernel of F lies in the -1 eigenspace of the compact operator F² - 1. This supplies the finite-dimensional obstruction needed before replacing a unital odd Fredholm operator by an invertible one.

  1. theorem OAI.CoarseAssembly.Analytic.finiteDimensional_ker_of_compact_square line 17
  2. theorem OAI.CoarseAssembly.Analytic.OddCycle.finiteDimensional_ker line 34