InducedDerivedFunctor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.induced_term_projective line 21
Source documentation
The fixed native rectification supplies the precise projectivity required by the frozen total theorem.
```
theorem induced_term_projective (n : ℤ) : Module.Projective Bᵐᵒᵖ
    (ComplexTensor.rightTerm k B (right k B
      (InducedRectification.total s D₀ D₁ D₂ f g H)) n) := by
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.InducedRectification.total
def OAI.LittleFinitistic.BimoduleTotal.inducedDerived line 31
Source documentation
Native P is fixed before the arbitrary derived input is supplied.
```
def inducedDerived (lo hi : ℤ) :
    DerivedCategory (ModuleCat.{u} B) ⥤ DerivedCategory (ModuleCat.{u} B) := by
…
```

theorem OAI.LittleFinitistic.BimoduleTotal.induced_complete line 40

Source documentation

The selected interval contains the complete actual native P whenever the source complexes have these bounds.

theorem induced_complete (lo hi : ℤ)
    (b₀ : ∀ n, n < lo ∨ hi < n → IsZero (D₀.X n))
    (b₁ : ∀ n, n < lo ∨ hi < n → IsZero (D₁.X n))
    (b₂ : ∀ n, n < lo ∨ hi < n → IsZero (D₂.X n))
    (n : ℤ) (hn : ∀ i, intervalDegrees (lo-2) hi i ≠ n) :
    IsZero ((InducedRectification.total s D₀ D₁ D₂ f g H).X n) :=
…

Mentions: OAI.LittleFinitistic.BimoduleTotal.intervalDegrees, OAI.LittleFinitistic.InducedRectification.total