RectificationLemma.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.LittleFinitistic.RectificationLemma.Verified line 17
Source documentation
The conclusions of the paper's rectification lemma for the explicitly constructed bimodule complex and original vertex insertion maps.
```
structure Verified (lo hi : ℤ) : Prop where
…
```

theorem OAI.LittleFinitistic.RectificationLemma.rectification line 39

Source documentation

Full rectification for arbitrary bounded finite projective input complexes, using only the assigned relation homotopies. No conclusion about the constructed P, its vertices, or its arrow homotopies is assumed.

theorem rectification (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))
    (p₀ : ∀ n, Module.Projective (B P)ᵐᵒᵖ (D₀.X n))
    (p₁ : ∀ n, Module.Projective (B P)ᵐᵒᵖ (D₁.X n))
    (p₂ : ∀ n, Module.Projective (B P)ᵐᵒᵖ (D₂.X n))
    (f₀ : ∀ n, Module.Finite (B P)ᵐᵒᵖ (D₀.X n))
    (f₁ : ∀ n, Module.Finite (B P)ᵐᵒᵖ (D₁.X n))
    (f₂ : ∀ n, Module.Finite (B P)ᵐᵒᵖ (D₂.X n)) :
    Verified P D₀ D₁ D₂ f g H lo hi := by
…

Mentions: OAI.LittleFinitistic.RectificationLemma.Verified