OAI/Topology/CoarseAssembly/StructureQuotient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The Roe ideal and the algebraic analytic-index quotient

This is the actual two-sided ideal in the controlled pseudolocal algebra. The quotient norm and the analytic-index class are constructed separately.

  1. def OAI.CoarseAssembly.DiscreteRoe.roeIdeal line 20
  2. theorem OAI.CoarseAssembly.DiscreteRoe.mem_roeIdeal line 28
  3. theorem OAI.CoarseAssembly.DiscreteRoe.roeIdeal_closed line 32
  4. abbrev OAI.CoarseAssembly.DiscreteRoe.StructureQuotient line 41
  5. def OAI.CoarseAssembly.DiscreteRoe.structureQuotientMap line 43
  6. theorem OAI.CoarseAssembly.DiscreteRoe.structureQuotientMap_eq line 50