OAI/Algebra/Finitistic/Rectification/FirstVertex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.FirstVertex.biprodInlIso line 12
2. theorem OAI.LittleFinitistic.FirstVertex.mapped_inl_isIso line 21
3. abbrev OAI.LittleFinitistic.FirstVertex.vertexComplex line 39
4. def OAI.LittleFinitistic.FirstVertex.columnInclusion line 45

   Source documentation

   The original first induced column includes into the actual zero column.

   def columnInclusion : (columnComplex k B (s).e₀).obj D₀ ⟶ L0Prime s D₀ D₁ D₂ f g := biprod.inl

5. theorem OAI.LittleFinitistic.FirstVertex.columnInclusion_isIso line 47
6. def OAI.LittleFinitistic.FirstVertex.iota line 57

   Source documentation

   The manuscript's original first-vertex insertion into the constructed total.

   def iota : D₀ ⟶ (vertexComplex P).obj (InducedRectification.total s D₀ D₁ D₂ f g H) :=
   …

   Mentions: OAI.LittleFinitistic.FirstVertex.vertexComplex, OAI.LittleFinitistic.InducedRectification.total

7. theorem OAI.LittleFinitistic.FirstVertex.iota_isIso line 63

   Source documentation

   At the first vertex the original insertion is already a chain isomorphism.

   theorem iota_isIso : IsIso (iota P D₀ D₁ D₂ f g H) := by
   …

   Mentions: OAI.LittleFinitistic.FirstVertex.iota