VertexTotalProperties.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.VertexTotalProperties.projective line 12
Source documentation
The actual vertex of a right-projective bimodule remains right-projective.
```
theorem projective (e : B) (he : e*e=e) (M : ModuleCat.{u} (Enveloping k B))
    (hM : Projective ((forgetRight k B).obj M)) :
    Projective ((BimoduleVertex.functor k B e).obj M) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleVertex.functor

theorem OAI.LittleFinitistic.VertexTotalProperties.total_projective line 32

Source documentation

Every actual vertex of the constructed total has projective right-module terms.

theorem total_projective (v : Fin 3)
    (h₀ : ∀ n, Module.Projective (QuadraticEncoding.B P)ᵐᵒᵖ (D₀.X n))
    (h₁ : ∀ n, Module.Projective (QuadraticEncoding.B P)ᵐᵒᵖ (D₁.X n))
    (h₂ : ∀ n, Module.Projective (QuadraticEncoding.B P)ᵐᵒᵖ (D₂.X n)) (n : ℤ) :
    Projective (((AdjacentArrowSum.vertexComplex (QuadraticEncoding.composition P) v).obj
      (InducedRectification.total (ConcreteQuadraticDiagram.quadratic P) D₀ D₁ D₂ f g H)).X n) :=
…

Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.LittleFinitistic.QuadraticEncoding.composition, OAI.LittleFinitistic.InducedRectification.total, OAI.LittleFinitistic.ConcreteQuadraticDiagram.quadratic

theorem OAI.LittleFinitistic.VertexTotalProperties.total_bounded line 43