OAI/Algebra/Finitistic/Rectification/SourceFiltrationComplex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.ModuleComplexExact.comp_zero line 12
2. def OAI.LittleFinitistic.ModuleComplexExact.sequence line 16
3. theorem OAI.LittleFinitistic.ModuleComplexExact.shortExact line 19
4. def OAI.ExternalTensor.Section4.SourceFiltration.Complex.source0 line 37
5. def OAI.ExternalTensor.Section4.SourceFiltration.Complex.source1 line 41
6. theorem OAI.ExternalTensor.Section4.SourceFiltration.Complex.source0_shortExact line 45
7. theorem OAI.ExternalTensor.Section4.SourceFiltration.Complex.source1_shortExact line 50
8. theorem OAI.ExternalTensor.Section4.SourceFiltration.Complex.vertex_shortExact line 54

   Source documentation

   Every original source filtration remains short exact after taking a left vertex.

   theorem vertex_shortExact (e : B) (he : e*e=e)
       (S : ShortComplex (BiComplex k B)) (hS : S.ShortExact) :
       (S.map ((BimoduleVertex.functor k B e).mapHomologicalComplex (.up ℤ))).ShortExact := by
   …

   Mentions: OAI.ExternalTensor.Section4.BiComplex