ShortLoops.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Short loops and the Rips edge cocycle

The combinatorial step in §4 of the coarse Novikov manuscript. The only hypothesis on the charge is vanishing on short closed graph walks, exactly the output required from the manuscript's small-loop lemma. This is a conditional combinatorial result, not an assumption about analytic K-homology.

def OAI.CoarseAssembly.walkCharge line 20

Source documentation

Sum an integer edge charge along an actual graph walk.

def walkCharge (a : V → V → ℤ) : {u v : V} → G.Walk u v → ℤ
  | _, _, .nil => 0
  | u, _, .cons (v := v) _ p => a u v + walkCharge a p

theorem OAI.CoarseAssembly.walkCharge_nil line 24
theorem OAI.CoarseAssembly.walkCharge_cons line 27
theorem OAI.CoarseAssembly.walkCharge_append line 31
theorem OAI.CoarseAssembly.walkCharge_reverse line 38
theorem OAI.CoarseAssembly.walkCharge_abs_le_length line 47
Source documentation
Pointwise unit charges give the elementary length bound used to control both the winding number and the word length in the small-loop argument.
```
theorem walkCharge_abs_le_length (a : V → V → ℤ)
    (ha : ∀ u v, G.Adj u v → |a u v| ≤ 1) {u v : V} (p : G.Walk u v) :
    |walkCharge a p| ≤ (p.length : ℤ) := by
…
```
Mentions: OAI.CoarseAssembly.walkCharge

theorem OAI.CoarseAssembly.walkCharge_eq_of_short_loops line 61

Source documentation

Vanishing short loops makes the charge independent of the chosen short path. The two paths are compared by concatenating one with the reverse of the other, exactly as in Proposition 4.1.

theorem walkCharge_eq_of_short_loops (a : V → V → ℤ)
    (ha : ∀ u v, G.Adj u v → a v u = -a u v) (r : ℕ)
    (hloop : ∀ u (p : G.Walk u u), p.length ≤ 2 * r → walkCharge a p = 0)
    {u v : V} (p q : G.Walk u v) (hp : p.length ≤ r) (hq : q.length ≤ r) :
    walkCharge a p = walkCharge a q := by
…

Mentions: OAI.CoarseAssembly.walkCharge

def OAI.CoarseAssembly.ripsGraph line 76
Source documentation
The graph of the edges of the Rips complex of a connected graph at scale r. Connectedness is supplied to results, because graph distance is zero between disconnected vertices in Mathlib's natural-valued convention.
```
def ripsGraph (G : SimpleGraph V) (r : ℕ) : SimpleGraph V where
…
```
def OAI.CoarseAssembly.shortestWalk line 81
theorem OAI.CoarseAssembly.shortestWalk_length line 84
def OAI.CoarseAssembly.ripsCharge line 90
Source documentation
The charge assigned to an oriented Rips edge, extended to all vertex pairs by choosing shortest graph walks.
```
noncomputable def ripsCharge (hG : G.Connected) (a : V → V → ℤ) (u v : V) : ℤ :=
…
```
theorem OAI.CoarseAssembly.ripsCharge_eq_walkCharge line 93

theorem OAI.CoarseAssembly.ripsCharge_antisymm line 104

Source documentation

The Rips charge is antisymmetric whenever loops of length at most 2r have zero charge.

theorem ripsCharge_antisymm (hG : G.Connected) (a : V → V → ℤ)
    (ha : ∀ u v, G.Adj u v → a v u = -a u v) (r : ℕ)
    (hloop : ∀ u (p : G.Walk u u), p.length ≤ 2 * r → walkCharge a p = 0)
    {u v : V} (huv : G.dist u v ≤ r) :
    ripsCharge hG a v u = -ripsCharge hG a u v := by
…

Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.ripsCharge

theorem OAI.CoarseAssembly.ripsCharge_triangle line 116

Source documentation

Every triangle in the Rips complex has zero total charge, assuming vanishing of graph loops of length at most 3r. This is the cocycle identity needed for the circle-valued winding test.

theorem ripsCharge_triangle (hG : G.Connected) (a : V → V → ℤ) (r : ℕ)
    (hloop : ∀ u (p : G.Walk u u), p.length ≤ 3 * r → walkCharge a p = 0)
    {u v w : V} (huv : G.dist u v ≤ r) (hvw : G.dist v w ≤ r)
    (hwu : G.dist w u ≤ r) :
    ripsCharge hG a u v + ripsCharge hG a v w + ripsCharge hG a w u = 0 := by
…

Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.ripsCharge

theorem OAI.CoarseAssembly.ripsCharge_on_edge line 130

Source documentation

Unit graph edges retain their original charges in the Rips cocycle.

theorem ripsCharge_on_edge (hG : G.Connected) (a : V → V → ℤ)
    (ha : ∀ u v, G.Adj u v → a v u = -a u v) (r : ℕ) (hr : 1 ≤ r)
    (hloop : ∀ u (p : G.Walk u u), p.length ≤ 2 * r → walkCharge a p = 0)
    {u v : V} (h : G.Adj u v) : ripsCharge hG a u v = a u v := by
…

Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.ripsCharge

theorem OAI.CoarseAssembly.ripsCharge_on_walk line 139

Source documentation

In particular, the same boundary walk has the same winding charge after passing to a Rips scale.

theorem ripsCharge_on_walk (hG : G.Connected) (a : V → V → ℤ)
    (ha : ∀ u v, G.Adj u v → a v u = -a u v) (r : ℕ) (hr : 1 ≤ r)
    (hloop : ∀ u (p : G.Walk u u), p.length ≤ 2 * r → walkCharge a p = 0)
    {u v : V} (p : G.Walk u v) :
    walkCharge (ripsCharge hG a) p = walkCharge a p := by
…

Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.ripsCharge

theorem OAI.CoarseAssembly.exists_rips_cocycle line 152

Source documentation

The finite-scale combinatorial conclusion used in the paper: a charge-one boundary and vanishing of loops through length 3r give an antisymmetric integer Rips cocycle that still evaluates to one on that boundary.

theorem exists_rips_cocycle (hG : G.Connected) (a : V → V → ℤ)
    (ha : ∀ u v, G.Adj u v → a v u = -a u v) (r : ℕ) (hr : 1 ≤ r)
    (hloop : ∀ u (p : G.Walk u u), p.length ≤ 3 * r → walkCharge a p = 0)
    {u : V} (boundary : G.Walk u u) (hboundary : walkCharge a boundary = 1) :
    ∃ b : V → V → ℤ,
      (∀ x y, G.dist x y ≤ r → b y x = -b x y) ∧
      (∀ x y z, G.dist x y ≤ r → G.dist y z ≤ r → G.dist z x ≤ r →
        b x y + b y z + b z x = 0) ∧ walkCharge b boundary = 1 := by
…

Mentions: OAI.CoarseAssembly.walkCharge