OAI/Algebra/Finitistic/Rectification/ThirdVertex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ThirdVertex.vertexComplex line 16
2. theorem OAI.LittleFinitistic.ThirdVertex.filtration_inclusion_quasiIso line 18
3. def OAI.LittleFinitistic.ThirdVertex.iota line 27
4. theorem OAI.LittleFinitistic.ThirdVertex.iota_quasiIso line 32
5. theorem OAI.LittleFinitistic.ThirdVertex.iota_original line 42

   Source documentation

   The final-vertex map is the original e2 tensor insertion followed by the original total inclusion.

   theorem iota_original : iota P D₀ D₁ D₂ f g H =
       (VertexColumnComplex.diagonalComplexIso (QuadraticEncoding.composition P) 2 D₂).hom ≫
         (vertexComplex P).map ((Exactness.data s D₀ D₁ D₂ f g).in₂) ≫
         (vertexComplex P).map (InducedRectification.inclusion s D₀ D₁ D₂ f g H) := by
   …

   Mentions: OAI.LittleFinitistic.ThirdVertex.iota, OAI.LittleFinitistic.VertexColumnComplex.diagonalComplexIso, OAI.LittleFinitistic.QuadraticEncoding.composition, OAI.LittleFinitistic.ThirdVertex.vertexComplex, OAI.LittleFinitistic.InducedRectification.inclusion