CirclePairing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The precise published circle-index input

Only the scalar-unitary index pairing, its naturality for a parametrized loop, and the classical winding formula are assumed. The domain groups are the Fredholm-module groups.

References: Blackadar, K-Theory for Operator Algebras, 2nd ed. (1998), Proposition 18.7.1 and Corollary 18.10.3; Khalkhali, Basic Noncommutative Geometry (2009), Example 4.2.4, with the sign convention of manuscript §2.3.

def OAI.CoarseAssembly.compactMap line 28
Source documentation
Continuous maps from a compact source are cocompact.
```
def compactMap [CompactSpace X] (f : C(X, Y)) : CocompactMap X Y where
…
```
theorem OAI.CoarseAssembly.compactMap_apply line 32
def OAI.CoarseAssembly.circleUnitary line 36
Source documentation
The scalar unitary represented by a circle-valued map.
```
def circleUnitary (f : C(X, WindingCircle)) : C(X, Circle) :=
…
```
Mentions: OAI.CoarseAssembly.WindingCircle
structure OAI.CoarseAssembly.PublishedCircleInput line 41
Source documentation
Minimal published analytic data needed to test loops. Each pairing f is the index pairing with the scalar unitary circleUnitary f.
```
structure PublishedCircleInput where
…
```
theorem OAI.CoarseAssembly.PublishedCircleInput.loop_pairing line 54
Source documentation
The constructed real lift is sufficient for the published index formula.
```
theorem PublishedCircleInput.loop_pairing (input : PublishedCircleInput)
    [CompactSpace Y] [T2Space Y] {y : Y}
    (f : C(Y, WindingCircle)) (γ : Path y y) (n : ℤ)
    (L : IntegerPathLift f γ n) :
    input.pairing f (pushforward (compactMap (loopCircle γ)) input.fundamental) = n := by
…
```
Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.WindingCircle, OAI.CoarseAssembly.IntegerPathLift, OAI.CoarseAssembly.compactMap, OAI.CoarseAssembly.loopCircle
theorem OAI.CoarseAssembly.PublishedCircleInput.fundamental_infinite_order line 66
Source documentation
In particular the normalized circle class has infinite order; this deduction is not part of the assumed published data.
```
theorem PublishedCircleInput.fundamental_infinite_order (input : PublishedCircleInput)
    (n : ℤ) (hn : n ≠ 0) : n • input.fundamental ≠ 0 := by
…
```
Mentions: OAI.CoarseAssembly.PublishedCircleInput