OAI/Topology/CoarseAssembly/RipsScaleCompatibility.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Increasing-scale compatibility of the explicit Rips representatives

The barycentric coordinate functions pull back identically under increasing the Rips scale. Consequently the localized operators themselves agree, before taking a K-theory class.

  1. def OAI.CoarseAssembly.Rips.scaleFunctionHom line 21
  2. theorem OAI.CoarseAssembly.Rips.scaleFunctionHom_sqrt line 25
  3. def OAI.CoarseAssembly.Rips.coarsenedCycle line 28
  4. theorem OAI.CoarseAssembly.Rips.coarsenedCycle_unital line 31
  5. theorem OAI.CoarseAssembly.Rips.coarsenedCycle_representedSqrt line 36
  6. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_scale line 41
  7. theorem OAI.CoarseAssembly.Rips.ampleRipsOperator_scale line 47
  8. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_scale line 55