OAI/Algebra/Finitistic/Ordinary/OrdinaryFiniteColumnComplex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.FiniteColumnComplex.term line 13
2. structure OAI.LittleFinitistic.FiniteColumnComplex.Differential line 16

   Source documentation

   A finite-column total differential, recorded independently of a chosen direct-sum presentation.

   structure Differential where
   …

3. def OAI.LittleFinitistic.FiniteColumnComplex.complex line 25
4. theorem OAI.LittleFinitistic.FiniteColumnComplex.complex_d line 29
5. theorem OAI.LittleFinitistic.FiniteColumnComplex.complex_d_hom line 34
6. theorem OAI.LittleFinitistic.FiniteColumnComplex.lower_single line 39
7. theorem OAI.LittleFinitistic.FiniteColumnComplex.diagonal_single line 48
8. theorem OAI.LittleFinitistic.FiniteColumnComplex.acyclic line 57

   Source documentation

   Finite totalization preserves acyclicity when every column is acyclic.

   theorem acyclic (hK : ∀ i, (K i).Acyclic) : (complex K δ).Acyclic := by
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.complex