RectificationTotal.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.RectificationTotal.rectifyingMap line 13
Source documentation
The relation null-homotopy extends p over the first cone.
```
noncomputable def rectifyingMap : mappingCone q ⟶ L₀ :=
…
```
def OAI.LittleFinitistic.RectificationTotal.total line 19
Source documentation
A genuine cochain complex rectifying a three-column homotopy diagram. The cone convention fixes all differential signs; the three-column term isomorphism is given below.
```
noncomputable def total : CochainComplex C ℤ := mappingCone (rectifyingMap p q h)
```
Mentions: OAI.LittleFinitistic.RectificationTotal.rectifyingMap
def OAI.LittleFinitistic.RectificationTotal.termIso line 22
Source documentation
The total complex has exactly the three finite columns.
```
noncomputable def termIso (i : ℤ) :
    (total p q h).X i ≅ (L₂.X (i+2) ⊞ L₁.X (i+1)) ⊞ L₀.X i :=
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total
theorem OAI.LittleFinitistic.RectificationTotal.total_isZero line 27

theorem OAI.LittleFinitistic.RectificationTotal.total_bounded line 33

Source documentation

Bounded columns give a bounded actual total complex.

theorem total_bounded (lo hi : ℤ)
    (h₀ : ∀ i, i < lo ∨ hi < i → IsZero (L₀.X i))
    (h₁ : ∀ i, i < lo ∨ hi < i → IsZero (L₁.X i))
    (h₂ : ∀ i, i < lo ∨ hi < i → IsZero (L₂.X i)) :
    ∀ i, i < lo-2 ∨ hi < i → IsZero ((total p q h).X i) := by
…

Mentions: OAI.LittleFinitistic.RectificationTotal.total

theorem OAI.LittleFinitistic.RectificationTotal.total_projective line 43
Source documentation
Termwise projectivity is preserved by the concrete three-column construction.
```
theorem total_projective (h₀ : ∀ i, Projective (L₀.X i))
    (h₁ : ∀ i, Projective (L₁.X i)) (h₂ : ∀ i, Projective (L₂.X i)) :
    ∀ i, Projective ((total p q h).X i) := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total
def OAI.LittleFinitistic.RectificationTotal.inclusion line 54
Source documentation
The original zero column includes by an actual chain map.
```
noncomputable def inclusion : L₀ ⟶ total p q h := mappingCone.inr (rectifyingMap p q h)
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total, OAI.LittleFinitistic.RectificationTotal.rectifyingMap
def OAI.LittleFinitistic.RectificationTotal.boundaryHomotopy line 58
Source documentation
The first-column boundary vanishes by a specified chain homotopy in the total. For the induced B-arrow columns this is exactly the arrow compatibility homotopy.
```
noncomputable def boundaryHomotopy : Homotopy (p ≫ inclusion p q h) 0 := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.inclusion
theorem OAI.LittleFinitistic.RectificationTotal.total_projective_after line 71
Source documentation
Projectivity after an additive forgetful functor, needed for right projectivity of a total built in the category of bimodules.
```
theorem total_projective_after (F : C ⥤ D) [F.Additive]
    (h₀ : ∀ i, Projective (F.obj (L₀.X i)))
    (h₁ : ∀ i, Projective (F.obj (L₁.X i)))
    (h₂ : ∀ i, Projective (F.obj (L₂.X i))) :
    ∀ i, Projective (F.obj ((total p q h).X i)) := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total