OAI/Topology/CoarseAssembly/ControlledRipsCoarsening.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Coarsening and the constructed controlled assembly homomorphism

  1. def OAI.CoarseAssembly.Rips.ControlledCycleFamily.coarsen line 17
  2. def OAI.CoarseAssembly.Rips.ControlledFamilyHomotopy.coarsen line 26
  3. theorem OAI.CoarseAssembly.Rips.ControlledFamilyHomotopy.coarsen_eval line 37
  4. theorem OAI.CoarseAssembly.Rips.controlled_coarsen_relation line 41
  5. def OAI.CoarseAssembly.Rips.controlledCoarsening line 65
  6. theorem OAI.CoarseAssembly.Rips.controlledCoarsening_class line 70
  7. theorem OAI.CoarseAssembly.Rips.controlled_hom_ext line 74
  8. theorem OAI.CoarseAssembly.Rips.ControlledCycleFamily.coarsen_refl line 81
  9. theorem OAI.CoarseAssembly.Rips.ControlledCycleFamily.coarsen_comp line 87
  10. theorem OAI.CoarseAssembly.Rips.controlledCoarsening_refl line 93
  11. theorem OAI.CoarseAssembly.Rips.controlledCoarsening_comp line 100
  12. theorem OAI.CoarseAssembly.Rips.controlledAssembly_coarsening line 110

    Source documentation

    Scale compatibility holds for the whole constructed map on the quotient, not only for its chosen cycle representatives.

    theorem controlledAssembly_coarsening (o : ∀ i, Q i) (hr : 0 ≤ r) (hs : 0 ≤ s)
    (hrs : r ≤ s) :
    letI := separatedMetric o
…

    Mentions: OAI.CoarseAssembly.separatedMetric

  13. theorem OAI.CoarseAssembly.Rips.controlledCoordinate_coarsening line 125