OAI/Topology/CoarseAssembly/RipsBoundaryDegeneracy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Degenerate families have zero whole-union Roe boundary

Vanishing is proved from an exact global involution, not from vanishing of the individual finite-component K-theory classes.

  1. theorem OAI.CoarseAssembly.isometricExtension_sq_eq_one line 16
  2. theorem OAI.CoarseAssembly.Analytic.localizedOperator_degenerate line 28
  3. theorem OAI.CoarseAssembly.Rips.ripsCompression_degenerate line 44
  4. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_degenerate_sq line 51
  5. theorem OAI.CoarseAssembly.Rips.ampleRipsOperator_degenerate_sq line 62
  6. theorem OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary_involution line 75
  7. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_degenerate line 108