OAI/Topology/CoarseAssembly/ControlledCoarseAssembly.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The coarsening-limit assembly for controlled component families

This is the direct limit of the constructed analytic quotient maps. Relating its source to full locally finite K-homology is a separate remaining theorem.

  1. def OAI.CoarseAssembly.Rips.controlledScaleMap line 21
  2. instance OAI.CoarseAssembly.Rips.controlledDirectedSystem line 24
  3. abbrev OAI.CoarseAssembly.Rips.ControlledCoarseK line 37
  4. def OAI.CoarseAssembly.Rips.controlledCoarseOf line 40
  5. def OAI.CoarseAssembly.Rips.controlledCoarseAssembly line 47

    Source documentation

    An actual compatible assembly map on the controlled component model.

    def controlledCoarseAssembly (o : ∀ i, Q i) :
    letI := separatedMetric o
…

    Mentions: OAI.CoarseAssembly.separatedMetric

  6. theorem OAI.CoarseAssembly.Rips.controlledCoarseAssembly_of line 60
  7. theorem OAI.CoarseAssembly.Rips.controlledCoarseAssembly_cycle line 66