AdditiveIterateAmplitude.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.IterateSupport.additive_resolved_exact_above line 17
Source documentation
A terminal additive functor applied to the actual projective bar resolution has finite support when the input has finite cohomological support. This covers balanced tensor with arbitrary right modules, not just the fixed bimodule.
```
theorem additive_resolved_exact_above (Z : ChainComplex (ModuleCat.{u} D) ℕ) (m : ℕ)
    (hZ : ∀ i, m < i → Z.ExactAt i) (n : ℕ) (hn : m+g+2 < n) :
    ((F.mapHomologicalComplex (.down ℕ)).obj (barTotal k D Z)).ExactAt n := by
…
```
Mentions: OAI.DerivedBar.barTotal
theorem OAI.DerivedBar.IterateSupport.iterated_additive_exact_above line 35
Source documentation
The extra resolved tensor used for residue/base Tor also has a finite bound, uniformly after every actual derived iteration.
```
theorem iterated_additive_exact_above (r n : ℕ) (hn : (r+1)*(g+2) < n) :
    ((F.mapHomologicalComplex (.down ℕ)).obj
      (barTotal k D (resolvedModel k D X N r))).ExactAt n := by
…
```
Mentions: OAI.DerivedBar.barTotal, OAI.DerivedBar.IterateSupport.resolvedModel

theorem OAI.DerivedBar.IterateSupport.nonzero_in_finite_window line 47

Source documentation

Nonzero genuine iterates are detected in a proved finite cohomological window.

theorem nonzero_in_finite_window (r : ℕ) (h : ¬ IsZero (object k D X N r)) :
    ∃ n : ℕ, n ≤ r*(g+2) ∧
      ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj
        (object k D X N r)) := by
…

Mentions: OAI.DerivedBar.IterateSupport.object