OAI/Topology/CoarseAssembly/WindingIndexEvaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reducing the winding index formula to one generator evaluation

The pairing, its naturality, homotopy invariance and power law are proved. Only an actual circle class with coordinate index one remains to construct.

  1. theorem OAI.CoarseAssembly.circleUnitary_degree line 17
  2. theorem OAI.CoarseAssembly.winding_index_hom line 23
  3. theorem OAI.CoarseAssembly.winding_index line 35
  4. def OAI.CoarseAssembly.circleInputOfIndexOne line 45

    Source documentation

    All the published circle fields follow from a single coordinate-index-one class.

    def circleInputOfIndexOne (α : LocallyFiniteK1 WindingCircle)
    (hα : compactIndexPairing (circleUnitary (ContinuousMap.id WindingCircle)) α = 1) :
    PublishedCircleInput where
…

    Mentions: OAI.CoarseAssembly.WindingCircle, OAI.CoarseAssembly.circleUnitary, OAI.CoarseAssembly.PublishedCircleInput