OAI/Topology/CoarseAssembly/RepresentedCutDown.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cutting down arbitrary cycles over the unital coefficient algebras

The compact-source algebras used by the circle pairing are unital, although the Fredholm representations themselves may be nonunital. Restriction to scalar coefficients gives precisely the local estimates needed for the represented-subspace cut-down.

  1. theorem OAI.CoarseAssembly.Analytic.representation_unit_selfAdjoint line 20
  2. theorem OAI.CoarseAssembly.Analytic.representation_unit_sq line 25
  3. theorem OAI.CoarseAssembly.Analytic.representedCutDown_compact line 29
  4. theorem OAI.CoarseAssembly.Analytic.exists_represented_cutDown line 43
  5. theorem OAI.CoarseAssembly.Analytic.represented_square_compact line 74