IntegerIterateExtinction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.IterateSupport.integerQ_isZero_iff line 17
Source documentation
The integer derived object of an actual nonnegative chain complex vanishes exactly when the original chain complex is exact in every degree.
```
theorem integerQ_isZero_iff (Z : ChainComplex (ModuleCat.{u} D) ℕ) :
    IsZero ((integerQ D).obj Z) ↔ ∀ n, Z.ExactAt n := by
…
```
Mentions: OAI.DerivedBar.integerQ
theorem OAI.DerivedBar.IterateSupport.tensor_acyclic line 63
Source documentation
The actual resolve-and-tensor functor sends an acyclic chain input to an acyclic output.
```
theorem tensor_acyclic (Z : ChainComplex (ModuleCat.{u} D) ℕ)
    (h : ∀ n, Z.ExactAt n) : ∀ n, ((tensorTotalFunctor k D X).obj Z).ExactAt n := by
…
```
Mentions: OAI.DerivedBar.tensorTotalFunctor
theorem OAI.DerivedBar.IterateSupport.zero_succ line 79
Source documentation
Extinction is permanent for the genuine bar-derived iteration.
```
theorem zero_succ (r : ℕ) (h : IsZero (object k D X N r)) :
    IsZero (object k D X N (r+1)) := by
…
```
Mentions: OAI.DerivedBar.IterateSupport.object
theorem OAI.DerivedBar.IterateSupport.zero_of_le line 88
Source documentation
A proved zero iterate kills every later iterate, without a native-functor comparison premise.
```
theorem zero_of_le (t r : ℕ) (htr : t ≤ r) (h : IsZero (object k D X N t)) :
    IsZero (object k D X N r) := by
…
```
Mentions: OAI.DerivedBar.IterateSupport.object