OAI/Topology/CoarseAssembly/MultiplierBoundaryClass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Boundary classes in the closed Roe multiplier algebra

A controlled Rips operator is a Roe multiplier even when it is not pseudolocal for the discrete vertex representation. The ideal-boundary construction is therefore performed in this actual closed multiplier algebra before constructing the coarse assembly map.

  1. theorem OAI.CoarseAssembly.DiscreteRoe.roeIdealizer_one line 29
  2. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra_closed line 35
  3. theorem OAI.CoarseAssembly.DiscreteRoe.mem_multiplierRoeIdeal line 38
  4. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryUnitary_sub_one_mem line 42