InducedRectification.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.InducedRectification.total line 20
Source documentation
The actual three-column induced bimodule complex of Section 4.
```
def total : BiComplex k B :=
…
```
def OAI.LittleFinitistic.InducedRectification.rightTotal line 25
Source documentation
Its right-module restriction, retaining the original bimodule construction.
```
def rightTotal : RightComplex B :=
…
```
theorem OAI.LittleFinitistic.InducedRectification.total_bounded line 28

theorem OAI.LittleFinitistic.InducedRectification.rightTotal_projective line 39

Source documentation

Termwise projectivity holds for the actual right restriction of the total.

theorem rightTotal_projective
    (h₀ : ∀ n, Module.Projective Bᵐᵒᵖ (D₀.X n))
    (h₁ : ∀ n, Module.Projective Bᵐᵒᵖ (D₁.X n))
    (h₂ : ∀ n, Module.Projective Bᵐᵒᵖ (D₂.X n)) :
    ∀ n, Projective ((rightTotal s D₀ D₁ D₂ f g H).X n) := by
…

Mentions: OAI.LittleFinitistic.InducedRectification.rightTotal

def OAI.LittleFinitistic.InducedRectification.inclusion line 49
Source documentation
The entire zero column has its original chain inclusion.
```
def inclusion : L0Prime s D₀ D₁ D₂ f g ⟶ total s D₀ D₁ D₂ f g H :=
…
```
Mentions: OAI.LittleFinitistic.InducedRectification.total
def OAI.LittleFinitistic.InducedRectification.boundaryHomotopy line 53
Source documentation
The prescribed first boundary becomes null-homotopic in the actual total.
```
def boundaryHomotopy : Homotopy
    (p s D₀ D₁ D₂ f g ≫ inclusion s D₀ D₁ D₂ f g H) 0 :=
…
```
Mentions: OAI.LittleFinitistic.InducedRectification.inclusion