OAI/Topology/CoarseAssembly/HomotopyFilling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The precise homotopy and odd-coefficient inputs for filling

Blackadar, K-Theory for Operator Algebras, 2nd ed. (1998), Proposition 17.9.1 and §19.8.3 give homotopy invariance in the first variable and KK₁(ℂ, ℂ) = 0. Their required specializations are explicit below. Vanishing for a compact contractible space, and then for its countable family, is derived rather than assumed.

  1. structure OAI.CoarseAssembly.Analytic.PublishedCompactHomotopyInput line 22
  2. structure OAI.CoarseAssembly.Analytic.CompactContraction line 29

    Source documentation

    Actual continuous contraction data; this contains no K-theory assertion.

    structure CompactContraction (X : Type) [TopologicalSpace X] where
…
  3. theorem OAI.CoarseAssembly.Analytic.compactMap_comp line 33
  4. theorem OAI.CoarseAssembly.Analytic.compactMap_id line 41
  5. theorem OAI.CoarseAssembly.Analytic.contracted_odd_group_zero line 47
  6. theorem OAI.CoarseAssembly.Analytic.contracted_family_odd_group_zero line 66