OAI/Topology/CoarseAssembly/CongruenceMaps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compatible reductions between the congruence fibers

These are the actual entrywise reductions, including level zero. In particular, the compatibility of the chosen holonomy is a theorem, not an extra assumption on the graph construction.

  1. theorem OAI.CoarseAssembly.Congruence.quotientMap_self line 15
  2. theorem OAI.CoarseAssembly.Congruence.quotientMap_comp line 21
  3. theorem OAI.CoarseAssembly.Congruence.quotientMap_reduce line 30
  4. theorem OAI.CoarseAssembly.Congruence.map_diagonal line 36
  5. theorem OAI.CoarseAssembly.Congruence.quotientMap_holonomy line 46
  6. instance OAI.CoarseAssembly.Congruence.quotientZeroSubsingleton line 53