CountTorBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.baseChangeTor_zero_iff_counts line 26
Source documentation
Exact degreewise vanishing criterion for actual base-change Tor, in terms of the original integer-derived count objects.
```
theorem baseChangeTor_zero_iff_counts (n : ℕ) :
    IsZero (((Balanced.tensorFunctor (fstHom k D X)).leftDerived n).obj (ModuleCat.of A N)) ↔
      ∀ r, IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n:ℤ))).obj
        ((integerQ D).obj (S r))) := by
…
```
Mentions: OAI.DerivedBar.Balanced.tensorFunctor, OAI.DerivedBar.integerQ
theorem OAI.DerivedBar.ParityBridge.baseChangeTor_bounded_of_counts line 38
Source documentation
A uniform upper bound on the original count homologies is a uniform bound on actual base-change Tor. This is the consumer for Native's uniform count window.
```
theorem baseChangeTor_bounded_of_counts (B : ℕ)
    (h : ∀ r n, B < n →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n:ℤ))).obj
        ((integerQ D).obj (S r)))) :
    ∀ n, B < n →
      IsZero (((Balanced.tensorFunctor (fstHom k D X)).leftDerived n).obj (ModuleCat.of A N)) :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.Balanced.tensorFunctor

theorem OAI.DerivedBar.ParityBridge.baseChangeTor_nonzero_ge_of_count line 48

Source documentation

Any nonzero count homology witness above r gives a nonzero actual Tor witness above r, without replacing projective dimension by an invented invariant.

theorem baseChangeTor_nonzero_ge_of_count (r : ℕ)
    (h : ∃ n, r ≤ n ∧
      ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n:ℤ))).obj
        ((integerQ D).obj (S r)))) :
    ∃ n, r ≤ n ∧
      ¬ IsZero (((Balanced.tensorFunctor (fstHom k D X)).leftDerived n).obj (ModuleCat.of A N)) := by
…

Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.Balanced.tensorFunctor