OAI/Topology/CoarseAssembly/IndexPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar-unitary index pairing on odd analytic K-homology

All four defining Fredholm-cycle relations are respected by the explicit Toeplitz index. Hence it descends to the existing quotient group.

  1. def OAI.CoarseAssembly.Analytic.indexFree line 17
  2. theorem OAI.CoarseAssembly.Analytic.indexFree_relation line 20
  3. def OAI.CoarseAssembly.Analytic.indexPairing line 33

    Source documentation

    Pairing an odd analytic class with an actual scalar unitary.

    def indexPairing (u : A) (hul : star u * u = 1) (hur : u * star u = 1) : OddK A →+ ℤ :=
…

    Mentions: OAI.CoarseAssembly.Analytic.OddK

  4. theorem OAI.CoarseAssembly.Analytic.indexPairing_cycleClass line 37
  5. theorem OAI.CoarseAssembly.Analytic.indexPairing_precomp line 44