OAI/Topology/CoarseAssembly/CompactIndexPairing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The scalar-unitary pairing for compact spaces

  1. def OAI.CoarseAssembly.Analytic.compactUnitary line 18

    Source documentation

    A circle-valued map as a unitary in the compact continuous-function algebra.

    def compactUnitary (f : C(X, Circle)) : C(X, ℂ) :=
…
  2. theorem OAI.CoarseAssembly.Analytic.compactUnitary_star_mul line 22
  3. theorem OAI.CoarseAssembly.Analytic.compactUnitary_mul_star line 28
  4. def OAI.CoarseAssembly.Analytic.compactIndexPairing line 33

    Source documentation

    The index pairing on the actual locally finite K-homology group.

    def compactIndexPairing (f : C(X, Circle)) : LocallyFiniteK1 X →+ ℤ :=
…

    Mentions: OAI.CoarseAssembly.Analytic.LocallyFiniteK1

  5. theorem OAI.CoarseAssembly.Analytic.compactIndexPairing_cycleClass line 37
  6. theorem OAI.CoarseAssembly.Analytic.compactFunctionLift_pullback line 43
  7. theorem OAI.CoarseAssembly.Analytic.compactIndexPairing_natural line 50