TotalFinite.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExternalTensor.Section4.total_finite_after line 17
Source documentation
The rectification total has finite-dimensional terms whenever an additive scalar restriction makes all three columns finite-dimensional.
```
theorem total_finite_after (F : C ⥤ ModuleCat.{u} k) [F.Additive]
    (h₀ : ∀ i, FiniteDimensional k (F.obj (L₀.X i)))
    (h₁ : ∀ i, FiniteDimensional k (F.obj (L₁.X i)))
    (h₂ : ∀ i, FiniteDimensional k (F.obj (L₂.X i))) (i : ℤ) :
    FiniteDimensional k (F.obj ((LittleFinitistic.RectificationTotal.total p q h).X i)) := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.h

theorem OAI.ExternalTensor.Section4.induced_total_finite line 38

Source documentation

The finite-dimensionality conclusion for the manuscript's constructed P, with no projectivity or finite-dimensionality assumption on P or its columns.

theorem induced_total_finite [FiniteDimensional k B]
    (h₀ : ∀ i, Module.Finite Bᵐᵒᵖ (D₀.X i))
    (h₁ : ∀ i, Module.Finite Bᵐᵒᵖ (D₁.X i))
    (h₂ : ∀ i, Module.Finite Bᵐᵒᵖ (D₂.X i)) (i : ℤ) :
    FiniteDimensional k ((forgetK k B).obj
      ((LittleFinitistic.RectificationTotal.total (p s D₀ D₁ D₂ f g)
        (q s D₀ D₁ D₂ f g) (nullHomotopy s D₀ D₁ D₂ f g H)).X i)) := by
…

Mentions: OAI.ExternalTensor.Section4.forgetK, OAI.LittleFinitistic.RectificationTotal.total, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.nullHomotopy