Persistence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Algebraic persistence in the coarse Novikov construction

The direct-limit and rationalization arguments apply to arbitrary abelian groups. No compatibility between the tests at different scales is assumed or needed.

theorem OAI.CoarseAssembly.persistent_multiples_ne_zero line 27
Source documentation
A class detected with value one at every later scale has no nonzero integer multiple that vanishes in the actual algebraic direct limit. This is the last argument of the manuscript's Proposition 4.1, with the geometric tests supplied as explicit parameters. The tests need not form a compatible family.
```
theorem persistent_multiples_ne_zero (r₀ : ℕ) (a : G r₀)
    (test : ∀ r, r₀ ≤ r → G r →+ ℤ)
    (detects : ∀ r (hr : r₀ ≤ r), test r hr (f r₀ r hr a) = 1)
    (n : ℤ) (hn : n ≠ 0) :
    n • AddCommGroup.DirectLimit.of G f r₀ a ≠ 0 := by
…
```

theorem OAI.CoarseAssembly.persistent_cyclic_injective line 42

Source documentation

The cyclic subgroup generated by a persistently detected class is an embedded copy of the integers.

theorem persistent_cyclic_injective (r₀ : ℕ) (a : G r₀)
    (test : ∀ r, r₀ ≤ r → G r →+ ℤ)
    (detects : ∀ r (hr : r₀ ≤ r), test r hr (f r₀ r hr a) = 1) :
    Function.Injective (fun n : ℤ => n • AddCommGroup.DirectLimit.of G f r₀ a) := by
…

theorem OAI.CoarseAssembly.rationalization_ne_zero line 61
Source documentation
An element with no nonzero integer annihilator remains nonzero after rationalization. This is the torsion-kernel fact used after Proposition 4.1.
```
theorem rationalization_ne_zero (a : A)
    (ha : ∀ n : ℤ, n ≠ 0 → n • a ≠ 0) :
    (1 : ℚ) ⊗ₜ[ℤ] a ≠ 0 := by
…
```

theorem OAI.CoarseAssembly.kernel_obstructs_injectivity line 74

Source documentation

A non-torsion kernel element prevents both integral and rational injectivity. The scalar extension is the actual tensor product of groups.

theorem kernel_obstructs_injectivity (μ : A →+ B) (a : A)
    (ha : ∀ n : ℤ, n ≠ 0 → n • a ≠ 0) (hμ : μ a = 0) :
    ¬ Function.Injective μ ∧
      ¬ Function.Injective (μ.toIntLinearMap.lTensor ℚ) := by
…