OAI/Algebra/Finitistic/Rectification/SecondVertex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SecondVertex.vertex line 15
2. abbrev OAI.LittleFinitistic.SecondVertex.vertexComplex line 17
3. def OAI.LittleFinitistic.SecondVertex.intoF1 line 19
4. theorem OAI.LittleFinitistic.SecondVertex.intoF1_isIso line 23
5. theorem OAI.LittleFinitistic.SecondVertex.filtration_inclusion_quasiIso line 58
6. def OAI.LittleFinitistic.SecondVertex.iota line 66
7. theorem OAI.LittleFinitistic.SecondVertex.iota_quasiIso line 71
8. theorem OAI.LittleFinitistic.SecondVertex.intoF1_nested line 81

   Source documentation

   The filtration route retains the original vertex-one summand insertion.

   theorem intoF1_nested : intoF1 P D₀ D₁ D₂ f g ≫ Exactness.i1 s D₀ D₁ D₂ f g H =
       (Exactness.data s D₀ D₁ D₂ f g).in₁ ≫
         InducedRectification.inclusion s D₀ D₁ D₂ f g H := by
   …

   Mentions: OAI.LittleFinitistic.SecondVertex.intoF1, OAI.LittleFinitistic.InducedRectification.inclusion

9. theorem OAI.LittleFinitistic.SecondVertex.iota_original line 89