OAI/Topology/CoarseAssembly/SpatialBoundaryNaturality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The boundary representative respects spatial Roe maps

The target Fredholm operator is extended by the identity on the complement of the spatial isometry. The conclusion is the actual K₁ map equality.

  1. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryUnitary_spatial line 29
  2. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_spatial line 57