OAI/Topology/CoarseAssembly/ConcreteTransferMaps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The controlled fiber maps on the separated coarse union

Within a component these are compositions of graph-edge maps. On the finitely many relevant cross-component pairs they are rank-one constant maps. This discharges the second geometric hypothesis of the transfer criterion on the actual coarse spaces.

  1. theorem OAI.CoarseAssembly.vertexUnion_dist_same line 22
  2. def OAI.CoarseAssembly.constantMap line 33
  3. theorem OAI.CoarseAssembly.constantMap_norm line 38
  4. theorem OAI.CoarseAssembly.constantMap_constant line 45
  5. theorem OAI.CoarseAssembly.concrete_controlled_fiber_maps line 54