OAI/Topology/CoarseAssembly/AnalyticFamilyIndex.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A whole-union index on the actual analytic K-homology domain

Restriction homomorphisms into a family of finite Rips function algebras are explicit parameters. The map descends through every relation of the original Fredholm-module group, without a countable-additivity assumption.

  1. theorem OAI.CoarseAssembly.Rips.analyticFamilyIndexFree_relation line 22
  2. theorem OAI.CoarseAssembly.Rips.analyticFamilyIndex_eq_lift line 43
  3. theorem OAI.CoarseAssembly.Rips.analyticFamilyIndex_class line 62