GradedVertexAcyclic.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.GradedVertexAcyclic.acyclic_of_iso line 11
def OAI.LittleFinitistic.GradedVertexAcyclic.grade1VertexIso line 26
Source documentation
The actual source-one quotient is the adjacent-arrow cone after taking vertex two.
```
def grade1VertexIso :
    (AdjacentArrowSum.vertexComplex (QuadraticEncoding.composition P) 2).obj
      (Exactness.G1 s D₀ D₁ D₂ f g) ≅
    mappingCone ((AdjacentArrowSum.vertexComplex (QuadraticEncoding.composition P) 2).map
      (ConcreteAdjacentGraded.arrow12Sum P D₁)) :=
…
```
Mentions: OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.LittleFinitistic.QuadraticEncoding.composition, OAI.LittleFinitistic.ConcreteAdjacentGraded.arrow12Sum
theorem OAI.LittleFinitistic.GradedVertexAcyclic.grade1_vertex2_acyclic line 36
theorem OAI.LittleFinitistic.GradedVertexAcyclic.relationColumn_vertex1_zero line 43
Source documentation
The relation column of the actual source-zero quotient vanishes at vertex one.
```
theorem relationColumn_vertex1_zero :
    IsZero ((AdjacentArrowSum.vertexComplex (QuadraticEncoding.composition P) 1).obj
      (Exactness.data s D₀ D₁ D₂ f g).L₂) := by
…
```
Mentions: OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.LittleFinitistic.QuadraticEncoding.composition
def OAI.LittleFinitistic.GradedVertexAcyclic.grade0Vertex1Iso line 54
Source documentation
The actual source-zero quotient at vertex one is the first adjacent-arrow cone.
```
def grade0Vertex1Iso :
    (AdjacentArrowSum.vertexComplex (QuadraticEncoding.composition P) 1).obj
      (Exactness.G0 s D₀ D₁ D₂ f g) ≅
    mappingCone ((AdjacentArrowSum.vertexComplex (QuadraticEncoding.composition P) 1).map
      (ConcreteAdjacentGraded.arrow01Sum P D₀)) :=
…
```
Mentions: OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.LittleFinitistic.QuadraticEncoding.composition, OAI.LittleFinitistic.ConcreteAdjacentGraded.arrow01Sum
theorem OAI.LittleFinitistic.GradedVertexAcyclic.grade0_vertex1_acyclic line 64