OAI/Algebra/Finitistic/Rectification/ThirdVertexFiltration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ThirdVertexFiltration.vertexComplex line 13
2. theorem OAI.LittleFinitistic.ThirdVertexFiltration.inclusion_quasiIso line 16

   Source documentation

   The original deepest source-filtration inclusion is a quasi-isomorphism at vertex two.

   theorem inclusion_quasiIso :
       QuasiIso ((vertexComplex P).map (Exactness.i2 s D₀ D₁ D₂ f g)) := by
   …

   Mentions: OAI.LittleFinitistic.ThirdVertexFiltration.vertexComplex