OAI/Topology/CoarseAssembly/RipsReindex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Isometric reindexing of coarse homology

The two sigma-type presentations of the fibered vertex set give isomorphic Rips coarsening limits. This is used to compare the graph detector with the vertex indexing of the spatial transfer.

  1. theorem OAI.CoarseAssembly.Rips.equiv_inverse_isometry line 22
  2. theorem OAI.CoarseAssembly.Rips.mapPoint_equiv_inverse line 27
  3. def OAI.CoarseAssembly.Rips.reindexHomology line 42
  4. theorem OAI.CoarseAssembly.Rips.reindexHomology_inverse line 45
  5. theorem OAI.CoarseAssembly.Rips.reindexHomology_injective line 67