OAI/Topology/CoarseAssembly/ControlledRipsCycles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Controlled analytic cycles for the separated finite-component application

This intermediate cycle group retains uniform analytic homotopy control. Its map to ordinary analytic coordinates is constructed explicitly; no identification with the full locally finite analytic group is assumed.

  1. structure OAI.CoarseAssembly.Rips.ControlledFamilyHomotopy line 25
  2. def OAI.CoarseAssembly.Rips.ControlledFamilyHomotopy.eval line 42
  3. inductive OAI.CoarseAssembly.Rips.ControlledCycleRelation line 51
  4. def OAI.CoarseAssembly.Rips.controlledRelations line 63
  5. abbrev OAI.CoarseAssembly.Rips.ControlledK line 67
  6. def OAI.CoarseAssembly.Rips.controlledClass line 71
  7. theorem OAI.CoarseAssembly.Rips.controlled_relation_zero line 74
  8. def OAI.CoarseAssembly.Rips.controlledBoundaryFree line 78
  9. theorem OAI.CoarseAssembly.Rips.controlledBoundaryFree_relation line 86
  10. def OAI.CoarseAssembly.Rips.controlledAssembly line 115

    Source documentation

    The constructed whole-union Roe boundary descends through every relation of this controlled analytic cycle model.

    def controlledAssembly (o : ∀ i, Q i) (hr : 0 ≤ r) :
    letI := separatedMetric o
…

    Mentions: OAI.CoarseAssembly.separatedMetric

  11. theorem OAI.CoarseAssembly.Rips.controlledAssembly_class line 127