OAI/Topology/CoarseAssembly/CountableAdditivity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Countable additivity in the first KK variable

The coordinate maps below are the proved extension-by-zero restrictions on actual Fredholm-module groups. The sole published input is their bijectivity: Blackadar, K-Theory for Operator Algebras, 2nd ed. (1998), Theorem 19.7.1, for a countable disjoint union of compact metrizable spaces. Construction of a family class and vanishing from vanishing coordinates are consequences, not assumed inputs.

  1. def OAI.CoarseAssembly.Analytic.sigmaComponent line 24
  2. theorem OAI.CoarseAssembly.Analytic.sigmaComponent_open line 26
  3. def OAI.CoarseAssembly.Analytic.sigmaCoordinates line 31
  4. def OAI.CoarseAssembly.Analytic.CountableAdditivityInput line 38

    Source documentation

    The exact countable-additivity specialization used in this application. This is a published input on a specified family of spaces.

    def CountableAdditivityInput : Prop := Function.Bijective (sigmaCoordinates Y)

    Mentions: OAI.CoarseAssembly.Analytic.sigmaCoordinates

  5. def OAI.CoarseAssembly.Analytic.sigmaKKEquiv line 40
  6. def OAI.CoarseAssembly.Analytic.familyClass line 45

    Source documentation

    Assemble an integral family before any tensoring with the rationals.

    def familyClass (h : CountableAdditivityInput Y) (a : ∀ j, LocallyFiniteK1 (Y j)) :
    LocallyFiniteK1 (Sigma Y) := (sigmaKKEquiv Y h).symm a

    Mentions: OAI.CoarseAssembly.Analytic.CountableAdditivityInput, OAI.CoarseAssembly.Analytic.LocallyFiniteK1, OAI.CoarseAssembly.Analytic.sigmaKKEquiv

  7. theorem OAI.CoarseAssembly.Analytic.familyClass_coordinate line 48
  8. theorem OAI.CoarseAssembly.Analytic.eq_zero_of_coordinates line 54
  9. theorem OAI.CoarseAssembly.Analytic.sigma_group_subsingleton line 64